src/HOL/Limits.thy
changeset 64287 d85d88722745
parent 64272 f76b6dda2e56
child 64394 141e1ed8d5a0
     1.1 --- a/src/HOL/Limits.thy	Tue Oct 18 12:01:54 2016 +0200
     1.2 +++ b/src/HOL/Limits.thy	Tue Oct 18 15:55:53 2016 +0100
     1.3 @@ -2340,6 +2340,11 @@
     1.4  
     1.5  lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
     1.6    by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
     1.7 +  
     1.8 +lemma uniformly_continuous_imp_Cauchy_continuous:
     1.9 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    1.10 +  shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
    1.11 +  by (simp add: uniformly_continuous_on_def Cauchy_def) meson
    1.12  
    1.13  lemma (in bounded_linear) isUCont: "isUCont f"
    1.14    unfolding isUCont_def dist_norm