src/HOL/Lim.thy
changeset 44571 bd91b77c4cd6
parent 44570 b93d1b3ee300
child 45031 9583f2b56f85
equal deleted inserted replaced
44570:b93d1b3ee300 44571:bd91b77c4cd6
   112   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   112   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
   113   shows "g -- a --> m"
   113   shows "g -- a --> m"
   114   by (rule metric_LIM_imp_LIM [OF f],
   114   by (rule metric_LIM_imp_LIM [OF f],
   115     simp add: dist_norm le)
   115     simp add: dist_norm le)
   116 
   116 
   117 lemma trivial_limit_at:
       
   118   fixes a :: "'a::real_normed_algebra_1"
       
   119   shows "\<not> trivial_limit (at a)"  -- {* TODO: find a more appropriate class *}
       
   120 unfolding trivial_limit_def
       
   121 unfolding eventually_at dist_norm
       
   122 by (clarsimp, rule_tac x="a + of_real (d/2)" in exI, simp)
       
   123 
       
   124 lemma LIM_const_not_eq:
   117 lemma LIM_const_not_eq:
   125   fixes a :: "'a::real_normed_algebra_1"
   118   fixes a :: "'a::perfect_space"
   126   fixes k L :: "'b::t2_space"
   119   fixes k L :: "'b::t2_space"
   127   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
   120   shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
   128 by (simp add: tendsto_const_iff trivial_limit_at)
   121   by (simp add: tendsto_const_iff)
   129 
   122 
   130 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
   123 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
   131 
   124 
   132 lemma LIM_const_eq:
   125 lemma LIM_const_eq:
   133   fixes a :: "'a::real_normed_algebra_1"
   126   fixes a :: "'a::perfect_space"
   134   fixes k L :: "'b::t2_space"
   127   fixes k L :: "'b::t2_space"
   135   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
   128   shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
   136   by (simp add: tendsto_const_iff trivial_limit_at)
   129   by (simp add: tendsto_const_iff)
   137 
   130 
   138 lemma LIM_unique:
   131 lemma LIM_unique:
   139   fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
   132   fixes a :: "'a::perfect_space"
   140   fixes L M :: "'b::t2_space"
   133   fixes L M :: "'b::t2_space"
   141   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
   134   shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
   142   using trivial_limit_at by (rule tendsto_unique)
   135   using at_neq_bot by (rule tendsto_unique)
   143 
   136 
   144 text{*Limits are equal for functions equal except at limit point*}
   137 text{*Limits are equal for functions equal except at limit point*}
   145 lemma LIM_equal:
   138 lemma LIM_equal:
   146      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   139      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
   147 unfolding tendsto_def eventually_at_topological by simp
   140 unfolding tendsto_def eventually_at_topological by simp