src/HOL/SEQ.thy
changeset 44208 1d2bf1f240ac
parent 44206 5e4a1664106e
child 44282 f0de18b62d63
     1.1 --- a/src/HOL/SEQ.thy	Sun Aug 14 11:44:12 2011 -0700
     1.2 +++ b/src/HOL/SEQ.thy	Sun Aug 14 13:04:57 2011 -0700
     1.3 @@ -691,9 +691,13 @@
     1.4  apply (blast intro: seq_suble le_trans dest!: spec) 
     1.5  done
     1.6  
     1.7 +lemma convergent_subseq_convergent:
     1.8 +  "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
     1.9 +  unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
    1.10 +
    1.11 +
    1.12  subsection {* Bounded Monotonic Sequences *}
    1.13  
    1.14 -
    1.15  text{*Bounded Sequence*}
    1.16  
    1.17  lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
    1.18 @@ -1007,11 +1011,6 @@
    1.19    shows "Cauchy X = convergent X"
    1.20  by (fast intro: Cauchy_convergent convergent_Cauchy)
    1.21  
    1.22 -lemma convergent_subseq_convergent:
    1.23 -  fixes X :: "nat \<Rightarrow> 'a::complete_space"
    1.24 -  shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
    1.25 -  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
    1.26 -
    1.27  text {*
    1.28  Proof that Cauchy sequences converge based on the one from
    1.29  http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html