--- a/src/HOL/SEQ.thy Mon Feb 22 20:08:10 2010 +0100
+++ b/src/HOL/SEQ.thy Mon Feb 22 20:41:49 2010 +0100
@@ -435,7 +435,7 @@
lemma LIMSEQ_diff_approach_zero2:
fixes L :: "'a::real_normed_vector"
- shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L";
+ shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
by (drule (1) LIMSEQ_diff, simp)
text{*A sequence tends to zero iff its abs does*}
@@ -1047,6 +1047,17 @@
shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
unfolding Cauchy_def dist_norm ..
+lemma Cauchy_iff2:
+ "Cauchy X =
+ (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
+apply (simp add: Cauchy_iff, auto)
+apply (drule reals_Archimedean, safe)
+apply (drule_tac x = n in spec, auto)
+apply (rule_tac x = M in exI, auto)
+apply (drule_tac x = m in spec, simp)
+apply (drule_tac x = na in spec, auto)
+done
+
lemma CauchyI:
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
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"