src/HOL/Topological_Spaces.thy
 changeset 62101 26c0a70f78a3 parent 62083 7582b39f51ed child 62102 877463945ce9
```     1.1 --- a/src/HOL/Topological_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
1.3 @@ -11,7 +11,6 @@
1.4
1.5  named_theorems continuous_intros "structural introduction rules for continuity"
1.6
1.7 -
1.8  subsection \<open>Topological space\<close>
1.9
1.10  class "open" =
1.11 @@ -693,8 +692,6 @@
1.12    by (rule tendsto_le [OF F tendsto_const x a])
1.13
1.14
1.15 -
1.16 -
1.17  subsubsection \<open>Rules about @{const Lim}\<close>
1.18
1.19  lemma tendsto_Lim:
1.20 @@ -2435,4 +2432,173 @@
1.21    qed
1.22  qed (intro cSUP_least \<open>antimono f\<close>[THEN antimonoD] cInf_lower S)
1.23
1.24 +subsection \<open>Uniform spaces\<close>
1.25 +
1.26 +class uniformity =
1.27 +  fixes uniformity :: "('a \<times> 'a) filter"
1.28 +begin
1.29 +
1.30 +abbreviation uniformity_on :: "'a set \<Rightarrow> ('a \<times> 'a) filter" where
1.31 +  "uniformity_on s \<equiv> inf uniformity (principal (s\<times>s))"
1.32 +
1.33  end
1.34 +
1.35 +class open_uniformity = "open" + uniformity +
1.36 +  assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
1.37 +
1.38 +class uniform_space = open_uniformity +
1.39 +  assumes uniformity_refl: "eventually E uniformity \<Longrightarrow> E (x, x)"
1.40 +  assumes uniformity_sym: "eventually E uniformity \<Longrightarrow> eventually (\<lambda>(x, y). E (y, x)) uniformity"
1.41 +  assumes uniformity_trans: "eventually E uniformity \<Longrightarrow> \<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
1.42 +begin
1.43 +
1.44 +subclass topological_space
1.45 +  proof qed (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
1.46 +
1.47 +lemma uniformity_bot: "uniformity \<noteq> bot"
1.48 +  using uniformity_refl by auto
1.49 +
1.50 +lemma uniformity_trans':
1.51 +  "eventually E uniformity \<Longrightarrow> eventually (\<lambda>((x, y), (y', z)). y = y' \<longrightarrow> E (x, z)) (uniformity \<times>\<^sub>F uniformity)"
1.52 +  by (drule uniformity_trans) (auto simp add: eventually_prod_same)
1.53 +
1.54 +lemma uniformity_transE:
1.55 +  assumes E: "eventually E uniformity"
1.56 +  obtains D where "eventually D uniformity" "\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)"
1.57 +  using uniformity_trans[OF E] by auto
1.58 +
1.59 +lemma eventually_nhds_uniformity:
1.60 +  "eventually P (nhds x) \<longleftrightarrow> eventually (\<lambda>(x', y). x' = x \<longrightarrow> P y) uniformity" (is "_ \<longleftrightarrow> ?N P x")
1.61 +  unfolding eventually_nhds
1.62 +proof safe
1.63 +  assume *: "?N P x"
1.64 +  { fix x assume "?N P x"
1.65 +    then guess D by (rule uniformity_transE) note D = this
1.66 +    from D(1) have "?N (?N P) x"
1.67 +      by eventually_elim (insert D, force elim: eventually_mono split: prod.split) }
1.68 +  then have "open {x. ?N P x}"
1.69 +    by (simp add: open_uniformity)
1.70 +  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x\<in>S. P x)"
1.71 +    by (intro exI[of _ "{x. ?N P x}"]) (auto dest: uniformity_refl simp: *)
1.72 +qed (force simp add: open_uniformity elim: eventually_mono)
1.73 +
1.74 +subsubsection \<open>Totally bounded sets\<close>
1.75 +
1.76 +definition totally_bounded :: "'a set \<Rightarrow> bool" where
1.77 +  "totally_bounded S \<longleftrightarrow>
1.78 +    (\<forall>E. eventually E uniformity \<longrightarrow> (\<exists>X. finite X \<and> (\<forall>s\<in>S. \<exists>x\<in>X. E (x, s))))"
1.79 +
1.80 +lemma totally_bounded_empty[iff]: "totally_bounded {}"
1.81 +  by (auto simp add: totally_bounded_def)
1.82 +
1.83 +lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
1.84 +  by (force simp add: totally_bounded_def)
1.85 +
1.86 +lemma totally_bounded_Union[intro]:
1.87 +  assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"
1.88 +  unfolding totally_bounded_def
1.89 +proof safe
1.90 +  fix E assume "eventually E uniformity"
1.91 +  with M obtain X where "\<forall>S\<in>M. finite (X S) \<and> (\<forall>s\<in>S. \<exists>x\<in>X S. E (x, s))"
1.92 +    by (metis totally_bounded_def)
1.93 +  with `finite M` show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
1.94 +    by (intro exI[of _ "\<Union>S\<in>M. X S"]) force
1.95 +qed
1.96 +
1.97 +subsubsection \<open>Cauchy filter\<close>
1.98 +
1.99 +definition cauchy_filter :: "'a filter \<Rightarrow> bool" where
1.100 +  "cauchy_filter F \<longleftrightarrow> F \<times>\<^sub>F F \<le> uniformity"
1.101 +
1.102 +definition Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
1.103 +  Cauchy_uniform: "Cauchy X = cauchy_filter (filtermap X sequentially)"
1.104 +
1.105 +lemma Cauchy_uniform_iff:
1.106 +  "Cauchy X \<longleftrightarrow> (\<forall>P. eventually P uniformity \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)))"
1.107 +  unfolding Cauchy_uniform cauchy_filter_def le_filter_def eventually_prod_same
1.108 +    eventually_filtermap eventually_sequentially
1.109 +proof safe
1.110 +  let ?U = "\<lambda>P. eventually P uniformity"
1.111 +  { fix P assume "?U P" "\<forall>P. ?U P \<longrightarrow> (\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
1.112 +    then obtain Q N where "\<And>n. n \<ge> N \<Longrightarrow> Q (X n)" "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> P (x, y)"
1.113 +      by metis
1.114 +    then show "\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)"
1.115 +      by blast }
1.116 +  { fix P assume "?U P" and P: "\<forall>P. ?U P \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m))"
1.117 +    then obtain Q where "?U Q" and Q: "\<And>x y z. Q (x, y) \<Longrightarrow> Q (y, z) \<Longrightarrow> P (x, z)"
1.118 +      by (auto elim: uniformity_transE)
1.119 +    then have "?U (\<lambda>x. Q x \<and> (\<lambda>(x, y). Q (y, x)) x)"
1.120 +      unfolding eventually_conj_iff by (simp add: uniformity_sym)
1.121 +    from P[rule_format, OF this]
1.122 +    obtain N where N: "\<And>n m. n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> Q (X n, X m) \<and> Q (X m, X n)"
1.123 +      by auto
1.124 +    show "\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
1.125 +    proof (safe intro!: exI[of _ "\<lambda>x. \<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)"] exI[of _ N] N)
1.126 +      fix x y assume "\<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)" "\<forall>n\<ge>N. Q (y, X n) \<and> Q (X n, y)"
1.127 +      then have "Q (x, X N)" "Q (X N, y)" by auto
1.128 +      then show "P (x, y)"
1.129 +        by (rule Q)
1.130 +    qed }
1.131 +qed
1.132 +
1.133 +lemma nhds_imp_cauchy_filter:
1.134 +  assumes *: "F \<le> nhds x" shows "cauchy_filter F"
1.135 +proof -
1.136 +  have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
1.137 +    by (intro prod_filter_mono *)
1.138 +  also have "\<dots> \<le> uniformity"
1.139 +    unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
1.140 +  proof safe
1.141 +    fix P assume "eventually P uniformity"
1.142 +    then guess Ql by (rule uniformity_transE) note Ql = this
1.143 +    moreover note Ql(1)[THEN uniformity_sym]
1.144 +    ultimately show "\<exists>Q. eventually (\<lambda>(x', y). x' = x \<longrightarrow> Q y) uniformity \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
1.145 +      by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
1.146 +  qed
1.147 +  finally show ?thesis
1.148 +    by (simp add: cauchy_filter_def)
1.149 +qed
1.150 +
1.151 +lemma LIMSEQ_imp_Cauchy: "X \<longlonglongrightarrow> x \<Longrightarrow> Cauchy X"
1.152 +  unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
1.153 +
1.154 +lemma Cauchy_subseq_Cauchy: assumes "Cauchy X" "subseq f" shows "Cauchy (X \<circ> f)"
1.155 +  unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
1.156 +  by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
1.157 +     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
1.158 +
1.159 +lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
1.160 +  unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)
1.161 +
1.162 +definition complete :: "'a set \<Rightarrow> bool" where
1.163 +  complete_uniform: "complete S \<longleftrightarrow> (\<forall>F \<le> principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x))"
1.164 +
1.165 +end
1.166 +
1.167 +subsubsection \<open>Uniformly continuous functions\<close>
1.168 +
1.169 +definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool" where
1.170 +  uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow>
1.171 +    (LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
1.172 +
1.173 +lemma uniformly_continuous_onD:
1.174 +  "uniformly_continuous_on s f \<Longrightarrow> eventually E uniformity
1.175 +    \<Longrightarrow> eventually (\<lambda>(x, y). x \<in> s \<longrightarrow> y \<in> s \<longrightarrow> E (f x, f y)) uniformity"
1.176 +  by (simp add: uniformly_continuous_on_uniformity filterlim_iff eventually_inf_principal split_beta' mem_Times_iff imp_conjL)
1.177 +
1.178 +lemma uniformly_continuous_on_const[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. c)"
1.179 +  by (auto simp: uniformly_continuous_on_uniformity filterlim_iff uniformity_refl)
1.180 +
1.181 +lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
1.182 +  by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
1.183 +
1.184 +lemma uniformly_continuous_on_compose[continuous_intros]:
1.185 +  "uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f (g x))"
1.186 +  using filterlim_compose[of "\<lambda>(x, y). (f x, f y)" uniformity "uniformity_on (g`s)"  "\<lambda>(x, y). (g x, g y)" "uniformity_on s"]
1.187 +  by (simp add: split_beta' uniformly_continuous_on_uniformity filterlim_inf filterlim_principal eventually_inf_principal mem_Times_iff)
1.188 +
1.189 +lemma uniformly_continuous_imp_continuous: assumes f: "uniformly_continuous_on s f" shows "continuous_on s f"
1.190 +  by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
1.191 +           elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
1.192 +
1.193 +end
```