# HG changeset patch # User immler # Date 1360769707 -3600 # Node ID 358b27c56469837cc784ff881ad21ecbb6498f32 # Parent 60e4b75fefe1cf090aa78697f40cae556eaaae01 generalized diff -r 60e4b75fefe1 -r 358b27c56469 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 13 13:38:52 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Feb 13 16:35:07 2013 +0100 @@ -3704,7 +3704,7 @@ text{* Cauchy-type criteria for uniform convergence. *} -lemma uniformly_convergent_eq_cauchy: fixes s::"nat \ 'b \ 'a::heine_borel" shows +lemma uniformly_convergent_eq_cauchy: fixes s::"nat \ 'b \ 'a::complete_space" shows "(\l. \e>0. \N. \n x. N \ n \ P x --> dist(s n x)(l x) < e) \ (\e>0. \N. \m n x. N \ m \ N \ n \ P x --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs") proof(rule) @@ -3738,7 +3738,7 @@ qed lemma uniformly_cauchy_imp_uniformly_convergent: - fixes s :: "nat \ 'a \ 'b::heine_borel" + fixes s :: "nat \ 'a \ 'b::complete_space" assumes "\e>0.\N. \m (n::nat) x. N \ m \ N \ n \ P x --> dist(s m x)(s n x) < e" "\x. P x --> (\e>0. \N. \n. N \ n --> dist(s n x)(l x) < e)" shows "\e>0. \N. \n x. N \ n \ P x --> dist(s n x)(l x) < e"