src/HOL/Limits.thy
changeset 63104 9505a883403c
parent 63081 5a5beb3dbe7e
child 63263 c6c95d64607a
     1.1 --- a/src/HOL/Limits.thy	Fri May 20 22:01:39 2016 +0200
     1.2 +++ b/src/HOL/Limits.thy	Fri May 20 21:21:28 2016 +0200
     1.3 @@ -2131,21 +2131,39 @@
     1.4  
     1.5  subsection \<open>Uniform Continuity\<close>
     1.6  
     1.7 -definition
     1.8 -  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
     1.9 -  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    1.10 +lemma uniformly_continuous_on_def:
    1.11 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    1.12 +  shows "uniformly_continuous_on s f \<longleftrightarrow>
    1.13 +    (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
    1.14 +  unfolding uniformly_continuous_on_uniformity
    1.15 +    uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
    1.16 +  by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric)
    1.17 +
    1.18 +abbreviation isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
    1.19 +  "isUCont f \<equiv> uniformly_continuous_on UNIV f"
    1.20 +
    1.21 +lemma isUCont_def: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    1.22 +  by (auto simp: uniformly_continuous_on_def dist_commute)
    1.23  
    1.24  lemma isUCont_isCont: "isUCont f ==> isCont f x"
    1.25 -by (simp add: isUCont_def isCont_def LIM_def, force)
    1.26 +  by (drule uniformly_continuous_imp_continuous) (simp add: continuous_on_eq_continuous_at)
    1.27 +
    1.28 +lemma uniformly_continuous_on_Cauchy:
    1.29 +  fixes f::"'a::metric_space \<Rightarrow> 'b::metric_space"
    1.30 +  assumes "uniformly_continuous_on S f" "Cauchy X" "\<And>n. X n \<in> S"
    1.31 +  shows "Cauchy (\<lambda>n. f (X n))"
    1.32 +  using assms
    1.33 +  unfolding uniformly_continuous_on_def
    1.34 +  apply -
    1.35 +  apply (rule metric_CauchyI)
    1.36 +  apply (drule_tac x=e in spec, safe)
    1.37 +  apply (drule_tac e=d in metric_CauchyD, safe)
    1.38 +  apply (rule_tac x=M in exI, simp)
    1.39 +  done
    1.40  
    1.41  lemma isUCont_Cauchy:
    1.42    "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
    1.43 -unfolding isUCont_def
    1.44 -apply (rule metric_CauchyI)
    1.45 -apply (drule_tac x=e in spec, safe)
    1.46 -apply (drule_tac e=s in metric_CauchyD, safe)
    1.47 -apply (rule_tac x=M in exI, simp)
    1.48 -done
    1.49 +  by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
    1.50  
    1.51  lemma (in bounded_linear) isUCont: "isUCont f"
    1.52  unfolding isUCont_def dist_norm