# Theory Urysohn

```(*  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)"
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}"
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"
then show ?thesis
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"
by (smt (verit, del_insts) ‹0 < d› ‹0 ≤ y›)
then show ?thesis
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'"
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›
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)"
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
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)
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)"
also have "… = (c/3) * 3 * ((2/3) ^ m - (2/3) ^ n)"
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)"
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}"
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)"
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"

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"
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"
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
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
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}))"
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"

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)"

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›
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 ```