src/HOL/Lim.thy
changeset 44205 18da2a87421c
parent 44194 0639898074ae
child 44217 5cdad94bdc29
     1.1 --- a/src/HOL/Lim.thy	Sun Aug 14 08:45:38 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sun Aug 14 10:25:43 2011 -0700
     1.3 @@ -181,32 +181,32 @@
     1.4  lemma LIM_rabs_zero_iff: "(\<lambda>x. \<bar>f x\<bar>) -- a --> (0::real) = f -- a --> 0"
     1.5    by (rule tendsto_rabs_zero_iff)
     1.6  
     1.7 -lemma at_neq_bot:
     1.8 +lemma trivial_limit_at:
     1.9    fixes a :: "'a::real_normed_algebra_1"
    1.10 -  shows "at a \<noteq> bot"  -- {* TODO: find a more appropriate class *}
    1.11 -unfolding eventually_False [symmetric]
    1.12 +  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
    1.13 +unfolding trivial_limit_def
    1.14  unfolding eventually_at dist_norm
    1.15  by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
    1.16  
    1.17  lemma LIM_const_not_eq:
    1.18    fixes a :: "'a::real_normed_algebra_1"
    1.19 -  fixes k L :: "'b::metric_space"
    1.20 +  fixes k L :: "'b::t2_space"
    1.21    shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
    1.22 -by (simp add: tendsto_const_iff at_neq_bot)
    1.23 +by (simp add: tendsto_const_iff trivial_limit_at)
    1.24  
    1.25  lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
    1.26  
    1.27  lemma LIM_const_eq:
    1.28    fixes a :: "'a::real_normed_algebra_1"
    1.29 -  fixes k L :: "'b::metric_space"
    1.30 +  fixes k L :: "'b::t2_space"
    1.31    shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
    1.32 -by (simp add: tendsto_const_iff at_neq_bot)
    1.33 +  by (simp add: tendsto_const_iff trivial_limit_at)
    1.34  
    1.35  lemma LIM_unique:
    1.36    fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
    1.37 -  fixes L M :: "'b::metric_space"
    1.38 +  fixes L M :: "'b::t2_space"
    1.39    shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
    1.40 -by (drule (1) tendsto_dist, simp add: tendsto_const_iff at_neq_bot)
    1.41 +  using trivial_limit_at by (rule tendsto_unique)
    1.42  
    1.43  lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
    1.44  by (rule tendsto_ident_at)