author immler Wed Feb 13 16:35:07 2013 +0100 (2013-02-13) changeset 51102 358b27c56469 parent 51096 60e4b75fefe1 child 51103 5dd7b89a16de
generalized
```     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"
```