author huffman Tue Jun 02 23:06:05 2009 -0700 (2009-06-02) changeset 31403 0baaad47cef2 parent 31402 e37967787a4f child 31404 05d2eddc5d41
class complete_space
 src/HOL/SEQ.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/SEQ.thy	Tue Jun 02 22:35:56 2009 -0700
1.2 +++ b/src/HOL/SEQ.thy	Tue Jun 02 23:06:05 2009 -0700
1.3 @@ -1034,9 +1034,11 @@
1.4
1.5  subsubsection {* Cauchy Sequences are Convergent *}
1.6
1.7 -axclass banach \<subseteq> real_normed_vector
1.8 +axclass complete_space \<subseteq> metric_space
1.9    Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
1.10
1.11 +axclass banach \<subseteq> real_normed_vector, complete_space
1.12 +
1.13  theorem LIMSEQ_imp_Cauchy:
1.14    assumes X: "X ----> a" shows "Cauchy X"
1.15  proof (rule metric_CauchyI)
1.16 @@ -1061,6 +1063,16 @@
1.17  unfolding convergent_def
1.18  by (erule exE, erule LIMSEQ_imp_Cauchy)
1.19
1.20 +lemma Cauchy_convergent_iff:
1.21 +  fixes X :: "nat \<Rightarrow> 'a::complete_space"
1.22 +  shows "Cauchy X = convergent X"
1.23 +by (fast intro: Cauchy_convergent convergent_Cauchy)
1.24 +
1.25 +lemma convergent_subseq_convergent:
1.26 +  fixes X :: "nat \<Rightarrow> 'a::complete_space"
1.27 +  shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
1.28 +  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
1.29 +
1.30  text {*
1.31  Proof that Cauchy sequences converge based on the one from
1.32  http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
1.33 @@ -1174,16 +1186,6 @@
1.34  instance real :: banach
1.35  by intro_classes (rule real_Cauchy_convergent)
1.36
1.37 -lemma Cauchy_convergent_iff:
1.38 -  fixes X :: "nat \<Rightarrow> 'a::banach"
1.39 -  shows "Cauchy X = convergent X"
1.40 -by (fast intro: Cauchy_convergent convergent_Cauchy)
1.41 -
1.42 -lemma convergent_subseq_convergent:
1.43 -  fixes X :: "nat \<Rightarrow> 'a::banach"
1.44 -  shows "\<lbrakk> convergent X; subseq f \<rbrakk> \<Longrightarrow> convergent (X o f)"
1.45 -  by (simp add: Cauchy_subseq_Cauchy Cauchy_convergent_iff [symmetric])
1.46 -
1.47
1.48  subsection {* Power Sequences *}
1.49
```