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
```