6084 by (meson dist_commute_lessI dist_triangle_lt add_strict_mono) |
6084 by (meson dist_commute_lessI dist_triangle_lt add_strict_mono) |
6085 then show "dist (f y) (f x) < e" by simp |
6085 then show "dist (f y) (f x) < e" by simp |
6086 qed |
6086 qed |
6087 qed |
6087 qed |
6088 |
6088 |
|
6089 lemma uniformly_continuous_on_extension_at_closure: |
|
6090 fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space" |
|
6091 assumes uc: "uniformly_continuous_on X f" |
|
6092 assumes "x \<in> closure X" |
|
6093 obtains l where "(f \<longlongrightarrow> l) (at x within X)" |
|
6094 proof - |
|
6095 from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" |
|
6096 by (auto simp: closure_sequential) |
|
6097 |
|
6098 from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs] |
|
6099 obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l" |
|
6100 by atomize_elim (simp only: convergent_eq_cauchy) |
|
6101 |
|
6102 have "(f \<longlongrightarrow> l) (at x within X)" |
|
6103 proof (safe intro!: Lim_within_LIMSEQ) |
|
6104 fix xs' |
|
6105 assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X" |
|
6106 and xs': "xs' \<longlonglongrightarrow> x" |
|
6107 then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto |
|
6108 |
|
6109 from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>] |
|
6110 obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'" |
|
6111 by atomize_elim (simp only: convergent_eq_cauchy) |
|
6112 |
|
6113 show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l" |
|
6114 proof (rule tendstoI) |
|
6115 fix e::real assume "e > 0" |
|
6116 define e' where "e' \<equiv> e / 2" |
|
6117 have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def) |
|
6118 |
|
6119 have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'" |
|
6120 by (simp add: \<open>0 < e'\<close> l tendstoD) |
|
6121 moreover |
|
6122 from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>] |
|
6123 obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'" |
|
6124 by auto |
|
6125 have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d" |
|
6126 by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs') |
|
6127 ultimately |
|
6128 show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e" |
|
6129 proof eventually_elim |
|
6130 case (elim n) |
|
6131 have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l" |
|
6132 by (metis dist_triangle dist_commute) |
|
6133 also have "dist (f (xs n)) (f (xs' n)) < e'" |
|
6134 by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim) |
|
6135 also note \<open>dist (f (xs n)) l < e'\<close> |
|
6136 also have "e' + e' = e" by (simp add: e'_def) |
|
6137 finally show ?case by simp |
|
6138 qed |
|
6139 qed |
|
6140 qed |
|
6141 thus ?thesis .. |
|
6142 qed |
|
6143 |
|
6144 lemma uniformly_continuous_on_extension_on_closure: |
|
6145 fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space" |
|
6146 assumes uc: "uniformly_continuous_on X f" |
|
6147 obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x" |
|
6148 "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x" |
|
6149 proof - |
|
6150 from uc have cont_f: "continuous_on X f" |
|
6151 by (simp add: uniformly_continuous_imp_continuous) |
|
6152 obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x |
|
6153 apply atomize_elim |
|
6154 apply (rule choice) |
|
6155 using uniformly_continuous_on_extension_at_closure[OF assms] |
|
6156 by metis |
|
6157 let ?g = "\<lambda>x. if x \<in> X then f x else y x" |
|
6158 |
|
6159 have "uniformly_continuous_on (closure X) ?g" |
|
6160 unfolding uniformly_continuous_on_def |
|
6161 proof safe |
|
6162 fix e::real assume "e > 0" |
|
6163 define e' where "e' \<equiv> e / 3" |
|
6164 have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def) |
|
6165 from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>] |
|
6166 obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'" |
|
6167 by auto |
|
6168 define d' where "d' = d / 3" |
|
6169 have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def) |
|
6170 show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e" |
|
6171 proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>) |
|
6172 fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'" |
|
6173 then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" |
|
6174 and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X" |
|
6175 by (auto simp: closure_sequential) |
|
6176 have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'" |
|
6177 and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'" |
|
6178 by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs') |
|
6179 moreover |
|
6180 have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x |
|
6181 using that not_eventuallyD |
|
6182 by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at) |
|
6183 then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x" |
|
6184 using x x' |
|
6185 by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs) |
|
6186 then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'" |
|
6187 "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'" |
|
6188 by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros) |
|
6189 ultimately |
|
6190 have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e" |
|
6191 proof eventually_elim |
|
6192 case (elim n) |
|
6193 have "dist (?g x') (?g x) \<le> |
|
6194 dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)" |
|
6195 by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le) |
|
6196 also |
|
6197 { |
|
6198 have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x" |
|
6199 by (metis add.commute add_le_cancel_left dist_triangle dist_triangle_le) |
|
6200 also note \<open>dist (xs' n) x' < d'\<close> |
|
6201 also note \<open>dist x' x < d'\<close> |
|
6202 also note \<open>dist (xs n) x < d'\<close> |
|
6203 finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def) |
|
6204 } |
|
6205 with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'" |
|
6206 by (rule d) |
|
6207 also note \<open>dist (f (xs' n)) (?g x') < e'\<close> |
|
6208 also note \<open>dist (f (xs n)) (?g x) < e'\<close> |
|
6209 finally show ?case by (simp add: e'_def) |
|
6210 qed |
|
6211 then show "dist (?g x') (?g x) < e" by simp |
|
6212 qed |
|
6213 qed |
|
6214 moreover have "f x = ?g x" if "x \<in> X" for x using that by simp |
|
6215 moreover |
|
6216 { |
|
6217 fix Y h x |
|
6218 assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h" |
|
6219 and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)" |
|
6220 { |
|
6221 assume "x \<notin> X" |
|
6222 have "x \<in> closure X" using Y by auto |
|
6223 then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" |
|
6224 by (auto simp: closure_sequential) |
|
6225 from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y |
|
6226 have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x" |
|
6227 by (auto simp: set_mp extension) |
|
6228 moreover |
|
6229 then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" |
|
6230 using \<open>x \<notin> X\<close> not_eventuallyD xs(2) |
|
6231 by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs) |
|
6232 ultimately have "h x = y x" by (rule LIMSEQ_unique) |
|
6233 } then |
|
6234 have "h x = ?g x" |
|
6235 using extension by auto |
|
6236 } |
|
6237 ultimately show ?thesis .. |
|
6238 qed |
|
6239 |
|
6240 |
6089 subsection\<open>Quotient maps\<close> |
6241 subsection\<open>Quotient maps\<close> |
6090 |
6242 |
6091 lemma quotient_map_imp_continuous_open: |
6243 lemma quotient_map_imp_continuous_open: |
6092 assumes t: "f ` s \<subseteq> t" |
6244 assumes t: "f ` s \<subseteq> t" |
6093 and ope: "\<And>u. u \<subseteq> t |
6245 and ope: "\<And>u. u \<subseteq> t |