class complete_space
authorhuffman
Tue Jun 02 23:06:05 2009 -0700 (2009-06-02)
changeset 314030baaad47cef2
parent 31402 e37967787a4f
child 31404 05d2eddc5d41
class complete_space
src/HOL/SEQ.thy
     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