generalize LIM_zero lemmas to arbitrary filters
authorhuffman
Sun, 28 Aug 2011 16:28:07 -0700
changeset 44570 b93d1b3ee300
parent 44569 44525dd281d4
child 44571 bd91b77c4cd6
generalize LIM_zero lemmas to arbitrary filters
src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Sun Aug 28 09:22:42 2011 -0700
+++ b/src/HOL/Lim.thy	Sun Aug 28 16:28:07 2011 -0700
@@ -85,17 +85,17 @@
 
 lemma LIM_zero:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
-  shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
+  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
 unfolding tendsto_iff dist_norm by simp
 
 lemma LIM_zero_cancel:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
-  shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
+  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
 unfolding tendsto_iff dist_norm by simp
 
 lemma LIM_zero_iff:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
+  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
 unfolding tendsto_iff dist_norm by simp
 
 lemma metric_LIM_imp_LIM: