src/HOL/Lim.thy
 changeset 44251 d101ed3177b6 parent 44233 aa74ce315bae child 44253 c073a0bd8458
```     1.1 --- a/src/HOL/Lim.thy	Wed Aug 17 09:59:10 2011 -0700
1.2 +++ b/src/HOL/Lim.thy	Wed Aug 17 11:06:39 2011 -0700
1.3 @@ -132,12 +132,8 @@
1.4    assumes f: "f -- a --> l"
1.5    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
1.6    shows "g -- a --> m"
1.7 -apply (rule tendstoI, drule tendstoD [OF f])
1.8 -apply (simp add: eventually_at_topological, safe)
1.9 -apply (rule_tac x="S" in exI, safe)
1.10 -apply (drule_tac x="x" in bspec, safe)
1.11 -apply (erule (1) order_le_less_trans [OF le])
1.12 -done
1.13 +  by (rule metric_tendsto_imp_tendsto [OF f],
1.14 +    auto simp add: eventually_at_topological le)
1.15
1.16  lemma LIM_imp_LIM:
1.17    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.18 @@ -145,9 +141,8 @@
1.19    assumes f: "f -- a --> l"
1.20    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
1.21    shows "g -- a --> m"
1.22 -apply (rule metric_LIM_imp_LIM [OF f])
1.23 -apply (simp add: dist_norm le)
1.24 -done
1.25 +  by (rule metric_LIM_imp_LIM [OF f],
1.26 +    simp add: dist_norm le)
1.27
1.28  lemma LIM_norm:
1.29    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
```