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"