generalized
authorimmler
Wed Feb 13 16:35:07 2013 +0100 (2013-02-13)
changeset 51102358b27c56469
parent 51096 60e4b75fefe1
child 51103 5dd7b89a16de
generalized
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 13 16:35:07 2013 +0100
     1.3 @@ -3704,7 +3704,7 @@
     1.4  
     1.5  text{* Cauchy-type criteria for uniform convergence. *}
     1.6  
     1.7 -lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::heine_borel" shows
     1.8 +lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space" shows
     1.9   "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
    1.10    (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs")
    1.11  proof(rule)
    1.12 @@ -3738,7 +3738,7 @@
    1.13  qed
    1.14  
    1.15  lemma uniformly_cauchy_imp_uniformly_convergent:
    1.16 -  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::heine_borel"
    1.17 +  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
    1.18    assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
    1.19            "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
    1.20    shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"