(* Title: HOL/Analysis/Urysohn.thy Authors: LC Paulson, based on material from HOL Light *) section ‹The Urysohn lemma, its consequences and other advanced material about metric spaces› theory Urysohn imports Abstract_Topological_Spaces Abstract_Metric_Spaces Infinite_Sum Arcwise_Connected begin subsection ‹Urysohn lemma and Tietze's theorem› proposition Urysohn_lemma: fixes a b :: real assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T" "a ≤ b" obtains f where "continuous_map X (top_of_set {a..b}) f" "f ` S ⊆ {a}" "f ` T ⊆ {b}" proof - obtain U where "openin X U" "S ⊆ U" "X closure_of U ⊆ topspace X - T" using assms unfolding normal_space_alt disjnt_def by (metis Diff_mono Un_Diff_Int closedin_def subset_eq sup_bot_right) have "∃G :: real ⇒ 'a set. G 0 = U ∧ G 1 = topspace X - T ∧ (∀x ∈ dyadics ∩ {0..1}. ∀y ∈ dyadics ∩ {0..1}. x < y ⟶ openin X (G x) ∧ openin X (G y) ∧ X closure_of (G x) ⊆ G y)" proof (rule recursion_on_dyadic_fractions) show "openin X U ∧ openin X (topspace X - T) ∧ X closure_of U ⊆ topspace X - T" using ‹X closure_of U ⊆ topspace X - T› ‹openin X U› ‹closedin X T› by blast show "∃z. (openin X x ∧ openin X z ∧ X closure_of x ⊆ z) ∧ openin X z ∧ openin X y ∧ X closure_of z ⊆ y" if "openin X x ∧ openin X y ∧ X closure_of x ⊆ y" for x y by (meson that closedin_closure_of normal_space_alt ‹normal_space X›) show "openin X x ∧ openin X z ∧ X closure_of x ⊆ z" if "openin X x ∧ openin X y ∧ X closure_of x ⊆ y" and "openin X y ∧ openin X z ∧ X closure_of y ⊆ z" for x y z by (meson that closure_of_subset openin_subset subset_trans) qed then obtain G :: "real ⇒ 'a set" where G0: "G 0 = U" and G1: "G 1 = topspace X - T" and G: "⋀x y. ⟦x ∈ dyadics; y ∈ dyadics; 0 ≤ x; x < y; y ≤ 1⟧ ⟹ openin X (G x) ∧ openin X (G y) ∧ X closure_of (G x) ⊆ G y" by (smt (verit, del_insts) Int_iff atLeastAtMost_iff) define f where "f ≡ λx. Inf(insert 1 {r. r ∈ dyadics ∩ {0..1} ∧ x ∈ G r})" have f_ge: "f x ≥ 0" if "x ∈ topspace X" for x unfolding f_def by (force intro: cInf_greatest) moreover have f_le1: "f x ≤ 1" if "x ∈ topspace X" for x proof - have "bdd_below {r ∈ dyadics ∩ {0..1}. x ∈ G r}" by (auto simp: bdd_below_def) then show ?thesis by (auto simp: f_def cInf_lower) qed ultimately have fim: "f ` topspace X ⊆ {0..1}" by (auto simp: f_def) have 0: "0 ∈ dyadics ∩ {0..1::real}" and 1: "1 ∈ dyadics ∩ {0..1::real}" by (force simp: dyadics_def)+ then have opeG: "openin X (G r)" if "r ∈ dyadics ∩ {0..1}" for r using G G0 ‹openin X U› less_eq_real_def that by auto have "x ∈ G 0" if "x ∈ S" for x using G0 ‹S ⊆ U› that by blast with 0 have fimS: "f ` S ⊆ {0}" unfolding f_def by (force intro!: cInf_eq_minimum) have False if "r ∈ dyadics" "0 ≤ r" "r < 1" "x ∈ G r" "x ∈ T" for r x using G [of r 1] 1 by (smt (verit, best) DiffD2 G1 Int_iff closure_of_subset inf.orderE openin_subset that) then have "r≥1" if "r ∈ dyadics" "0 ≤ r" "r ≤ 1" "x ∈ G r" "x ∈ T" for r x using linorder_not_le that by blast then have fimT: "f ` T ⊆ {1}" unfolding f_def by (force intro!: cInf_eq_minimum) have fle1: "f z ≤ 1" for z by (force simp: f_def intro: cInf_lower) have fle: "f z ≤ x" if "x ∈ dyadics ∩ {0..1}" "z ∈ G x" for z x using that by (force simp: f_def intro: cInf_lower) have *: "b ≤ f z" if "b ≤ 1" "⋀x. ⟦x ∈ dyadics ∩ {0..1}; z ∈ G x⟧ ⟹ b ≤ x" for z b using that by (force simp: f_def intro: cInf_greatest) have **: "r ≤ f x" if r: "r ∈ dyadics ∩ {0..1}" "x ∉ G r" for r x proof (rule *) show "r ≤ s" if "s ∈ dyadics ∩ {0..1}" and "x ∈ G s" for s :: real using that r G [of s r] by (force simp: dest: closure_of_subset openin_subset) qed (use that in force) have "∃U. openin X U ∧ x ∈ U ∧ (∀y ∈ U. ¦f y - f x¦ < ε)" if "x ∈ topspace X" and "0 < ε" for x ε proof - have A: "∃r. r ∈ dyadics ∩ {0..1} ∧ r < y ∧ ¦r - y¦ < d" if "0 < y" "y ≤ 1" "0 < d" for y d::real proof - obtain n q r where "of_nat q / 2^n < y" "y < of_nat r / 2^n" "¦q / 2^n - r / 2^n ¦ < d" by (smt (verit, del_insts) padic_rational_approximation_straddle_pos ‹0 < d› ‹0 < y›) then show ?thesis unfolding dyadics_def using divide_eq_0_iff that(2) by fastforce qed have B: "∃r. r ∈ dyadics ∩ {0..1} ∧ y < r ∧ ¦r - y¦ < d" if "0 ≤ y" "y < 1" "0 < d" for y d::real proof - obtain n q r where "of_nat q / 2^n ≤ y" "y < of_nat r / 2^n" "¦q / 2^n - r / 2^n ¦ < d" using padic_rational_approximation_straddle_pos_le by (smt (verit, del_insts) ‹0 < d› ‹0 ≤ y›) then show ?thesis apply (clarsimp simp: dyadics_def) using divide_eq_0_iff ‹y < 1› by (smt (verit) divide_nonneg_nonneg divide_self of_nat_0_le_iff of_nat_1 power_0 zero_le_power) qed show ?thesis proof (cases "f x = 0") case True with B[of 0] obtain r where r: "r ∈ dyadics ∩ {0..1}" "0 < r" "¦r¦ < ε/2" by (smt (verit) ‹0 < ε› half_gt_zero) show ?thesis proof (intro exI conjI) show "openin X (G r)" using opeG r(1) by blast show "x ∈ G r" using True ** r by force show "∀y ∈ G r. ¦f y - f x¦ < ε" using f_ge ‹openin X (G r)› fle openin_subset r by (fastforce simp: True) qed next case False show ?thesis proof (cases "f x = 1") case True with A[of 1] obtain r where r: "r ∈ dyadics ∩ {0..1}" "r < 1" "¦r-1¦ < ε/2" by (smt (verit) ‹0 < ε› half_gt_zero) define G' where "G' ≡ topspace X - X closure_of G r" show ?thesis proof (intro exI conjI) show "openin X G'" unfolding G'_def by fastforce obtain r' where "r' ∈ dyadics ∧ 0 ≤ r' ∧ r' ≤ 1 ∧ r < r' ∧ ¦r' - r¦ < 1 - r" using B r by force moreover have "1 - r ∈ dyadics" "0 ≤ r" using 1 r dyadics_diff by force+ ultimately have "x ∉ X closure_of G r" using G True r fle by force then show "x ∈ G'" by (simp add: G'_def that) show "∀y ∈ G'. ¦f y - f x¦ < ε" using ** f_le1 in_closure_of r by (fastforce simp: True G'_def) qed next case False have "0 < f x" "f x < 1" using fle1 f_ge that(1) ‹f x ≠ 0› ‹f x ≠ 1› by (metis order_le_less) + obtain r where r: "r ∈ dyadics ∩ {0..1}" "r < f x" "¦r - f x¦ < ε / 2" using A ‹0 < ε› ‹0 < f x› ‹f x < 1› by (smt (verit, best) half_gt_zero) obtain r' where r': "r' ∈ dyadics ∩ {0..1}" "f x < r'" "¦r' - f x¦ < ε / 2" using B ‹0 < ε› ‹0 < f x› ‹f x < 1› by (smt (verit, best) half_gt_zero) have "r < 1" using ‹f x < 1› r(2) by force show ?thesis proof (intro conjI exI) show "openin X (G r' - X closure_of G r)" using closedin_closure_of opeG r' by blast have "x ∈ X closure_of G r ⟹ False" using B [of r "f x - r"] r ‹r < 1› G [of r] fle by force then show "x ∈ G r' - X closure_of G r" using ** r' by fastforce show "∀y∈G r' - X closure_of G r. ¦f y - f x¦ < ε" using r r' ** G closure_of_subset field_sum_of_halves fle openin_subset subset_eq by (smt (verit) DiffE opeG) qed qed qed qed then have contf: "continuous_map X (top_of_set {0..1}) f" by (force simp: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: mtopology_is_euclidean) define g where "g ≡ λx. a + (b - a) * f x" show thesis proof have "continuous_map X euclideanreal g" using contf ‹a ≤ b› unfolding g_def by (auto simp: continuous_intros continuous_map_in_subtopology) moreover have "g ` (topspace X) ⊆ {a..b}" using mult_left_le [of "f _" "b-a"] contf ‹a ≤ b› by (simp add: g_def add.commute continuous_map_in_subtopology image_subset_iff le_diff_eq) ultimately show "continuous_map X (top_of_set {a..b}) g" by (meson continuous_map_in_subtopology) show "g ` S ⊆ {a}" "g ` T ⊆ {b}" using fimS fimT by (auto simp: g_def) qed qed lemma Urysohn_lemma_alt: fixes a b :: real assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T" obtains f where "continuous_map X euclideanreal f" "f ` S ⊆ {a}" "f ` T ⊆ {b}" by (metis Urysohn_lemma assms continuous_map_in_subtopology disjnt_sym linear) lemma normal_space_iff_Urysohn_gen_alt: assumes "a ≠ b" shows "normal_space X ⟷ (∀S T. closedin X S ∧ closedin X T ∧ disjnt S T ⟶ (∃f. continuous_map X euclideanreal f ∧ f ` S ⊆ {a} ∧ f ` T ⊆ {b}))" (is "?lhs=?rhs") proof show "?lhs ⟹ ?rhs" by (metis Urysohn_lemma_alt) next assume R: ?rhs show ?lhs unfolding normal_space_def proof clarify fix S T assume "closedin X S" and "closedin X T" and "disjnt S T" with R obtain f where contf: "continuous_map X euclideanreal f" and "f ` S ⊆ {a}" "f ` T ⊆ {b}" by meson show "∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" proof (intro conjI exI) show "openin X {x ∈ topspace X. f x ∈ ball a (¦a - b¦ / 2)}" by (force intro!: openin_continuous_map_preimage [OF contf]) show "openin X {x ∈ topspace X. f x ∈ ball b (¦a - b¦ / 2)}" by (force intro!: openin_continuous_map_preimage [OF contf]) show "S ⊆ {x ∈ topspace X. f x ∈ ball a (¦a - b¦ / 2)}" using ‹closedin X S› closedin_subset ‹f ` S ⊆ {a}› assms by force show "T ⊆ {x ∈ topspace X. f x ∈ ball b (¦a - b¦ / 2)}" using ‹closedin X T› closedin_subset ‹f ` T ⊆ {b}› assms by force have "⋀x. ⟦x ∈ topspace X; dist a (f x) < ¦a-b¦/2; dist b (f x) < ¦a-b¦/2⟧ ⟹ False" by (smt (verit, best) dist_real_def dist_triangle_half_l) then show "disjnt {x ∈ topspace X. f x ∈ ball a (¦a-b¦ / 2)} {x ∈ topspace X. f x ∈ ball b (¦a-b¦ / 2)}" using disjnt_iff by fastforce qed qed qed lemma normal_space_iff_Urysohn_gen: fixes a b::real shows "a < b ⟹ normal_space X ⟷ (∀S T. closedin X S ∧ closedin X T ∧ disjnt S T ⟶ (∃f. continuous_map X (top_of_set {a..b}) f ∧ f ` S ⊆ {a} ∧ f ` T ⊆ {b}))" by (metis linear not_le Urysohn_lemma normal_space_iff_Urysohn_gen_alt continuous_map_in_subtopology) lemma normal_space_iff_Urysohn_alt: "normal_space X ⟷ (∀S T. closedin X S ∧ closedin X T ∧ disjnt S T ⟶ (∃f. continuous_map X euclideanreal f ∧ f ` S ⊆ {0} ∧ f ` T ⊆ {1}))" by (rule normal_space_iff_Urysohn_gen_alt) auto lemma normal_space_iff_Urysohn: "normal_space X ⟷ (∀S T. closedin X S ∧ closedin X T ∧ disjnt S T ⟶ (∃f::'a⇒real. continuous_map X (top_of_set {0..1}) f ∧ f ` S ⊆ {0} ∧ f ` T ⊆ {1}))" by (rule normal_space_iff_Urysohn_gen) auto lemma normal_space_perfect_map_image: "⟦normal_space X; perfect_map X Y f⟧ ⟹ normal_space Y" unfolding perfect_map_def proper_map_def using normal_space_continuous_closed_map_image by fastforce lemma Hausdorff_normal_space_closed_continuous_map_image: "⟦normal_space X; closed_map X Y f; continuous_map X Y f; f ` topspace X = topspace Y; t1_space Y⟧ ⟹ Hausdorff_space Y" by (metis normal_space_continuous_closed_map_image normal_t1_imp_Hausdorff_space) lemma normal_Hausdorff_space_closed_continuous_map_image: "⟦normal_space X; Hausdorff_space X; closed_map X Y f; continuous_map X Y f; f ` topspace X = topspace Y⟧ ⟹ normal_space Y ∧ Hausdorff_space Y" by (meson normal_space_continuous_closed_map_image normal_t1_eq_Hausdorff_space t1_space_closed_map_image) lemma Lindelof_cover: assumes "regular_space X" and "Lindelof_space X" and "S ≠ {}" and clo: "closedin X S" "closedin X T" "disjnt S T" obtains h :: "nat ⇒ 'a set" where "⋀n. openin X (h n)" "⋀n. disjnt T (X closure_of (h n))" and "S ⊆ ⋃(range h)" proof - have "∃U. openin X U ∧ x ∈ U ∧ disjnt T (X closure_of U)" if "x ∈ S" for x using ‹regular_space X› unfolding regular_space by (metis (full_types) Diff_iff ‹disjnt S T› clo closure_of_eq disjnt_iff in_closure_of that) then obtain h where oh: "⋀x. x ∈ S ⟹ openin X (h x)" and xh: "⋀x. x ∈ S ⟹ x ∈ h x" and dh: "⋀x. x ∈ S ⟹ disjnt T (X closure_of h x)" by metis have "Lindelof_space(subtopology X S)" by (simp add: Lindelof_space_closedin_subtopology ‹Lindelof_space X› ‹closedin X S›) then obtain 𝒰 where 𝒰: "countable 𝒰 ∧ 𝒰 ⊆ h ` S ∧ S ⊆ ⋃𝒰" unfolding Lindelof_space_subtopology_subset [OF closedin_subset [OF ‹closedin X S›]] by (smt (verit, del_insts) oh xh UN_I image_iff subsetI) with ‹S ≠ {}› have "𝒰 ≠ {}" by blast show ?thesis proof show "openin X (from_nat_into 𝒰 n)" for n by (metis 𝒰 from_nat_into image_iff ‹𝒰 ≠ {}› oh subsetD) show "disjnt T (X closure_of (from_nat_into 𝒰) n)" for n using dh from_nat_into [OF ‹𝒰 ≠ {}›] by (metis 𝒰 f_inv_into_f inv_into_into subset_eq) show "S ⊆ ⋃(range (from_nat_into 𝒰))" by (simp add: 𝒰 ‹𝒰 ≠ {}›) qed qed lemma regular_Lindelof_imp_normal_space: assumes "regular_space X" and "Lindelof_space X" shows "normal_space X" unfolding normal_space_def proof clarify fix S T assume clo: "closedin X S" "closedin X T" and "disjnt S T" show "∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" proof (cases "S={} ∨ T={}") case True with clo show ?thesis by (meson closedin_def disjnt_empty1 disjnt_empty2 openin_empty openin_topspace subset_empty) next case False obtain h :: "nat ⇒ 'a set" where opeh: "⋀n. openin X (h n)" and dish: "⋀n. disjnt T (X closure_of (h n))" and Sh: "S ⊆ ⋃(range h)" by (metis Lindelof_cover False ‹disjnt S T› assms clo) obtain k :: "nat ⇒ 'a set" where opek: "⋀n. openin X (k n)" and disk: "⋀n. disjnt S (X closure_of (k n))" and Tk: "T ⊆ ⋃(range k)" by (metis Lindelof_cover False ‹disjnt S T› assms clo disjnt_sym) define U where "U ≡ ⋃i. h i - (⋃j<i. X closure_of k j)" define V where "V ≡ ⋃i. k i - (⋃j≤i. X closure_of h j)" show ?thesis proof (intro exI conjI) show "openin X U" "openin X V" unfolding U_def V_def by (force intro!: opek opeh closedin_Union closedin_closure_of)+ show "S ⊆ U" "T ⊆ V" using Sh Tk dish disk by (fastforce simp: U_def V_def disjnt_iff)+ have "⋀x i j. ⟦x ∈ k i; x ∈ h j; ∀j≤i. x ∉ X closure_of h j⟧ ⟹ ∃i<j. x ∈ X closure_of k i" by (metis in_closure_of linorder_not_less opek openin_subset subsetD) then show "disjnt U V" by (force simp: U_def V_def disjnt_iff) qed qed qed theorem Tietze_extension_closed_real_interval: assumes "normal_space X" and "closedin X S" and contf: "continuous_map (subtopology X S) euclideanreal f" and fim: "f ` S ⊆ {a..b}" and "a ≤ b" obtains g where "continuous_map X euclideanreal g" "⋀x. x ∈ S ⟹ g x = f x" "g ` topspace X ⊆ {a..b}" proof - define c where "c ≡ max ¦a¦ ¦b¦ + 1" have "0 < c" and c: "⋀x. x ∈ S ⟹ ¦f x¦ ≤ c" using fim by (auto simp: c_def image_subset_iff) define good where "good ≡ λg n. continuous_map X euclideanreal g ∧ (∀x ∈ S. ¦f x - g x¦ ≤ c * (2/3)^n)" have step: "∃g. good g (Suc n) ∧ (∀x ∈ topspace X. ¦g x - h x¦ ≤ c * (2/3)^n / 3)" if h: "good h n" for n h proof - have pos: "0 < c * (2/3) ^ n" by (simp add: ‹0 < c›) have S_eq: "S = topspace(subtopology X S)" and "S ⊆ topspace X" using ‹closedin X S› closedin_subset by auto define d where "d ≡ c/3 * (2/3) ^ n" define SA where "SA ≡ {x ∈ S. f x - h x ∈ {..-d}}" define SB where "SB ≡ {x ∈ S. f x - h x ∈ {d..}}" have contfh: "continuous_map (subtopology X S) euclideanreal (λx. f x - h x)" using that by (simp add: contf good_def continuous_map_diff continuous_map_from_subtopology) then have "closedin (subtopology X S) SA" unfolding SA_def by (smt (verit, del_insts) closed_closedin continuous_map_closedin Collect_cong S_eq closed_real_atMost) then have "closedin X SA" using ‹closedin X S› closedin_trans_full by blast moreover have "closedin (subtopology X S) SB" unfolding SB_def using closedin_continuous_map_preimage_gen [OF contfh] by (metis (full_types) S_eq closed_atLeast closed_closedin closedin_topspace) then have "closedin X SB" using ‹closedin X S› closedin_trans_full by blast moreover have "disjnt SA SB" using pos by (auto simp: d_def disjnt_def SA_def SB_def) moreover have "-d ≤ d" using pos by (auto simp: d_def) ultimately obtain g where contg: "continuous_map X (top_of_set {- d..d}) g" and ga: "g ` SA ⊆ {- d}" and gb: "g ` SB ⊆ {d}" using Urysohn_lemma ‹normal_space X› by metis then have g_le_d: "⋀x. x ∈ topspace X ⟹ ¦g x¦ ≤ d" by (fastforce simp: abs_le_iff continuous_map_def minus_le_iff) have g_eq_d: "⋀x. ⟦x ∈ S; f x - h x ≤ -d⟧ ⟹ g x = -d" using ga by (auto simp: SA_def) have g_eq_negd: "⋀x. ⟦x ∈ S; f x - h x ≥ d⟧ ⟹ g x = d" using gb by (auto simp: SB_def) show ?thesis unfolding good_def proof (intro conjI strip exI) show "continuous_map X euclideanreal (λx. h x + g x)" using contg continuous_map_add continuous_map_in_subtopology that unfolding good_def by blast show "¦f x - (h x + g x)¦ ≤ c * (2 / 3) ^ Suc n" if "x ∈ S" for x proof - have x: "x ∈ topspace X" using ‹S ⊆ topspace X› that by auto have "¦f x - h x¦ ≤ c * (2/3) ^ n" using good_def h that by blast with g_eq_d [OF that] g_eq_negd [OF that] g_le_d [OF x] have "¦f x - (h x + g x)¦ ≤ d + d" unfolding d_def by linarith then show ?thesis by (simp add: d_def) qed show "¦h x + g x - h x¦ ≤ c * (2 / 3) ^ n / 3" if "x ∈ topspace X" for x using that d_def g_le_d by auto qed qed then obtain nxtg where nxtg: "⋀h n. good h n ⟹ good (nxtg h n) (Suc n) ∧ (∀x ∈ topspace X. ¦nxtg h n x - h x¦ ≤ c * (2/3)^n / 3)" by metis define g where "g ≡ rec_nat (λx. 0) (λn r. nxtg r n)" have [simp]: "g 0 x = 0" for x by (auto simp: g_def) have g_Suc: "g(Suc n) = nxtg (g n) n" for n by (auto simp: g_def) have good: "good (g n) n" for n proof (induction n) case 0 with c show ?case by (auto simp: good_def) qed (simp add: g_Suc nxtg) have *: "⋀n x. x ∈ topspace X ⟹ ¦g(Suc n) x - g n x¦ ≤ c * (2/3) ^ n / 3" using nxtg g_Suc good by force obtain h where conth: "continuous_map X euclideanreal h" and h: "⋀ε. 0 < ε ⟹ ∀⇩_{F}n in sequentially. ∀x∈topspace X. dist (g n x) (h x) < ε" proof (rule Met_TC.continuous_map_uniformly_Cauchy_limit) show "∀⇩_{F}n in sequentially. continuous_map X (Met_TC.mtopology) (g n)" using good good_def by fastforce show "∃N. ∀m n x. N ≤ m ⟶ N ≤ n ⟶ x ∈ topspace X ⟶ dist (g m x) (g n x) < ε" if "ε > 0" for ε proof - have "∀⇩_{F}n in sequentially. ¦(2/3) ^ n¦ < ε/c" proof (rule Archimedean_eventually_pow_inverse) show "0 < ε / c" by (simp add: ‹0 < c› that) qed auto then obtain N where N: "⋀n. n ≥ N ⟹ ¦(2/3) ^ n¦ < ε/c" by (meson eventually_sequentially order_le_less_trans) have "¦g m x - g n x¦ < ε" if "N ≤ m" "N ≤ n" and x: "x ∈ topspace X" "m ≤ n" for m n x proof (cases "m < n") case True have 23: "(∑k = m..<n. (2/3)^k) = 3 * ((2/3) ^ m - (2/3::real) ^ n)" using ‹m ≤ n› by (induction n) (auto simp: le_Suc_eq) have "¦g m x - g n x¦ ≤ ¦∑k = m..<n. g (Suc k) x - g k x¦" by (subst sum_Suc_diff' [OF ‹m ≤ n›]) linarith also have "… ≤ (∑k = m..<n. ¦g (Suc k) x - g k x¦)" by (rule sum_abs) also have "… ≤ (∑k = m..<n. c * (2/3)^k / 3)" by (meson "*" sum_mono x(1)) also have "… = (c/3) * (∑k = m..<n. (2/3)^k)" by (simp add: sum_distrib_left) also have "… = (c/3) * 3 * ((2/3) ^ m - (2/3) ^ n)" by (simp add: sum_distrib_left 23) also have "... < (c/3) * 3 * ((2/3) ^ m)" using ‹0 < c› by auto also have "… < ε" using N [OF ‹N ≤ m›] ‹0 < c› by (simp add: field_simps) finally show ?thesis . qed (use ‹0 < ε› ‹m ≤ n› in auto) then show ?thesis by (metis dist_commute_lessI dist_real_def nle_le) qed qed auto define φ where "φ ≡ λx. max a (min (h x) b)" show thesis proof show "continuous_map X euclidean φ" unfolding φ_def using conth by (intro continuous_intros) auto show "φ x = f x" if "x ∈ S" for x proof - have x: "x ∈ topspace X" using ‹closedin X S› closedin_subset that by blast have "h x = f x" proof (rule Met_TC.limitin_metric_unique) show "limitin Met_TC.mtopology (λn. g n x) (h x) sequentially" using h x by (force simp: tendsto_iff eventually_sequentially) show "limitin Met_TC.mtopology (λn. g n x) (f x) sequentially" proof (clarsimp simp: tendsto_iff) fix ε::real assume "ε > 0" then have "∀⇩_{F}n in sequentially. ¦(2/3) ^ n¦ < ε/c" by (intro Archimedean_eventually_pow_inverse) (auto simp: ‹c > 0›) then show "∀⇩_{F}n in sequentially. dist (g n x) (f x) < ε" apply eventually_elim by (smt (verit) good x good_def ‹c > 0› dist_real_def mult.commute pos_less_divide_eq that) qed qed auto then show ?thesis using that fim by (auto simp: φ_def) qed then show "φ ` topspace X ⊆ {a..b}" using fim ‹a ≤ b› by (auto simp: φ_def) qed qed theorem Tietze_extension_realinterval: assumes XS: "normal_space X" "closedin X S" and T: "is_interval T" "T ≠ {}" and contf: "continuous_map (subtopology X S) euclideanreal f" and "f ` S ⊆ T" obtains g where "continuous_map X euclideanreal g" "g ` topspace X ⊆ T" "⋀x. x ∈ S ⟹ g x = f x" proof - define Φ where "Φ ≡ λT::real set. ∀f. continuous_map (subtopology X S) euclidean f ⟶ f`S ⊆ T ⟶ (∃g. continuous_map X euclidean g ∧ g ` topspace X ⊆ T ∧ (∀x ∈ S. g x = f x))" have "Φ T" if *: "⋀T. ⟦bounded T; is_interval T; T ≠ {}⟧ ⟹ Φ T" and "is_interval T" "T ≠ {}" for T unfolding Φ_def proof (intro strip) fix f assume contf: "continuous_map (subtopology X S) euclideanreal f" and "f ` S ⊆ T" have ΦT: "Φ ((λx. x / (1 + ¦x¦)) ` T)" proof (rule *) show "bounded ((λx. x / (1 + ¦x¦)) ` T)" using shrink_range [of T] by (force intro: boundedI [where B=1]) show "is_interval ((λx. x / (1 + ¦x¦)) ` T)" using connected_shrink that(2) is_interval_connected_1 by blast show "(λx. x / (1 + ¦x¦)) ` T ≠ {}" using ‹T ≠ {}› by auto qed moreover have "continuous_map (subtopology X S) euclidean ((λx. x / (1 + ¦x¦)) ∘ f)" by (metis contf continuous_map_compose continuous_map_into_fulltopology continuous_map_real_shrink) moreover have "((λx. x / (1 + ¦x¦)) ∘ f) ` S ⊆ (λx. x / (1 + ¦x¦)) ` T" using ‹f ` S ⊆ T› by auto ultimately obtain g where contg: "continuous_map X euclidean g" and gim: "g ` topspace X ⊆ (λx. x / (1 + ¦x¦)) ` T" and geq: "⋀x. x ∈ S ⟹ g x = ((λx. x / (1 + ¦x¦)) ∘ f) x" using ΦT unfolding Φ_def by force show "∃g. continuous_map X euclideanreal g ∧ g ` topspace X ⊆ T ∧ (∀x∈S. g x = f x)" proof (intro conjI exI) have "continuous_map X (top_of_set {-1<..<1}) g" using contg continuous_map_in_subtopology gim shrink_range by blast then show "continuous_map X euclideanreal ((λx. x / (1 - ¦x¦)) ∘ g)" by (rule continuous_map_compose) (auto simp: continuous_on_real_grow) show "((λx. x / (1 - ¦x¦)) ∘ g) ` topspace X ⊆ T" using gim real_grow_shrink by fastforce show "∀x∈S. ((λx. x / (1 - ¦x¦)) ∘ g) x = f x" using geq real_grow_shrink by force qed qed moreover have "Φ T" if "bounded T" "is_interval T" "T ≠ {}" for T unfolding Φ_def proof (intro strip) fix f assume contf: "continuous_map (subtopology X S) euclideanreal f" and "f ` S ⊆ T" obtain a b where ab: "closure T = {a..b}" by (meson ‹bounded T› ‹is_interval T› compact_closure connected_compact_interval_1 connected_imp_connected_closure is_interval_connected) with ‹T ≠ {}› have "a ≤ b" by auto have "f ` S ⊆ {a..b}" using ‹f ` S ⊆ T› ab closure_subset by auto then obtain g where contg: "continuous_map X euclideanreal g" and gf: "⋀x. x ∈ S ⟹ g x = f x" and gim: "g ` topspace X ⊆ {a..b}" using Tietze_extension_closed_real_interval [OF XS contf _ ‹a ≤ b›] by metis define W where "W ≡ {x ∈ topspace X. g x ∈ closure T - T}" have "{a..b} - {a, b} ⊆ T" using that by (metis ab atLeastAtMost_diff_ends convex_interior_closure interior_atLeastAtMost_real interior_subset is_interval_convex) with finite_imp_compact have "compact (closure T - T)" by (metis Diff_eq_empty_iff Diff_insert2 ab finite.emptyI finite_Diff_insert) then have "closedin X W" unfolding W_def using closedin_continuous_map_preimage [OF contg] compact_imp_closed by force moreover have "disjnt W S" unfolding W_def disjnt_iff using ‹f ` S ⊆ T› gf by blast ultimately obtain h :: "'a ⇒ real" where conth: "continuous_map X (top_of_set {0..1}) h" and him: "h ` W ⊆ {0}" "h ` S ⊆ {1}" by (metis XS normal_space_iff_Urysohn) then have him01: "h ` topspace X ⊆ {0..1}" by (meson continuous_map_in_subtopology) obtain z where "z ∈ T" using ‹T ≠ {}› by blast define g' where "g' ≡ λx. z + h x * (g x - z)" show "∃g. continuous_map X euclidean g ∧ g ` topspace X ⊆ T ∧ (∀x∈S. g x = f x)" proof (intro exI conjI) show "continuous_map X euclideanreal g'" unfolding g'_def using contg conth continuous_map_in_subtopology by (intro continuous_intros) auto show "g' ` topspace X ⊆ T" unfolding g'_def proof clarify fix x assume "x ∈ topspace X" show "z + h x * (g x - z) ∈ T" proof (cases "g x ∈ T") case True define w where "w ≡ z + h x * (g x - z)" have "¦h x¦ * ¦g x - z¦ ≤ ¦g x - z¦" "¦1 - h x¦ * ¦g x - z¦ ≤ ¦g x - z¦" using him01 ‹x ∈ topspace X› by (force simp: intro: mult_left_le_one_le)+ then consider "z ≤ w ∧ w ≤ g x" | "g x ≤ w ∧ w ≤ z" unfolding w_def by (smt (verit) left_diff_distrib mult_cancel_right2 mult_minus_right zero_less_mult_iff) then show ?thesis using ‹is_interval T› unfolding w_def is_interval_1 by (metis True ‹z ∈ T›) next case False then have "g x ∈ closure T" using ‹x ∈ topspace X› ab gim by blast then have "h x = 0" using him False ‹x ∈ topspace X› by (auto simp: W_def image_subset_iff) then show ?thesis by (simp add: ‹z ∈ T›) qed qed show "∀x∈S. g' x = f x" using gf him by (auto simp: W_def g'_def) qed qed ultimately show thesis using assms that unfolding Φ_def by best qed lemma normal_space_iff_Tietze: "normal_space X ⟷ (∀f S. closedin X S ∧ continuous_map (subtopology X S) euclidean f ⟶ (∃g:: 'a ⇒ real. continuous_map X euclidean g ∧ (∀x ∈ S. g x = f x)))" (is "?lhs ⟷ ?rhs") proof assume ?lhs then show ?rhs by (metis Tietze_extension_realinterval empty_not_UNIV is_interval_univ subset_UNIV) next assume R: ?rhs show ?lhs unfolding normal_space_iff_Urysohn_alt proof clarify fix S T assume "closedin X S" and "closedin X T" and "disjnt S T" then have cloST: "closedin X (S ∪ T)" by (simp add: closedin_Un) moreover have "continuous_map (subtopology X (S ∪ T)) euclideanreal (λx. if x ∈ S then 0 else 1)" unfolding continuous_map_closedin proof (intro conjI strip) fix C :: "real set" define D where "D ≡ {x ∈ topspace X. if x ∈ S then 0 ∈ C else x ∈ T ∧ 1 ∈ C}" have "D ∈ {{}, S, T, S ∪ T}" unfolding D_def using closedin_subset [OF ‹closedin X S›] closedin_subset [OF ‹closedin X T›] ‹disjnt S T› by (auto simp: disjnt_iff) then have "closedin X D" using ‹closedin X S› ‹closedin X T› closedin_empty by blast with closedin_subset_topspace show "closedin (subtopology X (S ∪ T)) {x ∈ topspace (subtopology X (S ∪ T)). (if x ∈ S then 0::real else 1) ∈ C}" apply (simp add: D_def) by (smt (verit, best) Collect_cong Collect_mono_iff Un_def closedin_subset_topspace) qed auto ultimately obtain g :: "'a ⇒ real" where contg: "continuous_map X euclidean g" and gf: "∀x ∈ S ∪ T. g x = (if x ∈ S then 0 else 1)" using R by blast then show "∃f. continuous_map X euclideanreal f ∧ f ` S ⊆ {0} ∧ f ` T ⊆ {1}" by (smt (verit) Un_iff ‹disjnt S T› disjnt_iff image_subset_iff insert_iff) qed qed subsection ‹Random metric space stuff› lemma metrizable_imp_k_space: assumes "metrizable_space X" shows "k_space X" proof - obtain M d where "Metric_space M d" and Xeq: "X = Metric_space.mtopology M d" using assms unfolding metrizable_space_def by metis then interpret Metric_space M d by blast show ?thesis unfolding k_space Xeq proof clarsimp fix S assume "S ⊆ M" and S: "∀K. compactin mtopology K ⟶ closedin (subtopology mtopology K) (K ∩ S)" have "l ∈ S" if σ: "range σ ⊆ S" and l: "limitin mtopology σ l sequentially" for σ l proof - define K where "K ≡ insert l (range σ)" interpret Submetric M d K proof show "K ⊆ M" unfolding K_def using l limitin_mspace ‹S ⊆ M› σ by blast qed have "compactin mtopology K" unfolding K_def using ‹S ⊆ M› σ by (force intro: compactin_sequence_with_limit [OF l]) then have *: "closedin sub.mtopology (K ∩ S)" by (simp add: S mtopology_submetric) have "σ n ∈ K ∩ S" for n by (simp add: K_def range_subsetD σ) moreover have "limitin sub.mtopology σ l sequentially" using l unfolding sub.limit_metric_sequentially limit_metric_sequentially by (force simp: K_def) ultimately have "l ∈ K ∩ S" by (meson * σ image_subsetI sub.metric_closedin_iff_sequentially_closed) then show ?thesis by simp qed then show "closedin mtopology S" unfolding metric_closedin_iff_sequentially_closed using ‹S ⊆ M› by blast qed qed lemma (in Metric_space) k_space_mtopology: "k_space mtopology" by (simp add: metrizable_imp_k_space metrizable_space_mtopology) lemma k_space_euclideanreal: "k_space (euclidean :: 'a::metric_space topology)" using metrizable_imp_k_space metrizable_space_euclidean by auto subsection‹Hereditarily normal spaces› lemma hereditarily_B: assumes "⋀S T. separatedin X S T ⟹ ∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" shows "hereditarily normal_space X" unfolding hereditarily_def proof (intro strip) fix W assume "W ⊆ topspace X" show "normal_space (subtopology X W)" unfolding normal_space_def proof clarify fix S T assume clo: "closedin (subtopology X W) S" "closedin (subtopology X W) T" and "disjnt S T" then have "separatedin (subtopology X W) S T" by (simp add: separatedin_closed_sets) then obtain U V where "openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" using assms [of S T] by (meson separatedin_subtopology) then show "∃U V. openin (subtopology X W) U ∧ openin (subtopology X W) V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" apply (simp add: openin_subtopology_alt) by (meson clo closedin_imp_subset disjnt_subset1 disjnt_subset2 inf_le2) qed qed lemma hereditarily_C: assumes "separatedin X S T" and norm: "⋀U. openin X U ⟹ normal_space (subtopology X U)" shows "∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" proof - define ST where "ST ≡ X closure_of S ∩ X closure_of T" have subX: "S ⊆ topspace X" "T ⊆ topspace X" by (meson ‹separatedin X S T› separation_closedin_Un_gen)+ have sub: "S ⊆ topspace X - ST" "T ⊆ topspace X - ST" unfolding ST_def by (metis Diff_mono Diff_triv ‹separatedin X S T› Int_lower1 Int_lower2 separatedin_def)+ have "normal_space (subtopology X (topspace X - ST))" by (simp add: ST_def norm closedin_Int openin_diff) moreover have " disjnt (subtopology X (topspace X - ST) closure_of S) (subtopology X (topspace X - ST) closure_of T)" using Int_absorb1 ST_def sub by (fastforce simp: disjnt_iff closure_of_subtopology) ultimately show ?thesis using sub subX apply (simp add: normal_space_closures) by (metis ST_def closedin_Int closedin_closure_of closedin_def openin_trans_full) qed lemma hereditarily_normal_space: "hereditarily normal_space X ⟷ (∀U. openin X U ⟶ normal_space(subtopology X U))" by (metis hereditarily_B hereditarily_C hereditarily) lemma hereditarily_normal_separation: "hereditarily normal_space X ⟷ (∀S T. separatedin X S T ⟶ (∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V))" by (metis hereditarily_B hereditarily_C hereditarily) lemma metrizable_imp_hereditarily_normal_space: "metrizable_space X ⟹ hereditarily normal_space X" by (simp add: hereditarily metrizable_imp_normal_space metrizable_space_subtopology) lemma metrizable_space_separation: "⟦metrizable_space X; separatedin X S T⟧ ⟹ ∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" by (metis hereditarily hereditarily_C metrizable_imp_hereditarily_normal_space) lemma hereditarily_normal_separation_pairwise: "hereditarily normal_space X ⟷ (∀𝒰. finite 𝒰 ∧ (∀S ∈ 𝒰. S ⊆ topspace X) ∧ pairwise (separatedin X) 𝒰 ⟶ (∃ℱ. (∀S ∈ 𝒰. openin X (ℱ S) ∧ S ⊆ ℱ S) ∧ pairwise (λS T. disjnt (ℱ S) (ℱ T)) 𝒰))" (is "?lhs ⟷ ?rhs") proof assume L: ?lhs show ?rhs proof clarify fix 𝒰 assume "finite 𝒰" and 𝒰: "∀S∈𝒰. S ⊆ topspace X" and pw𝒰: "pairwise (separatedin X) 𝒰" have "∃V W. openin X V ∧ openin X W ∧ S ⊆ V ∧ (∀T. T ∈ 𝒰 ∧ T ≠ S ⟶ T ⊆ W) ∧ disjnt V W" if "S ∈ 𝒰" for S proof - have "separatedin X S (⋃(𝒰 - {S}))" by (metis 𝒰 ‹finite 𝒰› pw𝒰 finite_Diff pairwise_alt separatedin_Union(1) that) with L show ?thesis unfolding hereditarily_normal_separation by (smt (verit) Diff_iff UnionI empty_iff insert_iff subset_iff) qed then obtain ℱ 𝒢 where *: "⋀S. S ∈ 𝒰 ⟹ S ⊆ ℱ S ∧ (∀T. T ∈ 𝒰 ∧ T ≠ S ⟶ T ⊆ 𝒢 S)" and ope: "⋀S. S ∈ 𝒰 ⟹ openin X (ℱ S) ∧ openin X (𝒢 S)" and dis: "⋀S. S ∈ 𝒰 ⟹ disjnt (ℱ S) (𝒢 S)" by metis define ℋ where "ℋ ≡ λS. ℱ S ∩ (⋂T ∈ 𝒰 - {S}. 𝒢 T)" show "∃ℱ. (∀S∈𝒰. openin X (ℱ S) ∧ S ⊆ ℱ S) ∧ pairwise (λS T. disjnt (ℱ S) (ℱ T)) 𝒰" proof (intro exI conjI strip) show "openin X (ℋ S)" if "S ∈ 𝒰" for S unfolding ℋ_def by (smt (verit) ope that DiffD1 ‹finite 𝒰› finite_Diff finite_imageI imageE openin_Int_Inter) show "S ⊆ ℋ S" if "S ∈ 𝒰" for S unfolding ℋ_def using "*" that by auto show "pairwise (λS T. disjnt (ℋ S) (ℋ T)) 𝒰" using dis by (fastforce simp: disjnt_iff pairwise_alt ℋ_def) qed qed next assume R: ?rhs show ?lhs unfolding hereditarily_normal_separation proof (intro strip) fix S T assume "separatedin X S T" show "∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V" proof (cases "T=S") case True then show ?thesis using ‹separatedin X S T› by force next case False have "pairwise (separatedin X) {S, T}" by (simp add: ‹separatedin X S T› pairwise_insert separatedin_sym) moreover have "∀S∈{S, T}. S ⊆ topspace X" by (metis ‹separatedin X S T› insertE separatedin_def singletonD) ultimately show ?thesis using R by (smt (verit) False finite.emptyI finite.insertI insertCI pairwiseD) qed qed qed lemma hereditarily_normal_space_perfect_map_image: "⟦hereditarily normal_space X; perfect_map X Y f⟧ ⟹ hereditarily normal_space Y" unfolding perfect_map_def proper_map_def by (meson hereditarily_normal_space_continuous_closed_map_image) lemma regular_second_countable_imp_hereditarily_normal_space: assumes "regular_space X ∧ second_countable X" shows "hereditarily normal_space X" unfolding hereditarily proof (intro regular_Lindelof_imp_normal_space strip) show "regular_space (subtopology X S)" for S by (simp add: assms regular_space_subtopology) show "Lindelof_space (subtopology X S)" for S using assms by (simp add: second_countable_imp_Lindelof_space second_countable_subtopology) qed subsection‹Completely regular spaces› definition completely_regular_space where "completely_regular_space X ≡ ∀S x. closedin X S ∧ x ∈ topspace X - S ⟶ (∃f::'a⇒real. continuous_map X (top_of_set {0..1}) f ∧ f x = 0 ∧ (f ` S ⊆ {1}))" lemma homeomorphic_completely_regular_space_aux: assumes X: "completely_regular_space X" and hom: "X homeomorphic_space Y" shows "completely_regular_space Y" proof - obtain f g where hmf: "homeomorphic_map X Y f" and hmg: "homeomorphic_map Y X g" and fg: "(∀x ∈ topspace X. g(f x) = x) ∧ (∀y ∈ topspace Y. f(g y) = y)" using assms X homeomorphic_maps_map homeomorphic_space_def by fastforce show ?thesis unfolding completely_regular_space_def proof clarify fix S x assume A: "closedin Y S" and x: "x ∈ topspace Y" and "x ∉ S" then have "closedin X (g`S)" using hmg homeomorphic_map_closedness_eq by blast moreover have "g x ∉ g`S" by (meson A x ‹x ∉ S› closedin_subset hmg homeomorphic_imp_injective_map inj_on_image_mem_iff) ultimately obtain φ where φ: "continuous_map X (top_of_set {0..1::real}) φ ∧ φ (g x) = 0 ∧ φ ` g`S ⊆ {1}" by (metis DiffI X completely_regular_space_def hmg homeomorphic_imp_surjective_map image_eqI x) then have "continuous_map Y (top_of_set {0..1::real}) (φ ∘ g)" by (meson continuous_map_compose hmg homeomorphic_imp_continuous_map) then show "∃ψ. continuous_map Y (top_of_set {0..1::real}) ψ ∧ ψ x = 0 ∧ ψ ` S ⊆ {1}" by (metis φ comp_apply image_comp) qed qed lemma homeomorphic_completely_regular_space: assumes "X homeomorphic_space Y" shows "completely_regular_space X ⟷ completely_regular_space Y" by (meson assms homeomorphic_completely_regular_space_aux homeomorphic_space_sym) lemma completely_regular_space_alt: "completely_regular_space X ⟷ (∀S x. closedin X S ⟶ x ∈ topspace X - S ⟶ (∃f. continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` S ⊆ {1}))" proof - have "∃f. continuous_map X (top_of_set {0..1::real}) f ∧ f x = 0 ∧ f ` S ⊆ {1}" if "closedin X S" "x ∈ topspace X - S" and f: "continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` S ⊆ {1}" for S x f proof (intro exI conjI) show "continuous_map X (top_of_set {0..1}) (λx. max 0 (min (f x) 1))" using that by (auto simp: continuous_map_in_subtopology intro!: continuous_map_real_max continuous_map_real_min) qed (use that in auto) with continuous_map_in_subtopology show ?thesis unfolding completely_regular_space_def by metis qed text ‹As above, but with @{term openin}› lemma completely_regular_space_alt': "completely_regular_space X ⟷ (∀S x. openin X S ⟶ x ∈ S ⟶ (∃f. continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` (topspace X - S) ⊆ {1}))" apply (simp add: completely_regular_space_alt all_closedin) by (meson openin_subset subsetD) lemma completely_regular_space_gen_alt: fixes a b::real assumes "a ≠ b" shows "completely_regular_space X ⟷ (∀S x. closedin X S ⟶ x ∈ topspace X - S ⟶ (∃f. continuous_map X euclidean f ∧ f x = a ∧ (f ` S ⊆ {b})))" proof - have "∃f. continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` S ⊆ {1}" if "closedin X S" "x ∈ topspace X - S" and f: "continuous_map X euclidean f ∧ f x = a ∧ f ` S ⊆ {b}" for S x f proof (intro exI conjI) show "continuous_map X euclideanreal ((λx. inverse(b - a) * (x - a)) ∘ f)" using that by (intro continuous_intros) auto qed (use that assms in auto) moreover have "∃f. continuous_map X euclidean f ∧ f x = a ∧ f ` S ⊆ {b}" if "closedin X S" "x ∈ topspace X - S" and f: "continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` S ⊆ {1}" for S x f proof (intro exI conjI) show "continuous_map X euclideanreal ((λx. a + (b - a) * x) ∘ f)" using that by (intro continuous_intros) auto qed (use that in auto) ultimately show ?thesis unfolding completely_regular_space_alt by meson qed text ‹As above, but with @{term openin}› lemma completely_regular_space_gen_alt': fixes a b::real assumes "a ≠ b" shows "completely_regular_space X ⟷ (∀S x. openin X S ⟶ x ∈ S ⟶ (∃f. continuous_map X euclidean f ∧ f x = a ∧ (f ` (topspace X - S) ⊆ {b})))" apply (simp add: completely_regular_space_gen_alt[OF assms] all_closedin) by (meson openin_subset subsetD) lemma completely_regular_space_gen: fixes a b::real assumes "a < b" shows "completely_regular_space X ⟷ (∀S x. closedin X S ∧ x ∈ topspace X - S ⟶ (∃f. continuous_map X (top_of_set {a..b}) f ∧ f x = a ∧ f ` S ⊆ {b}))" proof - have "∃f. continuous_map X (top_of_set {a..b}) f ∧ f x = a ∧ f ` S ⊆ {b}" if "closedin X S" "x ∈ topspace X - S" and f: "continuous_map X euclidean f ∧ f x = a ∧ f ` S ⊆ {b}" for S x f proof (intro exI conjI) show "continuous_map X (top_of_set {a..b}) (λx. max a (min (f x) b))" using that assms by (auto simp: continuous_map_in_subtopology intro!: continuous_map_real_max continuous_map_real_min) qed (use that assms in auto) with continuous_map_in_subtopology assms show ?thesis using completely_regular_space_gen_alt [of a b] by (smt (verit) atLeastAtMost_singleton atLeastatMost_empty singletonI) qed lemma normal_imp_completely_regular_space_A: assumes "normal_space X" "t1_space X" shows "completely_regular_space X" unfolding completely_regular_space_alt proof clarify fix x S assume A: "closedin X S" "x ∉ S" assume "x ∈ topspace X" then have "closedin X {x}" by (simp add: ‹t1_space X› closedin_t1_singleton) with A ‹normal_space X› have "∃f. continuous_map X euclideanreal f ∧ f ` {x} ⊆ {0} ∧ f ` S ⊆ {1}" using assms unfolding normal_space_iff_Urysohn_alt disjnt_iff by blast then show "∃f. continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` S ⊆ {1}" by auto qed lemma normal_imp_completely_regular_space_B: assumes "normal_space X" "regular_space X" shows "completely_regular_space X" unfolding completely_regular_space_alt proof clarify fix x S assume "closedin X S" "x ∉ S" "x ∈ topspace X" then obtain U C where "openin X U" "closedin X C" "x ∈ U" "U ⊆ C" "C ⊆ topspace X - S" using assms unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of closedin_def by (metis Diff_iff) then obtain f where "continuous_map X euclideanreal f ∧ f ` C ⊆ {0} ∧ f ` S ⊆ {1}" using assms unfolding normal_space_iff_Urysohn_alt by (metis Diff_iff ‹closedin X S› disjnt_iff subsetD) then show "∃f. continuous_map X euclideanreal f ∧ f x = 0 ∧ f ` S ⊆ {1}" by (meson ‹U ⊆ C› ‹x ∈ U› image_subset_iff singletonD subsetD) qed lemma normal_imp_completely_regular_space_gen: "⟦normal_space X; t1_space X ∨ Hausdorff_space X ∨ regular_space X⟧ ⟹ completely_regular_space X" using normal_imp_completely_regular_space_A normal_imp_completely_regular_space_B t1_or_Hausdorff_space by blast lemma normal_imp_completely_regular_space: "⟦normal_space X; Hausdorff_space X ∨ regular_space X⟧ ⟹ completely_regular_space X" by (simp add: normal_imp_completely_regular_space_gen) lemma (in Metric_space) completely_regular_space_mtopology: "completely_regular_space mtopology" by (simp add: normal_imp_completely_regular_space normal_space_mtopology regular_space_mtopology) lemma metrizable_imp_completely_regular_space: "metrizable_space X ⟹ completely_regular_space X" by (simp add: metrizable_imp_normal_space metrizable_imp_regular_space normal_imp_completely_regular_space) lemma completely_regular_space_discrete_topology: "completely_regular_space(discrete_topology U)" by (simp add: normal_imp_completely_regular_space normal_space_discrete_topology) lemma completely_regular_space_subtopology: assumes "completely_regular_space X" shows "completely_regular_space (subtopology X S)" unfolding completely_regular_space_def proof clarify fix A x assume "closedin (subtopology X S) A" and x: "x ∈ topspace (subtopology X S)" and "x ∉ A" then obtain T where "closedin X T" "A = S ∩ T" "x ∈ topspace X" "x ∈ S" by (force simp: closedin_subtopology_alt image_iff) then show "∃f. continuous_map (subtopology X S) (top_of_set {0::real..1}) f ∧ f x = 0 ∧ f ` A ⊆ {1}" using assms ‹x ∉ A› apply (simp add: completely_regular_space_def continuous_map_from_subtopology) using continuous_map_from_subtopology by fastforce qed lemma completely_regular_space_retraction_map_image: " ⟦retraction_map X Y r; completely_regular_space X⟧ ⟹ completely_regular_space Y" using completely_regular_space_subtopology hereditary_imp_retractive_property homeomorphic_completely_regular_space by blast lemma completely_regular_imp_regular_space: assumes "completely_regular_space X" shows "regular_space X" proof - have *: "∃U V. openin X U ∧ openin X V ∧ a ∈ U ∧ C ⊆ V ∧ disjnt U V" if contf: "continuous_map X euclideanreal f" and a: "a ∈ topspace X - C" and "closedin X C" and fim: "f ` topspace X ⊆ {0..1}" and f0: "f a = 0" and f1: "f ` C ⊆ {1}" for C a f proof (intro exI conjI) show "openin X {x ∈ topspace X. f x ∈ {..<1 / 2}}" "openin X {x ∈ topspace X. f x ∈ {1 / 2<..}}" using openin_continuous_map_preimage [OF contf] by (meson open_lessThan open_greaterThan open_openin)+ show "a ∈ {x ∈ topspace X. f x ∈ {..<1 / 2}}" using a f0 by auto show "C ⊆ {x ∈ topspace X. f x ∈ {1 / 2<..}}" using ‹closedin X C› f1 closedin_subset by auto qed (auto simp: disjnt_iff) show ?thesis using assms unfolding completely_regular_space_def regular_space_def continuous_map_in_subtopology by (meson "*") qed proposition locally_compact_regular_imp_completely_regular_space: assumes "locally_compact_space X" "Hausdorff_space X ∨ regular_space X" shows "completely_regular_space X" unfolding completely_regular_space_def proof clarify fix S x assume "closedin X S" and "x ∈ topspace X" and "x ∉ S" have "regular_space X" using assms locally_compact_Hausdorff_imp_regular_space by blast then have nbase: "neighbourhood_base_of (λC. compactin X C ∧ closedin X C) X" using assms(1) locally_compact_regular_space_neighbourhood_base by blast then obtain U M where "openin X U" "compactin X M" "closedin X M" "x ∈ U" "U ⊆ M" "M ⊆ topspace X - S" unfolding neighbourhood_base_of by (metis (no_types, lifting) Diff_iff ‹closedin X S› ‹x ∈ topspace X› ‹x ∉ S› closedin_def) then have "M ⊆ topspace X" by blast obtain V K where "openin X V" "closedin X K" "x ∈ V" "V ⊆ K" "K ⊆ U" by (metis (no_types, lifting) ‹openin X U› ‹x ∈ U› neighbourhood_base_of nbase) have "compact_space (subtopology X M)" by (simp add: ‹compactin X M› compact_space_subtopology) then have "normal_space (subtopology X M)" by (simp add: ‹regular_space X› compact_Hausdorff_or_regular_imp_normal_space regular_space_subtopology) moreover have "closedin (subtopology X M) K" using ‹K ⊆ U› ‹U ⊆ M› ‹closedin X K› closedin_subset_topspace by fastforce moreover have "closedin (subtopology X M) (M - U)" by (simp add: ‹closedin X M› ‹openin X U› closedin_diff closedin_subset_topspace) moreover have "disjnt K (M - U)" by (meson DiffD2 ‹K ⊆ U› disjnt_iff subsetD) ultimately obtain f::"'a⇒real" where contf: "continuous_map (subtopology X M) (top_of_set {0..1}) f" and f0: "f ` K ⊆ {0}" and f1: "f ` (M - U) ⊆ {1}" using Urysohn_lemma [of "subtopology X M" K "M-U" 0 1] by auto then obtain g::"'a⇒real" where contg: "continuous_map (subtopology X M) euclidean g" and gim: "g ` M ⊆ {0..1}" and g0: "⋀x. x ∈ K ⟹ g x = 0" and g1: "⋀x. ⟦x ∈ M; x ∉ U⟧ ⟹ g x = 1" using ‹M ⊆ topspace X› by (force simp: continuous_map_in_subtopology image_subset_iff) show "∃f::'a⇒real. continuous_map X (top_of_set {0..1}) f ∧ f x = 0 ∧ f ` S ⊆ {1}" proof (intro exI conjI) show "continuous_map X (top_of_set {0..1}) (λx. if x ∈ M then g x else 1)" unfolding continuous_map_closedin proof (intro strip conjI) fix C assume C: "closedin (top_of_set {0::real..1}) C" have eq: "{x ∈ topspace X. (if x ∈ M then g x else 1) ∈ C} = {x ∈ M. g x ∈ C} ∪ (if 1 ∈ C then topspace X - U else {})" using ‹U ⊆ M› ‹M ⊆ topspace X› g1 by auto show "closedin X {x ∈ topspace X. (if x ∈ M then g x else 1) ∈ C}" unfolding eq proof (intro closedin_Un) have "closedin euclidean C" using C closed_closedin closedin_closed_trans by blast then have "closedin (subtopology X M) {x ∈ M. g x ∈ C}" using closedin_continuous_map_preimage_gen [OF contg] ‹M ⊆ topspace X› by auto then show "closedin X {x ∈ M. g x ∈ C}" using ‹closedin X M› closedin_trans_full by blast qed (use ‹openin X U› in force) qed (use gim in force) show "(if x ∈ M then g x else 1) = 0" using ‹U ⊆ M› ‹V ⊆ K› g0 ‹x ∈ U› ‹x ∈ V› by auto show "(λx. if x ∈ M then g x else 1) ` S ⊆ {1}" using ‹M ⊆ topspace X - S› by auto qed qed lemma completely_regular_eq_regular_space: "locally_compact_space X ⟹ (completely_regular_space X ⟷ regular_space X)" using completely_regular_imp_regular_space locally_compact_regular_imp_completely_regular_space by blast lemma completely_regular_space_prod_topology: "completely_regular_space (prod_topology X Y) ⟷ (prod_topology X Y) = trivial_topology ∨ completely_regular_space X ∧ completely_regular_space Y" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (rule topological_property_of_prod_component) (auto simp: completely_regular_space_subtopology homeomorphic_completely_regular_space) next assume R: ?rhs show ?lhs proof (cases "(prod_topology X Y) = trivial_topology") case False then have X: "completely_regular_space X" and Y: "completely_regular_space Y" using R by blast+ show ?thesis unfolding completely_regular_space_alt' proof clarify fix W x y assume "openin (prod_topology X Y) W" and "(x, y) ∈ W" then obtain U V where "openin X U" "openin Y V" "x ∈ U" "y ∈ V" "U×V ⊆ W" by (force simp: openin_prod_topology_alt) then have "x ∈ topspace X" "y ∈ topspace Y" using openin_subset by fastforce+ obtain f where contf: "continuous_map X euclideanreal f" and "f x = 0" and f1: "⋀x. x ∈ topspace X ⟹ x ∉ U ⟹ f x = 1" using X ‹openin X U› ‹x ∈ U› unfolding completely_regular_space_alt' by (smt (verit, best) Diff_iff image_subset_iff singletonD) obtain g where contg: "continuous_map Y euclideanreal g" and "g y = 0" and g1: "⋀y. y ∈ topspace Y ⟹ y ∉ V ⟹ g y = 1" using Y ‹openin Y V› ‹y ∈ V› unfolding completely_regular_space_alt' by (smt (verit, best) Diff_iff image_subset_iff singletonD) define h where "h ≡ λ(x,y). 1 - (1 - f x) * (1 - g y)" show "∃h. continuous_map (prod_topology X Y) euclideanreal h ∧ h (x,y) = 0 ∧ h ` (topspace (prod_topology X Y) - W) ⊆ {1}" proof (intro exI conjI) have "continuous_map (prod_topology X Y) euclideanreal (f ∘ fst)" using contf continuous_map_of_fst by blast moreover have "continuous_map (prod_topology X Y) euclideanreal (g ∘ snd)" using contg continuous_map_of_snd by blast ultimately show "continuous_map (prod_topology X Y) euclideanreal h" unfolding o_def h_def case_prod_unfold by (intro continuous_intros) auto show "h (x, y) = 0" by (simp add: h_def ‹f x = 0› ‹g y = 0›) show "h ` (topspace (prod_topology X Y) - W) ⊆ {1}" using ‹U × V ⊆ W› f1 g1 by (force simp: h_def) qed qed qed (force simp: completely_regular_space_def) qed proposition completely_regular_space_product_topology: "completely_regular_space (product_topology X I) ⟷ (∃i∈I. X i = trivial_topology) ∨ (∀i ∈ I. completely_regular_space (X i))" (is "?lhs ⟷ ?rhs") proof assume ?lhs then show ?rhs by (rule topological_property_of_product_component) (auto simp: completely_regular_space_subtopology homeomorphic_completely_regular_space) next assume R: ?rhs show ?lhs proof (cases "∃i∈I. X i = trivial_topology") case False show ?thesis unfolding completely_regular_space_alt' proof clarify fix W x assume W: "openin (product_topology X I) W" and "x ∈ W" then obtain U where finU: "finite {i ∈ I. U i ≠ topspace (X i)}" and ope: "⋀i. i∈I ⟹ openin (X i) (U i)" and x: "x ∈ Pi⇩_{E}I U" and "Pi⇩_{E}I U ⊆ W" by (auto simp: openin_product_topology_alt) have "∀i ∈ I. openin (X i) (U i) ∧ x i ∈ U i ⟶ (∃f. continuous_map (X i) euclideanreal f ∧ f (x i) = 0 ∧ (∀x ∈ topspace(X i). x ∉ U i ⟶ f x = 1))" using R unfolding completely_regular_space_alt' by (smt (verit) DiffI False image_subset_iff singletonD) with ope x have "⋀i. ∃f. i ∈ I ⟶ continuous_map (X i) euclideanreal f ∧ f (x i) = 0 ∧ (∀x ∈ topspace (X i). x ∉ U i ⟶ f x = 1)" by auto then obtain f where f: "⋀i. i ∈ I ⟹ continuous_map (X i) euclideanreal (f i) ∧ f i (x i) = 0 ∧ (∀x ∈ topspace (X i). x ∉ U i ⟶ f i x = 1)" by metis define h where "h ≡ λz. 1