src/HOL/Lim.thy
 changeset 44570 b93d1b3ee300 parent 44568 e6f291cb5810 child 44571 bd91b77c4cd6
```     1.1 --- a/src/HOL/Lim.thy	Sun Aug 28 09:22:42 2011 -0700
1.2 +++ b/src/HOL/Lim.thy	Sun Aug 28 16:28:07 2011 -0700
1.3 @@ -85,17 +85,17 @@
1.4
1.5  lemma LIM_zero:
1.6    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.7 -  shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
1.8 +  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
1.9  unfolding tendsto_iff dist_norm by simp
1.10
1.11  lemma LIM_zero_cancel:
1.12    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.13 -  shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
1.14 +  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
1.15  unfolding tendsto_iff dist_norm by simp
1.16
1.17  lemma LIM_zero_iff:
1.18    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.19 -  shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
1.20 +  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
1.21  unfolding tendsto_iff dist_norm by simp
1.22
1.23  lemma metric_LIM_imp_LIM:
```