src/HOL/SEQ.thy
 changeset 35292 e4a431b6d9b7 parent 35216 7641e8d831d2 child 35748 5f35613d9a65
```     1.1 --- a/src/HOL/SEQ.thy	Mon Feb 22 20:08:10 2010 +0100
1.2 +++ b/src/HOL/SEQ.thy	Mon Feb 22 20:41:49 2010 +0100
1.3 @@ -435,7 +435,7 @@
1.4
1.5  lemma LIMSEQ_diff_approach_zero2:
1.6    fixes L :: "'a::real_normed_vector"
1.7 -  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L";
1.8 +  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
1.9  by (drule (1) LIMSEQ_diff, simp)
1.10
1.11  text{*A sequence tends to zero iff its abs does*}
1.12 @@ -1047,6 +1047,17 @@
1.13    shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
1.14  unfolding Cauchy_def dist_norm ..
1.15
1.16 +lemma Cauchy_iff2:
1.17 +     "Cauchy X =
1.18 +      (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
1.19 +apply (simp add: Cauchy_iff, auto)
1.20 +apply (drule reals_Archimedean, safe)
1.21 +apply (drule_tac x = n in spec, auto)
1.22 +apply (rule_tac x = M in exI, auto)
1.23 +apply (drule_tac x = m in spec, simp)
1.24 +apply (drule_tac x = na in spec, auto)
1.25 +done
1.26 +
1.27  lemma CauchyI:
1.28    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
1.29    shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
```