src/HOL/Lim.thy
changeset 44571 bd91b77c4cd6
parent 44570 b93d1b3ee300
child 45031 9583f2b56f85
     1.1 --- a/src/HOL/Lim.thy	Sun Aug 28 16:28:07 2011 -0700
     1.2 +++ b/src/HOL/Lim.thy	Sun Aug 28 20:56:49 2011 -0700
     1.3 @@ -114,32 +114,25 @@
     1.4    by (rule metric_LIM_imp_LIM [OF f],
     1.5      simp add: dist_norm le)
     1.6  
     1.7 -lemma trivial_limit_at:
     1.8 -  fixes a :: "'a::real_normed_algebra_1"
     1.9 -  shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
    1.10 -unfolding trivial_limit_def
    1.11 -unfolding eventually_at dist_norm
    1.12 -by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
    1.13 -
    1.14  lemma LIM_const_not_eq:
    1.15 -  fixes a :: "'a::real_normed_algebra_1"
    1.16 +  fixes a :: "'a::perfect_space"
    1.17    fixes k L :: "'b::t2_space"
    1.18    shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
    1.19 -by (simp add: tendsto_const_iff trivial_limit_at)
    1.20 +  by (simp add: tendsto_const_iff)
    1.21  
    1.22  lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
    1.23  
    1.24  lemma LIM_const_eq:
    1.25 -  fixes a :: "'a::real_normed_algebra_1"
    1.26 +  fixes a :: "'a::perfect_space"
    1.27    fixes k L :: "'b::t2_space"
    1.28    shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
    1.29 -  by (simp add: tendsto_const_iff trivial_limit_at)
    1.30 +  by (simp add: tendsto_const_iff)
    1.31  
    1.32  lemma LIM_unique:
    1.33 -  fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
    1.34 +  fixes a :: "'a::perfect_space"
    1.35    fixes L M :: "'b::t2_space"
    1.36    shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
    1.37 -  using trivial_limit_at by (rule tendsto_unique)
    1.38 +  using at_neq_bot by (rule tendsto_unique)
    1.39  
    1.40  text{*Limits are equal for functions equal except at limit point*}
    1.41  lemma LIM_equal: