--- a/src/HOL/SEQ.thy Sun Aug 14 11:44:12 2011 -0700
+++ b/src/HOL/SEQ.thy Sun Aug 14 13:04:57 2011 -0700
@@ -691,9 +691,13 @@
apply (blast intro: seq_suble le_trans dest!: spec)
done
+lemma convergent_subseq_convergent:
+ "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
+ unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
+
+
subsection {* Bounded Monotonic Sequences *}
-
text{*Bounded Sequence*}
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
@@ -1007,11 +1011,6 @@
shows "Cauchy X = convergent X"
by (fast intro: Cauchy_convergent convergent_Cauchy)
-lemma convergent_subseq_convergent:
- fixes X :: "nat \<Rightarrow> 'a::complete_space"
- shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
- by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
-
text {*
Proof that Cauchy sequences converge based on the one from
http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html