src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
changeset 62101 26c0a70f78a3
parent 61969 e01015e49041
child 62343 24106dc44def
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -36,14 +36,18 @@
     1.4    using Rep_bcontfun[of x]
     1.5    by (auto simp: bcontfun_def intro: continuous_on_subset)
     1.6  
     1.7 +(* TODO: Generalize to uniform spaces? *)
     1.8  instantiation bcontfun :: (topological_space, metric_space) metric_space
     1.9  begin
    1.10  
    1.11  definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
    1.12    where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
    1.13  
    1.14 +definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
    1.15 +  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.16 +
    1.17  definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
    1.18 -  where "open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    1.19 +  where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    1.20  
    1.21  lemma dist_bounded:
    1.22    fixes f :: "('a, 'b) bcontfun"
    1.23 @@ -126,7 +130,7 @@
    1.24      finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
    1.25        by simp
    1.26    qed
    1.27 -qed (simp add: open_bcontfun_def)
    1.28 +qed (rule open_bcontfun_def uniformity_bcontfun_def)+
    1.29  
    1.30  end
    1.31