diff -r f3d19c8445ec -r 24b70433c2e8 src/HOL/Analysis/Urysohn.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Urysohn.thy	Tue May 30 12:33:06 2023 +0100
@@ -0,0 +1,2238 @@
+(*  Title:      HOL/Analysis/Arcwise_Connected.thy
+    Authors:    LC Paulson, based on material from HOL Light
+*)
+
+section \<open>Urysohn lemma and its Consequences\<close>
+
+theory Urysohn
+imports Abstract_Topological_Spaces Abstract_Metric_Spaces Infinite_Sum Arcwise_Connected
+begin
+
+subsection \<open>Urysohn lemma and Tietze's theorem\<close>
+
+lemma Urysohn_lemma:
+  fixes a b :: real
+  assumes "normal_space X" "closedin X S" "closedin X T" "disjnt S T" "a \<le> b" 
+  obtains f where "continuous_map X (top_of_set {a..b}) f" "f ` S \<subseteq> {a}" "f ` T \<subseteq> {b}"
+proof -
+  obtain U where "openin X U" "S \<subseteq> U" "X closure_of U \<subseteq> 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 "\<exists>G :: real \<Rightarrow> 'a set. G 0 = U \<and> G 1 = topspace X - T \<and>
+               (\<forall>x \<in> dyadics \<inter> {0..1}. \<forall>y \<in> dyadics \<inter> {0..1}. x < y \<longrightarrow> openin X (G x) \<and> openin X (G y) \<and> X closure_of (G x) \<subseteq> G y)"
+  proof (rule recursion_on_dyadic_fractions)
+    show "openin X U \<and> openin X (topspace X - T) \<and> X closure_of U \<subseteq> topspace X - T"
+      using \<open>X closure_of U \<subseteq> topspace X - T\<close> \<open>openin X U\<close> \<open>closedin X T\<close> by blast
+    show "\<exists>z. (openin X x \<and> openin X z \<and> X closure_of x \<subseteq> z) \<and> openin X z \<and> openin X y \<and> X closure_of z \<subseteq> y"
+      if "openin X x \<and> openin X y \<and> X closure_of x \<subseteq> y" for x y
+      by (meson that closedin_closure_of normal_space_alt \<open>normal_space X\<close>)
+    show "openin X x \<and> openin X z \<and> X closure_of x \<subseteq> z"
+      if "openin X x \<and> openin X y \<and> X closure_of x \<subseteq> y" and "openin X y \<and> openin X z \<and> X closure_of y \<subseteq> z" for x y z
+      by (meson that closure_of_subset openin_subset subset_trans)
+  qed
+  then obtain G :: "real \<Rightarrow> 'a set"
+      where G0: "G 0 = U" and G1: "G 1 = topspace X - T"
+        and G: "\<And>x y. \<lbrakk>x \<in> dyadics; y \<in> dyadics; 0 \<le> x; x < y; y \<le> 1\<rbrakk>
+                      \<Longrightarrow> openin X (G x) \<and> openin X (G y) \<and> X closure_of (G x) \<subseteq> G y"
+    by (smt (verit, del_insts) Int_iff atLeastAtMost_iff)
+  define f where "f \<equiv> \<lambda>x. Inf(insert 1 {r. r \<in> dyadics \<inter> {0..1} \<and> x \<in> G r})"
+  have f_ge: "f x \<ge> 0" if "x \<in> topspace X" for x
+    unfolding f_def by (force intro: cInf_greatest)
+  moreover have f_le1: "f x \<le> 1" if "x \<in> topspace X" for x
+  proof -
+    have "bdd_below {r \<in> dyadics \<inter> {0..1}. x \<in> 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 \<subseteq> {0..1}"
+    by (auto simp: f_def)
+  have 0: "0 \<in> dyadics \<inter> {0..1::real}" and 1: "1 \<in> dyadics \<inter> {0..1::real}"
+    by (force simp: dyadics_def)+
+  then have opeG: "openin X (G r)" if "r \<in> dyadics \<inter> {0..1}" for r
+    using G G0 \<open>openin X U\<close> less_eq_real_def that by auto
+  have "x \<in> G 0" if "x \<in> S" for x
+    using G0 \<open>S \<subseteq> U\<close> that by blast
+  with 0 have fimS: "f ` S \<subseteq> {0}"
+    unfolding f_def by (force intro!: cInf_eq_minimum)
+  have False if "r \<in> dyadics" "0 \<le> r" "r < 1" "x \<in> G r" "x \<in> 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\<ge>1" if "r \<in> dyadics" "0 \<le> r" "r \<le> 1" "x \<in> G r" "x \<in> T" for r x
+    using linorder_not_le that by blast
+  then have fimT: "f ` T \<subseteq> {1}"
+    unfolding f_def by (force intro!: cInf_eq_minimum)
+  have fle1: "f z \<le> 1" for z
+    by (force simp: f_def intro: cInf_lower)
+  have fle: "f z \<le> x" if "x \<in> dyadics \<inter> {0..1}" "z \<in> G x" for z x
+    using that by (force simp: f_def intro: cInf_lower)
+  have *: "b \<le> f z" if "b \<le> 1" "\<And>x. \<lbrakk>x \<in> dyadics \<inter> {0..1}; z \<in> G x\<rbrakk> \<Longrightarrow> b \<le> x" for z b
+    using that by (force simp: f_def intro: cInf_greatest)
+  have **: "r \<le> f x" if r: "r \<in> dyadics \<inter> {0..1}" "x \<notin> G r" for r x
+  proof (rule *)
+    show "r \<le> s" if "s \<in> dyadics \<inter> {0..1}" and "x \<in> G s" for s :: real
+      using that r G [of s r] by (force simp add: dest: closure_of_subset openin_subset)
+  qed (use that in force)
+
+  have "\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. \<bar>f y - f x\<bar> < \<epsilon>)"
+    if "x \<in> topspace X" and "0 < \<epsilon>" for x \<epsilon>
+  proof -
+    have A: "\<exists>r. r \<in> dyadics \<inter> {0..1} \<and> r < y \<and> \<bar>r - y\<bar> < d" if "0 < y" "y \<le> 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" "\<bar>q / 2^n - r / 2^n \<bar> < d"
+        by (smt (verit, del_insts) padic_rational_approximation_straddle_pos  \<open>0 < d\<close> \<open>0 < y\<close>) 
+      then show ?thesis
+        unfolding dyadics_def
+        using divide_eq_0_iff that(2) by fastforce
+    qed
+    have B: "\<exists>r. r \<in> dyadics \<inter> {0..1} \<and> y < r \<and> \<bar>r - y\<bar> < d" if "0 \<le> y" "y < 1" "0 < d" for y d::real
+    proof -
+      obtain n q r 
+        where "of_nat q / 2^n \<le> y" "y < of_nat r / 2^n" "\<bar>q / 2^n - r / 2^n \<bar> < d"
+        using padic_rational_approximation_straddle_pos_le
+        by (smt (verit, del_insts) \<open>0 < d\<close> \<open>0 \<le> y\<close>) 
+      then show ?thesis
+        apply (clarsimp simp: dyadics_def)
+        using divide_eq_0_iff \<open>y < 1\<close>
+        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 \<in> dyadics \<inter> {0..1}" "0 < r" "\<bar>r\<bar> < \<epsilon>/2"
+        by (smt (verit) \<open>0 < \<epsilon>\<close> half_gt_zero)
+      show ?thesis
+      proof (intro exI conjI)
+        show "openin X (G r)"
+          using opeG r(1) by blast
+        show "x \<in> G r"
+          using True ** r by force
+        show "\<forall>y \<in> G r. \<bar>f y - f x\<bar> < \<epsilon>"
+          using f_ge \<open>openin X (G r)\<close> 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 \<in> dyadics \<inter> {0..1}" "r < 1" "\<bar>r-1\<bar> < \<epsilon>/2"
+          by (smt (verit) \<open>0 < \<epsilon>\<close> half_gt_zero)
+        define G' where "G' \<equiv> 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' \<in> dyadics \<and> 0 \<le> r' \<and> r' \<le> 1 \<and> r < r' \<and> \<bar>r' - r\<bar> < 1 - r"
+            using B r by force 
+          moreover
+          have "1 - r \<in> dyadics" "0 \<le> r"
+            using 1 r dyadics_diff by force+
+          ultimately have "x \<notin> X closure_of G r"
+            using G True r fle by force
+          then show "x \<in> G'"
+            by (simp add: G'_def that)
+          show "\<forall>y \<in> G'. \<bar>f y - f x\<bar> < \<epsilon>"
+            using ** f_le1 in_closure_of r by (fastforce simp add: True G'_def)
+        qed
+      next
+        case False
+        have "0 < f x" "f x < 1"
+          using fle1 f_ge that(1) \<open>f x \<noteq> 0\<close> \<open>f x \<noteq> 1\<close> by (metis order_le_less) +
+        obtain r where r: "r \<in> dyadics \<inter> {0..1}" "r < f x" "\<bar>r - f x\<bar> < \<epsilon> / 2"
+          using A \<open>0 < \<epsilon>\<close> \<open>0 < f x\<close> \<open>f x < 1\<close> by (smt (verit, best) half_gt_zero)
+        obtain r' where r': "r' \<in> dyadics \<inter> {0..1}" "f x < r'" "\<bar>r' - f x\<bar> < \<epsilon> / 2"
+          using B \<open>0 < \<epsilon>\<close> \<open>0 < f x\<close> \<open>f x < 1\<close> by (smt (verit, best) half_gt_zero)
+        have "r < 1"
+          using \<open>f x < 1\<close> 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 \<in> X closure_of G r \<Longrightarrow> False"
+            using B [of r "f x - r"] r \<open>r < 1\<close> G [of r] fle by force
+          then show "x \<in> G r' - X closure_of G r"
+            using ** r' by fastforce
+          show "\<forall>y\<in>G r' - X closure_of G r. \<bar>f y - f x\<bar> < \<epsilon>"
+            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 add: Met_TC.continuous_map_to_metric dist_real_def continuous_map_in_subtopology fim simp flip: Met_TC.mtopology_is_euclideanreal)
+  define g where "g \<equiv> \<lambda>x. a + (b - a) * f x"
+  show thesis
+  proof
+    have "continuous_map X euclideanreal g"
+      using contf \<open>a \<le> b\<close> unfolding g_def by (auto simp: continuous_intros continuous_map_in_subtopology)
+    moreover have "g ` (topspace X) \<subseteq> {a..b}"
+      using mult_left_le [of "f _" "b-a"] contf \<open>a \<le> b\<close>   
+      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 \<subseteq> {a}" "g ` T \<subseteq> {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 \<subseteq> {a}" "f ` T \<subseteq> {b}"
+  by (metis Urysohn_lemma assms continuous_map_in_subtopology disjnt_sym linear)
+
+lemma normal_space_iff_Urysohn_gen_alt:
+  assumes "a \<noteq> b"
+  shows "normal_space X \<longleftrightarrow>
+         (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
+                \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and> f ` S \<subseteq> {a} \<and> f ` T \<subseteq> {b}))"
+ (is "?lhs=?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?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 \<subseteq> {a}" "f ` T \<subseteq> {b}"
+      by meson
+    show "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+    proof (intro conjI exI)
+      show "openin X {x \<in> topspace X. f x \<in> ball a (\<bar>a - b\<bar> / 2)}"
+        by (force intro!: openin_continuous_map_preimage [OF contf])
+      show "openin X {x \<in> topspace X. f x \<in> ball b (\<bar>a - b\<bar> / 2)}"
+        by (force intro!: openin_continuous_map_preimage [OF contf])
+      show "S \<subseteq> {x \<in> topspace X. f x \<in> ball a (\<bar>a - b\<bar> / 2)}"
+        using \<open>closedin X S\<close> closedin_subset \<open>f ` S \<subseteq> {a}\<close> assms by force
+      show "T \<subseteq> {x \<in> topspace X. f x \<in> ball b (\<bar>a - b\<bar> / 2)}"
+        using \<open>closedin X T\<close> closedin_subset \<open>f ` T \<subseteq> {b}\<close> assms by force
+      have "\<And>x. \<lbrakk>x \<in> topspace X; dist a (f x) < \<bar>a-b\<bar>/2; dist b (f x) < \<bar>a-b\<bar>/2\<rbrakk> \<Longrightarrow> False"
+        by (smt (verit, best) dist_real_def dist_triangle_half_l)
+      then show "disjnt {x \<in> topspace X. f x \<in> ball a (\<bar>a-b\<bar> / 2)} {x \<in> topspace X. f x \<in> ball b (\<bar>a-b\<bar> / 2)}"
+        using disjnt_iff by fastforce
+    qed
+  qed
+qed 
+
+lemma normal_space_iff_Urysohn_gen:
+  fixes a b::real
+  shows
+   "a < b \<Longrightarrow> 
+      normal_space X \<longleftrightarrow>
+        (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
+               \<longrightarrow> (\<exists>f. continuous_map X (top_of_set {a..b}) f \<and>
+                        f ` S \<subseteq> {a} \<and> f ` T \<subseteq> {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 \<longleftrightarrow>
+     (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
+           \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and>
+                   f ` S \<subseteq> {0} \<and> f ` T \<subseteq> {1}))"
+  by (rule normal_space_iff_Urysohn_gen_alt) auto
+
+lemma normal_space_iff_Urysohn:
+   "normal_space X \<longleftrightarrow>
+     (\<forall>S T. closedin X S \<and> closedin X T \<and> disjnt S T
+            \<longrightarrow> (\<exists>f::'a\<Rightarrow>real. continuous_map X (top_of_set {0..1}) f \<and> 
+                               f ` S \<subseteq> {0} \<and> f ` T \<subseteq> {1}))"
+  by (rule normal_space_iff_Urysohn_gen) auto
+
+lemma normal_space_perfect_map_image:
+   "\<lbrakk>normal_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> 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:
+   "\<lbrakk>normal_space X; closed_map X Y f; continuous_map X Y f;
+     f ` topspace X = topspace Y; t1_space Y\<rbrakk>
+    \<Longrightarrow> Hausdorff_space Y"
+  by (metis normal_space_continuous_closed_map_image normal_t1_imp_Hausdorff_space)
+
+lemma normal_Hausdorff_space_closed_continuous_map_image:
+   "\<lbrakk>normal_space X; Hausdorff_space X; closed_map X Y f;
+     continuous_map X Y f; f ` topspace X = topspace Y\<rbrakk>
+    \<Longrightarrow> normal_space Y \<and> 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 \<noteq> {}" 
+    and clo: "closedin X S" "closedin X T" "disjnt S T"
+  obtains h :: "nat \<Rightarrow> 'a set" where 
+    "\<And>n. openin X (h n)" "\<And>n. disjnt T (X closure_of (h n))" and  "S \<subseteq> \<Union>(range h)"
+proof -
+  have "\<exists>U. openin X U \<and> x \<in> U \<and> disjnt T (X closure_of U)"
+    if "x \<in> S" for x
+    using \<open>regular_space X\<close> unfolding regular_space 
+    by (metis (full_types) Diff_iff \<open>disjnt S T\<close> clo closure_of_eq disjnt_iff in_closure_of that)
+  then obtain h where oh: "\<And>x. x \<in> S \<Longrightarrow> openin X (h x)"
+    and xh: "\<And>x. x \<in> S \<Longrightarrow> x \<in> h x"
+    and dh: "\<And>x. x \<in> S \<Longrightarrow> disjnt T (X closure_of h x)"
+    by metis
+  have "Lindelof_space(subtopology X S)"
+    by (simp add: Lindelof_space_closedin_subtopology \<open>Lindelof_space X\<close> \<open>closedin X S\<close>)
+  then obtain \<U> where \<U>: "countable \<U> \<and> \<U> \<subseteq> h ` S \<and> S \<subseteq> \<Union>\<U>"
+    unfolding Lindelof_space_subtopology_subset [OF closedin_subset [OF \<open>closedin X S\<close>]]
+    by (smt (verit, del_insts) oh xh UN_I image_iff subsetI)
+  with \<open>S \<noteq> {}\<close> have "\<U> \<noteq> {}"
+    by blast
+  show ?thesis
+  proof
+    show "openin X (from_nat_into \<U> n)" for n
+      by (metis \<U> from_nat_into image_iff \<open>\<U> \<noteq> {}\<close> oh subsetD)
+    show "disjnt T (X closure_of (from_nat_into \<U>) n)" for n
+      using dh from_nat_into [OF \<open>\<U> \<noteq> {}\<close>]
+      by (metis \<U> f_inv_into_f inv_into_into subset_eq)
+    show "S \<subseteq> \<Union>(range (from_nat_into \<U>))"
+      by (simp add: \<U> \<open>\<U> \<noteq> {}\<close>)
+  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 "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+  proof (cases "S={} \<or> 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 \<Rightarrow> 'a set" where 
+      opeh: "\<And>n. openin X (h n)" and dish: "\<And>n. disjnt T (X closure_of (h n))"
+      and Sh: "S \<subseteq> \<Union>(range h)"
+      by (metis Lindelof_cover False \<open>disjnt S T\<close> assms clo)
+    obtain k :: "nat \<Rightarrow> 'a set" where 
+      opek: "\<And>n. openin X (k n)" and disk: "\<And>n. disjnt S (X closure_of (k n))"
+      and Tk: "T \<subseteq> \<Union>(range k)"
+      by (metis Lindelof_cover False \<open>disjnt S T\<close> assms clo disjnt_sym)
+    define U where "U \<equiv> \<Union>i. h i - (\<Union>j<i. X closure_of k j)"
+    define V where "V \<equiv> \<Union>i. k i - (\<Union>j\<le>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 \<subseteq> U" "T \<subseteq> V"
+        using Sh Tk dish disk by (fastforce simp: U_def V_def disjnt_iff)+
+      have "\<And>x i j. \<lbrakk>x \<in> k i; x \<in> h j; \<forall>j\<le>i. x \<notin> X closure_of h j\<rbrakk>
+                 \<Longrightarrow> \<exists>i<j. x \<in> 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 add: U_def V_def disjnt_iff)
+    qed
+  qed
+qed
+
+lemma 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 \<subseteq> {a..b}" and "a \<le> b"
+  obtains g 
+  where "continuous_map X euclideanreal g" 
+        "\<And>x. x \<in> S \<Longrightarrow> g x = f x" "g ` topspace X \<subseteq> {a..b}"
+proof -
+  define c where "c \<equiv> max \<bar>a\<bar> \<bar>b\<bar> + 1"
+  have "0 < c" and c: "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> c"
+    using fim by (auto simp: c_def image_subset_iff)
+  define good where 
+    "good \<equiv> \<lambda>g n. continuous_map X euclideanreal g \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> \<le> c * (2/3)^n)"
+  have step: "\<exists>g. good g (Suc n) \<and>
+              (\<forall>x \<in> topspace X. \<bar>g x - h x\<bar> \<le> c * (2/3)^n / 3)"
+    if h: "good h n" for n h
+  proof -
+    have pos: "0 < c * (2/3) ^ n"
+      by (simp add: \<open>0 < c\<close>)
+    have S_eq: "S = topspace(subtopology X S)" and "S \<subseteq> topspace X"
+      using \<open>closedin X S\<close> closedin_subset by auto
+    define d where "d \<equiv> c/3 * (2/3) ^ n"
+    define SA where "SA \<equiv> {x \<in> S. f x - h x \<in> {..-d}}"
+    define SB where "SB \<equiv> {x \<in> S. f x - h x \<in> {d..}}"
+    have contfh: "continuous_map (subtopology X S) euclideanreal (\<lambda>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 \<open>closedin X S\<close> 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 \<open>closedin X S\<close> 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 \<le> 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 \<subseteq> {- d}" and gb: "g ` SB \<subseteq> {d}"
+      using Urysohn_lemma \<open>normal_space X\<close> by metis
+    then have g_le_d: "\<And>x. x \<in> topspace X \<Longrightarrow> \<bar>g x\<bar> \<le> d"
+      by (simp add: abs_le_iff continuous_map_def minus_le_iff)
+    have g_eq_d: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<le> -d\<rbrakk> \<Longrightarrow> g x = -d"
+      using ga by (auto simp: SA_def)
+    have g_eq_negd: "\<And>x. \<lbrakk>x \<in> S; f x - h x \<ge> d\<rbrakk> \<Longrightarrow> 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 (\<lambda>x. h x + g x)"
+        using contg continuous_map_add continuous_map_in_subtopology that
+        unfolding good_def by blast
+      show "\<bar>f x - (h x + g x)\<bar> \<le> c * (2 / 3) ^ Suc n" if "x \<in> S" for x
+      proof -
+        have x: "x \<in> topspace X"
+          using \<open>S \<subseteq> topspace X\<close> that by auto
+        have "\<bar>f x - h x\<bar> \<le> 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 "\<bar>f x - (h x + g x)\<bar> \<le> d + d"
+          unfolding d_def by linarith
+        then show ?thesis 
+          by (simp add: d_def)
+      qed
+      show "\<bar>h x + g x - h x\<bar> \<le> c * (2 / 3) ^ n / 3" if "x \<in> topspace X" for x
+        using that d_def g_le_d by auto
+    qed
+  qed
+  then obtain nxtg where nxtg: "\<And>h n. good h n \<Longrightarrow> 
+          good (nxtg h n) (Suc n) \<and> (\<forall>x \<in> topspace X. \<bar>nxtg h n x - h x\<bar> \<le> c * (2/3)^n / 3)"
+    by metis
+  define g where "g \<equiv> rec_nat (\<lambda>x. 0) (\<lambda>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 *: "\<And>n x. x \<in> topspace X \<Longrightarrow> \<bar>g(Suc n) x - g n x\<bar> \<le> c * (2/3) ^ n / 3"
+    using nxtg g_Suc good by force
+  obtain h where conth:  "continuous_map X euclideanreal h"
+    and h: "\<And>\<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>topspace X. dist (g n x) (h x) < \<epsilon>"
+  proof (rule Met_TC.continuous_map_uniformly_Cauchy_limit)
+    show "\<forall>\<^sub>F n in sequentially. continuous_map X (Met_TC.mtopology) (g n)"
+      using good good_def by fastforce
+    show "\<exists>N. \<forall>m n x. N \<le> m \<longrightarrow> N \<le> n \<longrightarrow> x \<in> topspace X \<longrightarrow> dist (g m x) (g n x) < \<epsilon>"
+      if "\<epsilon> > 0" for \<epsilon> 
+    proof -
+      have "\<forall>\<^sub>F n in sequentially. \<bar>(2/3) ^ n\<bar> < \<epsilon>/c"
+      proof (rule Archimedean_eventually_pow_inverse)
+        show "0 < \<epsilon> / c"
+          by (simp add: \<open>0 < c\<close> that)
+      qed auto
+      then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>(2/3) ^ n\<bar> < \<epsilon>/c"
+        by (meson eventually_sequentially order_le_less_trans)
+      have "\<bar>g m x - g n x\<bar> < \<epsilon>"
+        if "N \<le> m" "N \<le> n" and x: "x \<in> topspace X" "m \<le> n" for m n x
+      proof (cases "m < n")
+        case True
+        have 23: "(\<Sum>k = m..<n. (2/3)^k) = 3 * ((2/3) ^ m - (2/3::real) ^ n)"
+          using \<open>m \<le> n\<close>
+          by (induction n) (auto simp: le_Suc_eq)
+        have "\<bar>g m x - g n x\<bar> \<le> \<bar>\<Sum>k = m..<n. g (Suc k) x - g k x\<bar>"
+          by (subst sum_Suc_diff' [OF \<open>m \<le> n\<close>]) linarith
+        also have "\<dots> \<le> (\<Sum>k = m..<n. \<bar>g (Suc k) x - g k x\<bar>)"
+          by (rule sum_abs)
+        also have "\<dots> \<le> (\<Sum>k = m..<n. c * (2/3)^k / 3)"
+          by (meson "*" sum_mono x(1))
+        also have "\<dots> = (c/3) * (\<Sum>k = m..<n. (2/3)^k)"
+          by (simp add: sum_distrib_left)
+        also have "\<dots> = (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 \<open>0 < c\<close> by auto
+        also have "\<dots> < \<epsilon>"
+          using N [OF \<open>N \<le> m\<close>] \<open>0 < c\<close> by (simp add: field_simps)
+        finally show ?thesis .
+      qed (use \<open>0 < \<epsilon>\<close> \<open>m \<le> n\<close> in auto)
+      then show ?thesis
+        by (metis dist_commute_lessI dist_real_def nle_le)
+    qed
+  qed auto
+  define \<phi> where "\<phi> \<equiv> \<lambda>x. max a (min (h x) b)"
+  show thesis
+  proof
+    show "continuous_map X euclidean \<phi>"
+      unfolding \<phi>_def using conth by (intro continuous_intros) auto
+    show "\<phi> x = f x" if "x \<in> S" for x 
+    proof -
+      have x: "x \<in> topspace X"
+        using \<open>closedin X S\<close> closedin_subset that by blast
+      have "h x = f x"
+      proof (rule Met_TC.limitin_metric_unique)
+        show "limitin Met_TC.mtopology (\<lambda>n. g n x) (h x) sequentially"
+          using h x by (force simp: tendsto_iff eventually_sequentially)
+        show "limitin Met_TC.mtopology (\<lambda>n. g n x) (f x) sequentially"
+        proof (clarsimp simp: tendsto_iff)
+          fix \<epsilon>::real
+          assume "\<epsilon> > 0"
+          then have "\<forall>\<^sub>F n in sequentially. \<bar>(2/3) ^ n\<bar> < \<epsilon>/c"
+            by (intro Archimedean_eventually_pow_inverse) (auto simp: \<open>c > 0\<close>)
+          then show "\<forall>\<^sub>F n in sequentially. dist (g n x) (f x) < \<epsilon>"
+            apply eventually_elim
+            by (smt (verit) good x good_def \<open>c > 0\<close> dist_real_def mult.commute pos_less_divide_eq that)
+        qed
+      qed auto
+      then show ?thesis
+        using that fim by (auto simp: \<phi>_def)
+    qed
+    then show "\<phi> ` topspace X \<subseteq> {a..b}"
+      using fim \<open>a \<le> b\<close> by (auto simp: \<phi>_def)
+  qed
+qed
+
+
+lemma Tietze_extension_realinterval:
+  assumes XS: "normal_space X" "closedin X S" and T: "is_interval T" "T \<noteq> {}" 
+    and contf: "continuous_map (subtopology X S) euclideanreal f" 
+    and "f ` S \<subseteq> T"
+  obtains g where "continuous_map X euclideanreal g"  "g ` topspace X \<subseteq> T"  "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+  define \<Phi> where 
+        "\<Phi> \<equiv> \<lambda>T::real set. \<forall>f. continuous_map (subtopology X S) euclidean f \<longrightarrow> f`S \<subseteq> T
+               \<longrightarrow> (\<exists>g. continuous_map X euclidean g \<and> g ` topspace X \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x))"
+  have "\<Phi> T"
+    if *: "\<And>T. \<lbrakk>bounded T; is_interval T; T \<noteq> {}\<rbrakk> \<Longrightarrow> \<Phi> T"
+      and "is_interval T" "T \<noteq> {}" for T
+    unfolding \<Phi>_def
+  proof (intro strip)
+    fix f
+    assume contf: "continuous_map (subtopology X S) euclideanreal f"
+      and "f ` S \<subseteq> T"
+    have \<Phi>T: "\<Phi> ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
+    proof (rule *)
+      show "bounded ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
+        using shrink_range [of T] by (force intro: boundedI [where B=1])
+      show "is_interval ((\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T)"
+        using connected_shrink that(2) is_interval_connected_1 by blast
+      show "(\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T \<noteq> {}"
+        using \<open>T \<noteq> {}\<close> by auto
+    qed
+    moreover have "continuous_map (subtopology X S) euclidean ((\<lambda>x. x / (1 + \<bar>x\<bar>)) \<circ> f)"
+      by (metis contf continuous_map_compose continuous_map_into_fulltopology continuous_map_real_shrink)
+    moreover have "((\<lambda>x. x / (1 + \<bar>x\<bar>)) \<circ> f) ` S \<subseteq> (\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T"
+      using \<open>f ` S \<subseteq> T\<close> by auto
+    ultimately obtain g 
+       where contg: "continuous_map X euclidean g" 
+         and gim: "g ` topspace X \<subseteq> (\<lambda>x. x / (1 + \<bar>x\<bar>)) ` T"
+         and geq: "\<And>x. x \<in> S \<Longrightarrow> g x = ((\<lambda>x. x / (1 + \<bar>x\<bar>)) \<circ> f) x"
+      using \<Phi>T unfolding \<Phi>_def by force
+    show "\<exists>g. continuous_map X euclideanreal g \<and> g ` topspace X \<subseteq> T \<and> (\<forall>x\<in>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 ((\<lambda>x. x / (1 - \<bar>x\<bar>)) \<circ> g)"
+        by (rule continuous_map_compose) (auto simp: continuous_on_real_grow)
+      show "((\<lambda>x. x / (1 - \<bar>x\<bar>)) \<circ> g) ` topspace X \<subseteq> T"
+        using gim real_grow_shrink by fastforce
+      show "\<forall>x\<in>S. ((\<lambda>x. x / (1 - \<bar>x\<bar>)) \<circ> g) x = f x"
+        using geq real_grow_shrink by force
+    qed
+  qed
+  moreover have "\<Phi> T"
+    if "bounded T" "is_interval T" "T \<noteq> {}" for T
+    unfolding \<Phi>_def
+  proof (intro strip)
+    fix f
+    assume contf: "continuous_map (subtopology X S) euclideanreal f"
+      and "f ` S \<subseteq> T"
+    obtain a b where ab: "closure T = {a..b}"
+      by (meson \<open>bounded T\<close> \<open>is_interval T\<close> compact_closure connected_compact_interval_1 
+            connected_imp_connected_closure is_interval_connected)
+    with \<open>T \<noteq> {}\<close> have "a \<le> b" by auto
+    have "f ` S \<subseteq> {a..b}"
+      using \<open>f ` S \<subseteq> T\<close> ab closure_subset by auto
+    then obtain g where contg: "continuous_map X euclideanreal g"
+      and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" and gim: "g ` topspace X \<subseteq> {a..b}"
+      using Tietze_extension_closed_real_interval [OF XS contf _ \<open>a \<le> b\<close>] by metis
+    define W where "W \<equiv> {x \<in> topspace X. g x \<in> closure T - T}"
+    have "{a..b} - {a, b} \<subseteq> 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 \<open>f ` S \<subseteq> T\<close> gf by blast
+    ultimately obtain h :: "'a \<Rightarrow> real" 
+      where conth: "continuous_map X (top_of_set {0..1}) h" 
+            and him: "h ` W \<subseteq> {0}" "h ` S \<subseteq> {1}"
+      by (metis XS normal_space_iff_Urysohn) 
+    then have him01: "h ` topspace X \<subseteq> {0..1}"
+      by (meson continuous_map_in_subtopology)
+    obtain z where "z \<in> T"
+      using \<open>T \<noteq> {}\<close> by blast
+    define g' where "g' \<equiv> \<lambda>x. z + h x * (g x - z)"
+    show "\<exists>g. continuous_map X euclidean g \<and> g ` topspace X \<subseteq> T \<and> (\<forall>x\<in>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 \<subseteq> T"
+        unfolding g'_def 
+      proof clarify
+        fix x
+        assume "x \<in> topspace X"
+        show "z + h x * (g x - z) \<in> T"
+        proof (cases "g x \<in> T")
+          case True
+          define w where "w \<equiv> z + h x * (g x - z)"
+          have "\<bar>h x\<bar> * \<bar>g x - z\<bar> \<le> \<bar>g x - z\<bar>" "\<bar>1 - h x\<bar> * \<bar>g x - z\<bar> \<le> \<bar>g x - z\<bar>"
+            using him01 \<open>x \<in> topspace X\<close> by (force simp: intro: mult_left_le_one_le)+
+          then consider "z \<le> w \<and> w \<le> g x" | "g x \<le> w \<and> w \<le> z"
+            unfolding w_def by (smt (verit) left_diff_distrib mult_cancel_right2 mult_minus_right zero_less_mult_iff)
+          then show ?thesis
+            using \<open>is_interval T\<close> unfolding w_def is_interval_1 by (metis True \<open>z \<in> T\<close>)
+        next
+          case False
+          then have "g x \<in> closure T"
+            using \<open>x \<in> topspace X\<close> ab gim by blast
+          then have "h x = 0"
+            using him False \<open>x \<in> topspace X\<close> by (auto simp: W_def image_subset_iff)
+          then show ?thesis
+            by (simp add: \<open>z \<in> T\<close>)
+        qed
+      qed
+      show "\<forall>x\<in>S. g' x = f x"
+        using gf him by (auto simp: W_def g'_def)
+    qed 
+  qed
+  ultimately show thesis
+    using assms that unfolding \<Phi>_def by best
+qed
+
+lemma normal_space_iff_Tietze:
+   "normal_space X \<longleftrightarrow>
+    (\<forall>f S. closedin X S \<and>
+           continuous_map (subtopology X S) euclidean f
+           \<longrightarrow> (\<exists>g:: 'a \<Rightarrow> real. continuous_map X euclidean g \<and> (\<forall>x \<in> S. g x = f x)))" 
+   (is "?lhs \<longleftrightarrow> ?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 \<union> T)"
+      by (simp add: closedin_Un)
+    moreover 
+    have "continuous_map (subtopology X (S \<union> T)) euclideanreal (\<lambda>x. if x \<in> S then 0 else 1)"
+      unfolding continuous_map_closedin
+    proof (intro conjI strip)
+      fix C :: "real set"
+      define D where "D \<equiv> {x \<in> topspace X. if x \<in> S then 0 \<in> C else x \<in> T \<and> 1 \<in> C}"
+      have "D \<in> {{}, S, T, S \<union> T}"
+        unfolding D_def
+        using closedin_subset [OF \<open>closedin X S\<close>] closedin_subset [OF \<open>closedin X T\<close>] \<open>disjnt S T\<close>
+        by (auto simp: disjnt_iff)
+      then have "closedin X D"
+        using \<open>closedin X S\<close> \<open>closedin X T\<close> closedin_empty by blast
+      with closedin_subset_topspace
+      show "closedin (subtopology X (S \<union> T)) {x \<in> topspace (subtopology X (S \<union> T)). (if x \<in> S then 0::real else 1) \<in> 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 \<Rightarrow> real"  where 
+      contg: "continuous_map X euclidean g" and gf: "\<forall>x \<in> S \<union> T. g x = (if x \<in> S then 0 else 1)"
+      using R by blast
+    then show "\<exists>f. continuous_map X euclideanreal f \<and> f ` S \<subseteq> {0} \<and> f ` T \<subseteq> {1}"
+      by (smt (verit) Un_iff \<open>disjnt S T\<close> disjnt_iff image_subset_iff insert_iff)
+  qed
+qed
+
+subsection \<open>random metric space stuff\<close>
+
+
+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 \<subseteq> M" and S: "\<forall>K. compactin mtopology K \<longrightarrow> closedin (subtopology mtopology K) (K \<inter> S)"
+    have "l \<in> S"
+      if \<sigma>: "range \<sigma> \<subseteq> S" and l: "limitin mtopology \<sigma> l sequentially" for \<sigma> l
+    proof -
+      define K where "K \<equiv> insert l (range \<sigma>)"
+      interpret Submetric M d K
+      proof
+        show "K \<subseteq> M"
+          unfolding K_def using l limitin_mspace \<open>S \<subseteq> M\<close> \<sigma> by blast
+      qed
+      have "compactin mtopology K"
+        unfolding K_def using \<open>S \<subseteq> M\<close> \<sigma>
+        by (force intro: compactin_sequence_with_limit [OF l])
+      then have *: "closedin sub.mtopology (K \<inter> S)"
+        by (simp add: S mtopology_submetric)
+      have "\<sigma> n \<in> K \<inter> S" for n
+        by (simp add: K_def range_subsetD \<sigma>)
+      moreover have "limitin sub.mtopology \<sigma> l sequentially"
+        using l 
+        unfolding sub.limit_metric_sequentially limit_metric_sequentially
+        by (force simp: K_def)
+      ultimately have "l \<in> K \<inter> S"
+        by (meson * \<sigma> 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 \<open>S \<subseteq> M\<close> 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\<open>Hereditarily normal spaces\<close>
+
+lemma hereditarily_B:
+  assumes "\<And>S T. separatedin X S T
+      \<Longrightarrow> \<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+  shows "hereditarily normal_space X"
+  unfolding hereditarily_def
+proof (intro strip)
+  fix W
+  assume "W \<subseteq> 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 \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+      using assms [of S T] by (meson separatedin_subtopology)
+    then show "\<exists>U V. openin (subtopology X W) U \<and> openin (subtopology X W) V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> 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: "\<And>U. openin X U \<Longrightarrow> normal_space (subtopology X U)"
+  shows "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+proof -
+  define ST where "ST \<equiv> X closure_of S \<inter> X closure_of T"
+  have subX: "S \<subseteq> topspace X" "T \<subseteq> topspace X"
+    by (meson \<open>separatedin X S T\<close> separation_closedin_Un_gen)+
+  have sub: "S \<subseteq> topspace X - ST" "T \<subseteq> topspace X - ST"
+    unfolding ST_def
+    by (metis Diff_mono Diff_triv \<open>separatedin X S T\<close> 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 \<longleftrightarrow> (\<forall>U. openin X U \<longrightarrow> normal_space(subtopology X U))"
+  by (metis hereditarily_B hereditarily_C hereditarily)
+
+lemma hereditarily_normal_separation:
+  "hereditarily normal_space X \<longleftrightarrow>
+        (\<forall>S T. separatedin X S T
+             \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V))"
+  by (metis hereditarily_B hereditarily_C hereditarily)
+
+
+lemma metrizable_imp_hereditarily_normal_space:
+   "metrizable_space X \<Longrightarrow> hereditarily normal_space X"
+  by (simp add: hereditarily metrizable_imp_normal_space metrizable_space_subtopology)
+
+lemma metrizable_space_separation:
+   "\<lbrakk>metrizable_space X; separatedin X S T\<rbrakk>
+    \<Longrightarrow> \<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+  by (metis hereditarily hereditarily_C metrizable_imp_hereditarily_normal_space)
+
+lemma hereditarily_normal_separation_pairwise:
+   "hereditarily normal_space X \<longleftrightarrow>
+    (\<forall>\<U>. finite \<U> \<and> (\<forall>S \<in> \<U>. S \<subseteq> topspace X) \<and> pairwise (separatedin X) \<U>
+        \<longrightarrow> (\<exists>\<F>. (\<forall>S \<in> \<U>. openin X (\<F> S) \<and> S \<subseteq> \<F> S) \<and>
+                pairwise (\<lambda>S T. disjnt (\<F> S) (\<F> T)) \<U>))"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume L: ?lhs 
+  show ?rhs
+  proof clarify
+    fix \<U>
+    assume "finite \<U>" and \<U>: "\<forall>S\<in>\<U>. S \<subseteq> topspace X" 
+      and pw\<U>: "pairwise (separatedin X) \<U>"
+    have "\<exists>V W. openin X V \<and> openin X W \<and> S \<subseteq> V \<and>
+                    (\<forall>T. T \<in> \<U> \<and> T \<noteq> S \<longrightarrow> T \<subseteq> W) \<and> disjnt V W" 
+      if "S \<in> \<U>" for S
+    proof -
+      have "separatedin X S (\<Union>(\<U> - {S}))"
+        by (metis \<U> \<open>finite \<U>\<close> pw\<U> 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 \<F> \<G> 
+        where *: "\<And>S. S \<in> \<U> \<Longrightarrow> S \<subseteq> \<F> S \<and> (\<forall>T. T \<in> \<U> \<and> T \<noteq> S \<longrightarrow> T \<subseteq> \<G> S)" 
+        and ope: "\<And>S. S \<in> \<U> \<Longrightarrow> openin X (\<F> S) \<and> openin X (\<G> S)" 
+        and dis: "\<And>S. S \<in> \<U> \<Longrightarrow> disjnt (\<F> S) (\<G> S)" 
+      by metis
+    define \<H> where "\<H> \<equiv> \<lambda>S. \<F> S \<inter> (\<Inter>T \<in> \<U> - {S}. \<G> T)"
+    show "\<exists>\<F>. (\<forall>S\<in>\<U>. openin X (\<F> S) \<and> S \<subseteq> \<F> S) \<and> pairwise (\<lambda>S T. disjnt (\<F> S) (\<F> T)) \<U>"
+    proof (intro exI conjI strip)
+      show "openin X (\<H> S)" if "S \<in> \<U>" for S
+        unfolding \<H>_def 
+        by (smt (verit) ope that DiffD1 \<open>finite \<U>\<close> finite_Diff finite_imageI imageE openin_Int_Inter)
+      show "S \<subseteq> \<H> S" if "S \<in> \<U>" for S
+        unfolding \<H>_def using "*" that by auto 
+    show "pairwise (\<lambda>S T. disjnt (\<H> S) (\<H> T)) \<U>"
+      using dis by (fastforce simp: disjnt_iff pairwise_alt \<H>_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 "\<exists>U V. openin X U \<and> openin X V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> disjnt U V"
+    proof (cases "T=S")
+      case True
+      then show ?thesis
+        using \<open>separatedin X S T\<close> by force
+    next
+      case False
+      have "pairwise (separatedin X) {S, T}"
+        by (simp add: \<open>separatedin X S T\<close> pairwise_insert separatedin_sym)
+      moreover have "\<forall>S\<in>{S, T}. S \<subseteq> topspace X"
+        by (metis \<open>separatedin X S T\<close> 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:
+   "\<lbrakk>hereditarily normal_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> 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 \<and> 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\<open>Completely regular spaces\<close>
+
+definition completely_regular_space where
+ "completely_regular_space X \<equiv>
+    \<forall>S x. closedin X S \<and> x \<in> topspace X - S
+          \<longrightarrow> (\<exists>f::'a\<Rightarrow>real. continuous_map X (top_of_set {0..1}) f \<and>
+                  f x = 0 \<and> (f ` S \<subseteq> {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: "(\<forall>x \<in> topspace X. g(f x) = x) \<and> (\<forall>y \<in> 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 \<in> topspace Y" and "x \<notin> S"
+    then have "closedin X (g`S)"
+      using hmg homeomorphic_map_closedness_eq by blast
+    moreover have "g x \<notin> g`S"
+      by (meson A x \<open>x \<notin> S\<close> closedin_subset hmg homeomorphic_imp_injective_map inj_on_image_mem_iff)
+    ultimately obtain \<phi> where \<phi>: "continuous_map X (top_of_set {0..1::real}) \<phi> \<and> \<phi> (g x) = 0 \<and> \<phi> ` g`S \<subseteq> {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}) (\<phi> \<circ> g)"
+      by (meson continuous_map_compose hmg homeomorphic_imp_continuous_map)
+    then show "\<exists>\<psi>. continuous_map Y (top_of_set {0..1::real}) \<psi> \<and> \<psi> x = 0 \<and> \<psi> ` S \<subseteq> {1}"
+      by (metis \<phi> comp_apply image_comp)
+  qed
+qed
+
+lemma homeomorphic_completely_regular_space:
+  assumes "X homeomorphic_space Y"
+  shows "completely_regular_space X \<longleftrightarrow> completely_regular_space Y"
+  by (meson assms homeomorphic_completely_regular_space_aux homeomorphic_space_sym)
+
+lemma completely_regular_space_alt:
+   "completely_regular_space X \<longleftrightarrow>
+     (\<forall>S x. closedin X S \<longrightarrow> x \<in> topspace X - S
+           \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}))"
+proof -
+  have "\<exists>f. continuous_map X (top_of_set {0..1::real}) f \<and> f x = 0 \<and> f ` S \<subseteq> {1}" 
+    if "closedin X S" "x \<in> topspace X - S" and f: "continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
+    for S x f
+  proof (intro exI conjI)
+    show "continuous_map X (top_of_set {0..1}) (\<lambda>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 \<open>As above, but with @{term openin}\<close>
+lemma completely_regular_space_alt':
+   "completely_regular_space X \<longleftrightarrow>
+     (\<forall>S x. openin X S \<longrightarrow> x \<in> S
+           \<longrightarrow> (\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` (topspace X - S) \<subseteq> {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 \<noteq> b"
+  shows "completely_regular_space X \<longleftrightarrow>
+         (\<forall>S x. closedin X S \<longrightarrow> x \<in> topspace X - S
+               \<longrightarrow> (\<exists>f. continuous_map X euclidean f \<and> f x = a \<and> (f ` S \<subseteq> {b})))"
+proof -
+  have "\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}" 
+    if "closedin X S" "x \<in> topspace X - S" 
+        and f: "continuous_map X euclidean f \<and> f x = a \<and> f ` S \<subseteq> {b}"
+    for S x f
+  proof (intro exI conjI)
+    show "continuous_map X euclideanreal ((\<lambda>x. inverse(b - a) * (x - a)) \<circ> f)"
+      using that by (intro continuous_intros) auto
+  qed (use that assms in auto)
+  moreover
+  have "\<exists>f. continuous_map X euclidean f \<and> f x = a \<and> f ` S \<subseteq> {b}" 
+    if "closedin X S" "x \<in> topspace X - S" 
+        and f: "continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
+    for S x f
+  proof (intro exI conjI)
+    show "continuous_map X euclideanreal ((\<lambda>x. a + (b - a) * x) \<circ> 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 \<open>As above, but with @{term openin}\<close>
+lemma completely_regular_space_gen_alt':
+  fixes a b::real
+  assumes "a \<noteq> b"
+  shows "completely_regular_space X \<longleftrightarrow>
+         (\<forall>S x. openin X S \<longrightarrow> x \<in> S
+               \<longrightarrow> (\<exists>f. continuous_map X euclidean f \<and> f x = a \<and> (f ` (topspace X - S) \<subseteq> {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 \<longleftrightarrow>
+         (\<forall>S x. closedin X S \<and> x \<in> topspace X - S
+               \<longrightarrow> (\<exists>f. continuous_map X (top_of_set {a..b}) f \<and> f x = a \<and> f ` S \<subseteq> {b}))"
+proof -
+  have "\<exists>f. continuous_map X (top_of_set {a..b}) f \<and> f x = a \<and> f ` S \<subseteq> {b}" 
+    if "closedin X S" "x \<in> topspace X - S" 
+      and f: "continuous_map X euclidean f \<and> f x = a \<and> f ` S \<subseteq> {b}"
+    for S x f
+  proof (intro exI conjI)
+    show "continuous_map X (top_of_set {a..b}) (\<lambda>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 \<notin> S"
+  assume "x \<in> topspace X" 
+  then have "closedin X {x}"
+    by (simp add: \<open>t1_space X\<close> closedin_t1_singleton)
+  with A \<open>normal_space X\<close> have "\<exists>f. continuous_map X euclideanreal f \<and> f ` {x} \<subseteq> {0} \<and> f ` S \<subseteq> {1}"
+    using assms unfolding normal_space_iff_Urysohn_alt disjnt_iff by blast
+  then show "\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {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 \<notin> S" "x \<in> topspace X" 
+  then obtain U C where "openin X U" "closedin X C" "x \<in> U" "U \<subseteq> C" "C \<subseteq> 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 \<and> f ` C \<subseteq> {0} \<and> f ` S \<subseteq> {1}"
+    using assms unfolding normal_space_iff_Urysohn_alt
+    by (metis Diff_iff \<open>closedin X S\<close> disjnt_iff subsetD)
+  then show "\<exists>f. continuous_map X euclideanreal f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
+    by (meson \<open>U \<subseteq> C\<close> \<open>x \<in> U\<close> image_subset_iff singletonD subsetD)
+qed
+
+lemma normal_imp_completely_regular_space_gen:
+   "\<lbrakk>normal_space X; t1_space X \<or> Hausdorff_space X \<or> regular_space X\<rbrakk> \<Longrightarrow> 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:
+   "\<lbrakk>normal_space X; Hausdorff_space X \<or> regular_space X\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<in> topspace (subtopology X S)" and "x \<notin> A"
+  then obtain T where "closedin X T" "A = S \<inter> T" "x \<in> topspace X" "x \<in> S"
+    by (force simp: closedin_subtopology_alt image_iff)
+  then show "\<exists>f. continuous_map (subtopology X S) (top_of_set {0::real..1}) f \<and> f x = 0 \<and> f ` A \<subseteq> {1}"
+    using assms \<open>x \<notin> A\<close>  
+    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:
+   " \<lbrakk>retraction_map X Y r; completely_regular_space X\<rbrakk> \<Longrightarrow> 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 *: "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
+    if contf: "continuous_map X euclideanreal f" and a: "a \<in> topspace X - C" and "closedin X C"
+      and fim: "f ` topspace X \<subseteq> {0..1}" and f0: "f a = 0" and f1: "f ` C \<subseteq> {1}"
+    for C a f
+  proof (intro exI conjI)
+    show "openin X {x \<in> topspace X. f x \<in> {..<1 / 2}}" "openin X {x \<in> topspace X. f x \<in> {1 / 2<..}}"
+      using openin_continuous_map_preimage [OF contf]
+      by (meson open_lessThan open_greaterThan open_openin)+
+    show "a \<in> {x \<in> topspace X. f x \<in> {..<1 / 2}}"
+      using a f0 by auto
+    show "C \<subseteq> {x \<in> topspace X. f x \<in> {1 / 2<..}}"
+      using \<open>closedin X C\<close> 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
+
+
+lemma locally_compact_regular_imp_completely_regular_space:
+  assumes "locally_compact_space X" "Hausdorff_space X \<or> regular_space X"
+  shows "completely_regular_space X"
+  unfolding completely_regular_space_def
+proof clarify
+  fix S x
+  assume "closedin X S" and "x \<in> topspace X" and "x \<notin> S"
+  have "regular_space X"
+    using assms locally_compact_Hausdorff_imp_regular_space by blast
+  then have nbase: "neighbourhood_base_of (\<lambda>C. compactin X C \<and> 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 \<in> U" "U \<subseteq> M" "M \<subseteq> topspace X - S"
+    unfolding neighbourhood_base_of by (metis (no_types, lifting) Diff_iff \<open>closedin X S\<close> \<open>x \<in> topspace X\<close> \<open>x \<notin> S\<close> closedin_def)
+  then have "M \<subseteq> topspace X"
+    by blast
+  obtain V K where "openin X V" "closedin X K" "x \<in> V" "V \<subseteq> K" "K \<subseteq> U"
+    by (metis (no_types, lifting) \<open>openin X U\<close> \<open>x \<in> U\<close> neighbourhood_base_of nbase)
+  have "compact_space (subtopology X M)"
+    by (simp add: \<open>compactin X M\<close> compact_space_subtopology)
+  then have "normal_space (subtopology X M)"
+    by (simp add: \<open>regular_space X\<close> compact_Hausdorff_or_regular_imp_normal_space regular_space_subtopology)
+  moreover have "closedin (subtopology X M) K"
+    using \<open>K \<subseteq> U\<close> \<open>U \<subseteq> M\<close> \<open>closedin X K\<close> closedin_subset_topspace by fastforce
+  moreover have "closedin (subtopology X M) (M - U)"
+    by (simp add: \<open>closedin X M\<close> \<open>openin X U\<close> closedin_diff closedin_subset_topspace)
+  moreover have "disjnt K (M - U)"
+    by (meson DiffD2 \<open>K \<subseteq> U\<close> disjnt_iff subsetD)
+  ultimately obtain f::"'a\<Rightarrow>real" where contf: "continuous_map (subtopology X M) (top_of_set {0..1}) f" 
+    and f0: "f ` K \<subseteq> {0}" and f1: "f ` (M - U) \<subseteq> {1}"
+    using Urysohn_lemma [of "subtopology X M" K "M-U" 0 1] by auto
+  then obtain g::"'a\<Rightarrow>real" where contg: "continuous_map (subtopology X M) euclidean g" and gim: "g ` M \<subseteq> {0..1}"
+    and g0: "\<And>x. x \<in> K \<Longrightarrow> g x = 0" and g1: "\<And>x. \<lbrakk>x \<in> M; x \<notin> U\<rbrakk> \<Longrightarrow> g x = 1"
+    using \<open>M \<subseteq> topspace X\<close> by (force simp add: continuous_map_in_subtopology image_subset_iff)
+  show "\<exists>f::'a\<Rightarrow>real. continuous_map X (top_of_set {0..1}) f \<and> f x = 0 \<and> f ` S \<subseteq> {1}"
+  proof (intro exI conjI)
+    show "continuous_map X (top_of_set {0..1}) (\<lambda>x. if x \<in> 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 \<in> topspace X. (if x \<in> M then g x else 1) \<in> C} = {x \<in> M. g x \<in> C} \<union> (if 1 \<in> C then topspace X - U else {})"
+        using \<open>U \<subseteq> M\<close> \<open>M \<subseteq> topspace X\<close> g1 by auto
+      show "closedin X {x \<in> topspace X. (if x \<in> M then g x else 1) \<in> 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 \<in> M. g x \<in> C}"
+          using closedin_continuous_map_preimage_gen [OF contg] \<open>M \<subseteq> topspace X\<close> by auto
+        then show "closedin X {x \<in> M. g x \<in> C}"
+          using \<open>closedin X M\<close> closedin_trans_full by blast
+      qed (use \<open>openin X U\<close> in force)
+    qed (use gim in force)
+    show "(if x \<in> M then g x else 1) = 0"
+      using \<open>U \<subseteq> M\<close> \<open>V \<subseteq> K\<close> g0 \<open>x \<in> U\<close> \<open>x \<in> V\<close> by auto
+    show "(\<lambda>x. if x \<in> M then g x else 1) ` S \<subseteq> {1}"
+      using \<open>M \<subseteq> topspace X - S\<close> by auto
+  qed
+qed
+
+lemma completely_regular_eq_regular_space:
+   "locally_compact_space X
+        \<Longrightarrow> (completely_regular_space X \<longleftrightarrow> 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) \<longleftrightarrow>
+      topspace (prod_topology X Y) = {} \<or>
+      completely_regular_space X \<and> 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 "topspace(prod_topology X Y) = {}")
+    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) \<in> W"
+      then obtain U V where "openin X U" "openin Y V" "x \<in> U" "y \<in> V" "U\<times>V \<subseteq> W"
+        by (force simp: openin_prod_topology_alt)
+      then have "x \<in> topspace X" "y \<in> topspace Y"
+        using openin_subset by fastforce+
+      obtain f where contf: "continuous_map X euclideanreal f" and "f x = 0" 
+        and f1: "\<And>x. x \<in> topspace X \<Longrightarrow> x \<notin> U \<Longrightarrow> f x = 1"
+        using X \<open>openin X U\<close> \<open>x \<in> U\<close> 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: "\<And>y. y \<in> topspace Y \<Longrightarrow> y \<notin> V \<Longrightarrow> g y = 1"
+        using Y \<open>openin Y V\<close> \<open>y \<in> V\<close> unfolding completely_regular_space_alt'
+        by (smt (verit, best) Diff_iff image_subset_iff singletonD)
+      define h where "h \<equiv> \<lambda>(x,y). 1 - (1 - f x) * (1 - g y)"
+      show "\<exists>h. continuous_map (prod_topology X Y) euclideanreal h \<and> h (x,y) = 0 \<and> h ` (topspace (prod_topology X Y) - W) \<subseteq> {1}"
+      proof (intro exI conjI)
+        have "continuous_map (prod_topology X Y) euclideanreal (f \<circ> fst)"
+          using contf continuous_map_of_fst by blast
+        moreover
+        have "continuous_map (prod_topology X Y) euclideanreal (g \<circ> 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 \<open>f x = 0\<close> \<open>g y = 0\<close>)
+        show "h ` (topspace (prod_topology X Y) - W) \<subseteq> {1}"
+          using \<open>U \<times> V \<subseteq> W\<close> f1 g1 by (force simp: h_def)
+      qed
+    qed
+  qed (force simp: completely_regular_space_def)
+qed
+
+
+lemma completely_regular_space_product_topology:
+   "completely_regular_space (product_topology X I) \<longleftrightarrow>
+    (\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {} \<or> (\<forall>i \<in> I. completely_regular_space (X i))" 
+   (is "?lhs \<longleftrightarrow> ?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 "(\<Pi>\<^sub>E i\<in>I. topspace(X i)) = {}")
+    case False
+    show ?thesis
+      unfolding completely_regular_space_alt'
+    proof clarify
+      fix W x
+      assume W: "openin (product_topology X I) W" and "x \<in> W"
+      then obtain U where finU: "finite {i \<in> I. U i \<noteq> topspace (X i)}" 
+             and ope: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (U i)" 
+             and x: "x \<in> Pi\<^sub>E I U" and "Pi\<^sub>E I U \<subseteq> W"
+        by (auto simp: openin_product_topology_alt)
+      have "\<forall>i \<in> I. openin (X i) (U i) \<and> x i \<in> U i
+              \<longrightarrow> (\<exists>f. continuous_map (X i) euclideanreal f \<and>
+                       f (x i) = 0 \<and> (\<forall>x \<in> topspace(X i). x \<notin> U i \<longrightarrow> f x = 1))"
+        using R unfolding completely_regular_space_alt'
+        by (smt (verit) DiffI False image_subset_iff singletonD)
+      with ope x have "\<And>i. \<exists>f. i \<in> I \<longrightarrow> continuous_map (X i) euclideanreal f \<and>
+              f (x i) = 0 \<and> (\<forall>x \<in> topspace (X i). x \<notin> U i \<longrightarrow> f x = 1)"
+        by auto
+      then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (X i) euclideanreal (f i) \<and>
+                                             f i (x i) = 0 \<and> (\<forall>x \<in> topspace (X i). x \<notin> U i \<longrightarrow> f i x = 1)"
+        by metis
+      define h where "h \<equiv> \<lambda>z. 1 - prod (\<lambda>i. 1 - f i (z i)) {i\<in>I. U i \<noteq> topspace(X i)}"
+      show "\<exists>h. continuous_map (product_topology X I) euclideanreal h \<and> h x = 0 \<and>
+                     h ` (topspace (product_topology X I) - W) \<subseteq> {1}"
+      proof (intro conjI exI)
+        have "continuous_map (product_topology X I) euclidean (f i \<circ> (\<lambda>x. x i))" if "i\<in>I" for i
+          using f that
+          by (blast intro: continuous_intros continuous_map_product_projection)
+        then show "continuous_map (product_topology X I) euclideanreal h"
+          unfolding h_def o_def by (intro continuous_intros) (auto simp: finU)
+        show "h x = 0"
+          by (simp add: h_def f)
+        show "h ` (topspace (product_topology X I) - W) \<subseteq> {1}"
+          proof -
+          have "\<exists>i. i \<in> I \<and> U i \<noteq> topspace (X i) \<and> f i (x' i) = 1"
+            if "x' \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" "x' \<notin> W" for x'
+            using that \<open>Pi\<^sub>E I U \<subseteq> W\<close> by (smt (verit, best) PiE_iff f in_mono)
+          then show ?thesis
+            by (auto simp: f h_def finU)
+        qed
+      qed
+    qed      
+  qed (force simp: completely_regular_space_def)
+qed
+
+
+lemma (in Metric_space) t1_space_mtopology:
+   "t1_space mtopology"
+  using Hausdorff_space_mtopology t1_or_Hausdorff_space by blast
+
+
+subsection\<open>More generally, the k-ification functor\<close>
+
+definition kification_open 
+  where "kification_open \<equiv> 
+          \<lambda>X S. S \<subseteq> topspace X \<and> (\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> S))"
+
+definition kification 
+  where "kification X \<equiv> topology (kification_open X)"
+
+lemma istopology_kification_open: "istopology (kification_open X)"
+  unfolding istopology_def
+proof (intro conjI strip)
+  show "kification_open X (S \<inter> T)"
+    if "kification_open X S" and "kification_open X T" for S T
+    using that unfolding kification_open_def
+    by (smt (verit, best) inf.idem inf_commute inf_left_commute le_infI2 openin_Int)
+  show "kification_open X (\<Union> \<K>)" if "\<forall>K\<in>\<K>. kification_open X K" for \<K>
+    using that unfolding kification_open_def Int_Union by blast
+qed
+
+lemma openin_kification:
+   "openin (kification X) U \<longleftrightarrow>
+        U \<subseteq> topspace X \<and>
+        (\<forall>K. compactin X K \<longrightarrow> openin (subtopology X K) (K \<inter> U))"
+  by (metis topology_inverse' kification_def istopology_kification_open kification_open_def)
+
+lemma openin_kification_finer:
+   "openin X S \<Longrightarrow> openin (kification X) S"
+  by (simp add: openin_kification openin_subset openin_subtopology_Int2)
+
+lemma topspace_kification [simp]:
+   "topspace(kification X) = topspace X"
+  by (meson openin_kification openin_kification_finer openin_topspace subset_antisym)
+
+lemma closedin_kification:
+   "closedin (kification X) U \<longleftrightarrow>
+      U \<subseteq> topspace X \<and>
+      (\<forall>K. compactin X K \<longrightarrow> closedin (subtopology X K) (K \<inter> U))"
+proof (cases "U \<subseteq> topspace X")
+  case True
+  then show ?thesis
+    by (simp add: closedin_def Diff_Int_distrib inf_commute le_infI2 openin_kification)
+qed (simp add: closedin_def)
+
+lemma closedin_kification_finer: "closedin X S \<Longrightarrow> closedin (kification X) S"
+  by (simp add: closedin_def openin_kification_finer)
+
+lemma kification_eq_self: "kification X = X \<longleftrightarrow> k_space X"
+  unfolding fun_eq_iff openin_kification k_space_alt openin_inject [symmetric]
+  by (metis openin_closedin_eq)
+
+lemma compactin_kification [simp]:
+   "compactin (kification X) K \<longleftrightarrow> compactin X K" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: compactin_contractive openin_kification_finer)
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding compactin_def
+  proof (intro conjI strip)
+    show "K \<subseteq> topspace (kification X)"
+      by (simp add: R compactin_subset_topspace)
+    fix \<U>
+    assume \<U>: "Ball \<U> (openin (kification X)) \<and> K \<subseteq> \<Union> \<U>"
+    then have *: "\<And>U. U \<in> \<U> \<Longrightarrow> U \<subseteq> topspace X \<and> openin (subtopology X K) (K \<inter> U)"
+      by (simp add: R openin_kification)
+    have "K \<subseteq> topspace X" "compact_space (subtopology X K)"
+      using R compactin_subspace by force+
+    then have "\<exists>V. finite V \<and> V \<subseteq> (\<lambda>U. K \<inter> U) ` \<U> \<and> \<Union> V = topspace (subtopology X K)"
+      unfolding compact_space
+      by (smt (verit, del_insts) Int_Union \<U> * image_iff inf.order_iff inf_commute topspace_subtopology)
+    then show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> K \<subseteq> \<Union> \<F>"
+      by (metis Int_Union \<open>K \<subseteq> topspace X\<close> finite_subset_image inf.orderI topspace_subtopology_subset)
+  qed
+qed
+
+lemma compact_space_kification [simp]:
+   "compact_space(kification X) \<longleftrightarrow> compact_space X"
+  by (simp add: compact_space_def)
+
+lemma kification_kification [simp]:
+   "kification(kification X) = kification X"
+  unfolding openin_inject [symmetric]
+proof
+  fix U
+  show "openin (kification (kification X)) U = openin (kification X) U"
+  proof
+    show "openin (kification (kification X)) U \<Longrightarrow> openin (kification X) U"
+      by (metis compactin_kification inf_commute openin_kification openin_subtopology topspace_kification)
+  qed (simp add: openin_kification_finer)
+qed
+
+lemma k_space_kification [iff]: "k_space(kification X)"
+  using kification_eq_self by fastforce
+
+lemma continuous_map_into_kification:
+  assumes "k_space X"
+  shows "continuous_map X (kification Y) f \<longleftrightarrow> continuous_map X Y f" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: continuous_map_def openin_kification_finer)
+next
+  assume R: ?rhs
+  have "openin X {x \<in> topspace X. f x \<in> V}" if V: "openin (kification Y) V" for V
+  proof -
+    have "openin (subtopology X K) (K \<inter> {x \<in> topspace X. f x \<in> V})"
+      if "compactin X K" for K
+    proof -
+      have "compactin Y (f ` K)"
+        using R image_compactin that by blast
+      then have "openin (subtopology Y (f ` K)) (f ` K \<inter> V)"
+        by (meson V openin_kification)
+      then obtain U where U: "openin Y U" "f`K \<inter> V = U \<inter> f`K"
+        by (meson openin_subtopology)
+      show ?thesis
+        unfolding openin_subtopology
+      proof (intro conjI exI)
+        show "openin X {x \<in> topspace X. f x \<in> U}"
+          using R U openin_continuous_map_preimage_gen by (simp add: continuous_map_def)
+      qed (use U in auto)
+    qed
+    then show ?thesis
+      by (metis (full_types) Collect_subset assms k_space_open)
+  qed
+  with R show ?lhs
+    by (simp add: continuous_map_def)
+qed
+
+lemma continuous_map_from_kification:
+   "continuous_map X Y f \<Longrightarrow> continuous_map (kification X) Y f"
+  by (simp add: continuous_map_openin_preimage_eq openin_kification_finer)
+
+lemma continuous_map_kification:
+   "continuous_map X Y f \<Longrightarrow> continuous_map (kification X) (kification Y) f"
+  by (simp add: continuous_map_from_kification continuous_map_into_kification)
+
+lemma subtopology_kification_compact:
+  assumes "compactin X K"
+  shows "subtopology (kification X) K = subtopology X K"
+  unfolding openin_inject [symmetric]
+proof
+  fix U
+  show "openin (subtopology (kification X) K) U = openin (subtopology X K) U"
+    by (metis assms inf_commute openin_kification openin_subset openin_subtopology)
+qed
+
+
+lemma subtopology_kification_finer:
+  assumes "openin (subtopology (kification X) S) U"
+  shows "openin (kification (subtopology X S)) U"
+  using assms 
+  by (fastforce simp: openin_subtopology_alt image_iff openin_kification subtopology_subtopology compactin_subtopology)
+
+lemma proper_map_from_kification:
+  assumes "k_space Y"
+  shows "proper_map (kification X) Y f \<longleftrightarrow> proper_map X Y f"   (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: closed_map_def closedin_kification_finer proper_map_alt)
+next
+  assume R: ?rhs
+  have "compactin Y K \<Longrightarrow> compactin X {x \<in> topspace X. f x \<in> K}" for K
+    using R proper_map_alt by auto
+  with R show ?lhs
+    by (simp add: assms proper_map_into_k_space_eq subtopology_kification_compact)
+qed
+
+lemma perfect_map_from_kification:
+   "\<lbrakk>k_space Y; perfect_map X Y f\<rbrakk> \<Longrightarrow> perfect_map(kification X) Y f"
+  by (simp add: continuous_map_from_kification perfect_map_def proper_map_from_kification)
+
+lemma k_space_perfect_map_image_eq:
+  assumes "Hausdorff_space X" "perfect_map X Y f"
+  shows "k_space X \<longleftrightarrow> k_space Y"
+proof
+  show "k_space X \<Longrightarrow> k_space Y"
+    using k_space_perfect_map_image assms by blast
+  assume "k_space Y"
+  have "homeomorphic_map (kification X) X id"
+    unfolding homeomorphic_eq_injective_perfect_map
+    proof (intro conjI perfect_map_from_composition_right [where f = id])
+  show "perfect_map (kification X) Y (f \<circ> id)"
+    by (simp add: \<open>k_space Y\<close> assms(2) perfect_map_from_kification)
+  show "continuous_map (kification X) X id"
+    by (simp add: continuous_map_from_kification)
+qed (use assms perfect_map_def in auto)
+  then show "k_space X"
+    using homeomorphic_k_space homeomorphic_space by blast 
+qed
+
+
+subsection\<open>One-point compactifications and the Alexandroff extension construction\<close>
+
+lemma one_point_compactification_dense:
+   "\<lbrakk>compact_space X; \<not> compactin X (topspace X - {a})\<rbrakk> \<Longrightarrow> X closure_of (topspace X - {a}) = topspace X"
+  unfolding closure_of_complement
+  by (metis Diff_empty closedin_compact_space interior_of_eq_empty openin_closedin_eq subset_singletonD)
+
+lemma one_point_compactification_interior:
+   "\<lbrakk>compact_space X; \<not> compactin X (topspace X - {a})\<rbrakk> \<Longrightarrow> X interior_of {a} = {}"
+  by (simp add: interior_of_eq_empty_complement one_point_compactification_dense)
+
+lemma kc_space_one_point_compactification_gen:
+  assumes "compact_space X"
+  shows "kc_space X \<longleftrightarrow>
+         openin X (topspace X - {a}) \<and> (\<forall>K. compactin X K \<and> a\<notin>K \<longrightarrow> closedin X K) \<and>
+         k_space (subtopology X (topspace X - {a})) \<and> kc_space (subtopology X (topspace X - {a}))"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume L: ?lhs show ?rhs
+  proof (intro conjI strip)
+    show "openin X (topspace X - {a})"
+      using L kc_imp_t1_space t1_space_openin_delete_alt by auto
+    then show "k_space (subtopology X (topspace X - {a}))"
+      by (simp add: L assms k_space_open_subtopology_aux)
+    show "closedin X k" if "compactin X k \<and> a \<notin> k" for k :: "'a set"
+      using L kc_space_def that by blast
+    show "kc_space (subtopology X (topspace X - {a}))"
+      by (simp add: L kc_space_subtopology)
+  qed
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding kc_space_def
+  proof (intro strip)
+    fix S
+    assume "compactin X S"
+    then have "S \<subseteq>topspace X"
+      by (simp add: compactin_subset_topspace)
+    show "closedin X S"
+    proof (cases "a \<in> S")
+      case True
+      then have "topspace X - S = topspace X - {a} - (S - {a})"
+        by auto
+      moreover have "openin X (topspace X - {a} - (S - {a}))"
+      proof (rule openin_trans_full)
+        show "openin (subtopology X (topspace X - {a})) (topspace X - {a} - (S - {a}))"
+        proof
+          show "openin (subtopology X (topspace X - {a})) (topspace X - {a})"
+            using R openin_open_subtopology by blast
+          have "closedin (subtopology X ((topspace X - {a}) \<inter> K)) (K \<inter> (S - {a}))"
+            if "compactin X K" "K \<subseteq> topspace X - {a}" for K
+          proof (intro closedin_subset_topspace)
+            show "closedin X (K \<inter> (S - {a}))"
+              using that
+              by (metis IntD1 Int_insert_right_if0 R True \<open>compactin X S\<close> closed_Int_compactin insert_Diff subset_Diff_insert)
+          qed (use that in auto)
+          moreover have "k_space (subtopology X (topspace X - {a}))"
+            using R by blast
+          moreover have "S-{a} \<subseteq> topspace X \<and> S-{a} \<subseteq> topspace X - {a}"
+            using \<open>S \<subseteq> topspace X\<close> by auto
+          ultimately show "closedin (subtopology X (topspace X - {a})) (S - {a})"
+            using \<open>S \<subseteq> topspace X\<close> True
+            by (simp add: k_space_def compactin_subtopology subtopology_subtopology)
+        qed 
+        show "openin X (topspace X - {a})"
+          by (simp add: R)
+      qed
+      ultimately show ?thesis
+        by (simp add: \<open>S \<subseteq> topspace X\<close> closedin_def)
+    next
+      case False
+      then show ?thesis
+        by (simp add: R \<open>compactin X S\<close>)
+    qed
+  qed
+qed
+
+  
+inductive Alexandroff_open for X where
+  base: "openin X U \<Longrightarrow> Alexandroff_open X (Some ` U)"
+| ext: "\<lbrakk>compactin X C; closedin X C\<rbrakk> \<Longrightarrow> Alexandroff_open X (insert None (Some ` (topspace X - C)))"
+
+lemma Alexandroff_open_iff: "Alexandroff_open X S \<longleftrightarrow>
+   (\<exists>U. (S = Some ` U \<and> openin X U) \<or> (S = insert None (Some ` (topspace X - U)) \<and> compactin X U \<and> closedin X U))"
+  by (meson Alexandroff_open.cases Alexandroff_open.ext base)
+
+lemma Alexandroff_open_Un_aux:
+  assumes U: "openin X U" and "Alexandroff_open X T"
+  shows  "Alexandroff_open X (Some ` U \<union> T)"
+  using \<open>Alexandroff_open X T\<close>
+proof (induction rule: Alexandroff_open.induct)
+  case (base V)
+  then show ?case
+    by (metis Alexandroff_open.base U image_Un openin_Un)
+next
+  case (ext C)
+  have "U \<subseteq> topspace X"
+    by (simp add: U openin_subset)
+  then have eq: "Some ` U \<union> insert None (Some ` (topspace X - C)) = insert None (Some ` (topspace X - (C \<inter> (topspace X - U))))"
+    by force
+  have "closedin X (C \<inter> (topspace X - U))"
+    using U ext.hyps(2) by blast
+  moreover
+  have "compactin X (C \<inter> (topspace X - U))"
+    using U compact_Int_closedin ext.hyps(1) by blast
+  ultimately show ?case
+    unfolding eq using Alexandroff_open.ext by blast
+qed
+
+lemma Alexandroff_open_Un:
+  assumes "Alexandroff_open X S" and "Alexandroff_open X T"
+  shows "Alexandroff_open X (S \<union> T)"
+  using assms
+proof (induction rule: Alexandroff_open.induct)
+  case (base U)
+  then show ?case
+    by (simp add: Alexandroff_open_Un_aux)
+next
+  case (ext C)
+  then show ?case
+    by (smt (verit, best) Alexandroff_open_Un_aux Alexandroff_open_iff Un_commute Un_insert_left closedin_def insert_absorb2)
+qed
+
+lemma Alexandroff_open_Int_aux:
+  assumes U: "openin X U" and "Alexandroff_open X T"
+  shows  "Alexandroff_open X (Some ` U \<inter> T)"
+  using \<open>Alexandroff_open X T\<close>
+proof (induction rule: Alexandroff_open.induct)
+  case (base V)
+  then show ?case
+    by (metis Alexandroff_open.base U image_Int inj_Some openin_Int)
+next
+  case (ext C)
+  have eq: "Some ` U \<inter> insert None (Some ` (topspace X - C)) = Some ` (topspace X - (C \<union> (topspace X - U)))"
+    by force
+  have "openin X (topspace X - (C \<union> (topspace X - U)))"
+    using U ext.hyps(2) by blast
+  then show ?case
+    unfolding eq using Alexandroff_open.base by blast
+qed
+
+lemma istopology_Alexandroff_open: "istopology (Alexandroff_open X)"
+  unfolding istopology_def
+proof (intro conjI strip)
+  fix S T
+  assume "Alexandroff_open X S" and "Alexandroff_open X T"
+  then show "Alexandroff_open X (S \<inter> T)"
+  proof (induction rule: Alexandroff_open.induct)
+    case (base U)
+    then show ?case
+      using Alexandroff_open_Int_aux by blast
+  next
+    case EC: (ext C)
+    show ?case
+      using \<open>Alexandroff_open X T\<close>
+    proof (induction rule: Alexandroff_open.induct)
+      case (base V)
+      then show ?case
+        by (metis Alexandroff_open.ext Alexandroff_open_Int_aux EC.hyps inf_commute)
+    next
+      case (ext D)
+      have eq: "insert None (Some ` (topspace X - C)) \<inter> insert None (Some ` (topspace X - D))
+              = insert None (Some ` (topspace X - (C \<union> D)))"
+        by auto
+      show ?case
+        unfolding eq
+        by (simp add: Alexandroff_open.ext EC.hyps closedin_Un compactin_Un ext.hyps)
+    qed
+  qed
+next
+  fix \<K>
+  assume \<section>: "\<forall>K\<in>\<K>. Alexandroff_open X K"
+  show "Alexandroff_open X (\<Union>\<K>)"
+  proof (cases "None \<in> \<Union>\<K>")
+    case True
+    have "\<forall>K\<in>\<K>. \<exists>U. (openin X U \<and> K = Some ` U) \<or> (K = insert None (Some ` (topspace X - U)) \<and> compactin X U \<and> closedin X U)"
+      by (metis \<section> Alexandroff_open_iff)
+    then obtain U where U: 
+      "\<And>K. K \<in> \<K> \<Longrightarrow> openin X (U K) \<and> K = Some ` (U K) 
+                    \<or> (K = insert None (Some ` (topspace X - U K)) \<and> compactin X (U K) \<and> closedin X (U K))"
+      by metis
+    define \<K>N where "\<K>N \<equiv> {K \<in> \<K>. None \<in> K}"
+    define A where "A \<equiv> \<Union>K\<in>\<K>-\<K>N. U K"
+    define B where "B \<equiv> \<Inter>K\<in>\<K>N. U K"
+    have U1: "\<And>K. K \<in> \<K>-\<K>N \<Longrightarrow> openin X (U K) \<and> K = Some ` (U K)"
+      using U \<K>N_def by auto
+    have U2: "\<And>K. K \<in> \<K>N \<Longrightarrow> K = insert None (Some ` (topspace X - U K)) \<and> compactin X (U K) \<and> closedin X (U K)"
+      using U \<K>N_def by auto
+    have eqA: "\<Union>(\<K>-\<K>N) = Some ` A"
+    proof
+      show "\<Union> (\<K> - \<K>N) \<subseteq> Some ` A"
+        by (metis A_def Sup_le_iff U1 UN_upper subset_image_iff)
+      show "Some ` A \<subseteq> \<Union> (\<K> - \<K>N)"
+        using A_def U1 by blast
+    qed
+    have eqB: "\<Union>\<K>N = insert None (Some ` (topspace X - B))"
+      using U2 True
+      by (auto simp: B_def image_iff \<K>N_def)
+    have "\<Union>\<K> = \<Union>\<K>N \<union> \<Union>(\<K>-\<K>N)"
+      by (auto simp: \<K>N_def)
+    then have eq: "\<Union>\<K> = (Some ` A) \<union> (insert None (Some ` (topspace X - B)))"
+      by (simp add: eqA eqB Un_commute)
+    show ?thesis
+      unfolding eq
+    proof (intro Alexandroff_open_Un Alexandroff_open.intros)
+      show "openin X A"
+        using A_def U1 by blast
+      show "closedin X B"
+        unfolding B_def using U2 True \<K>N_def by auto
+      show "compactin X B"
+        by (metis B_def U2 eqB Inf_lower Union_iff \<open>closedin X B\<close> closed_compactin imageI insertI1)
+    qed
+  next
+    case False
+    then have "\<forall>K\<in>\<K>. \<exists>U. openin X U \<and> K = Some ` U"
+      by (metis Alexandroff_open.simps UnionI \<section> insertCI)
+    then obtain U where U: "\<forall>K\<in>\<K>. openin X (U K) \<and> K = Some ` (U K)"
+      by metis
+    then have eq: "\<Union>\<K> = Some ` (\<Union> K\<in>\<K>. U K)"
+      using image_iff by fastforce
+    show ?thesis
+      unfolding eq by (simp add: U base openin_clauses(3))
+  qed
+qed
+
+
+definition Alexandroff_compactification where
+  "Alexandroff_compactification X \<equiv> topology (Alexandroff_open X)"
+
+lemma openin_Alexandroff_compactification:
+   "openin(Alexandroff_compactification X) V \<longleftrightarrow>
+        (\<exists>U. openin X U \<and> V = Some ` U) \<or>
+        (\<exists>C. compactin X C \<and> closedin X C \<and> V = insert None (Some ` (topspace X - C)))"
+  by (auto simp: Alexandroff_compactification_def istopology_Alexandroff_open Alexandroff_open.simps)
+
+
+lemma topspace_Alexandroff_compactification [simp]:
+   "topspace(Alexandroff_compactification X) = insert None (Some ` topspace X)"
+   (is "?lhs = ?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    by (force simp add: topspace_def openin_Alexandroff_compactification)
+  have "None \<in> topspace (Alexandroff_compactification X)"
+    by (meson closedin_empty compactin_empty insert_subset openin_Alexandroff_compactification openin_subset)
+  moreover have "Some x \<in> topspace (Alexandroff_compactification X)"
+    if "x \<in> topspace X" for x 
+    by (meson that imageI openin_Alexandroff_compactification openin_subset openin_topspace subsetD)
+  ultimately show "?rhs \<subseteq> ?lhs"
+    by (auto simp: image_subset_iff)
+qed
+
+lemma closedin_Alexandroff_compactification:
+   "closedin (Alexandroff_compactification X) C \<longleftrightarrow>
+      (\<exists>K. compactin X K \<and> closedin X K \<and> C = Some ` K) \<or>
+      (\<exists>U. openin X U \<and> C = topspace(Alexandroff_compactification X) - Some ` U)"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show "?lhs \<Longrightarrow> ?rhs"
+    apply (clarsimp simp: closedin_def openin_Alexandroff_compactification)
+    by (smt (verit) Diff_Diff_Int None_notin_image_Some image_set_diff inf.absorb_iff2 inj_Some insert_Diff_if subset_insert)
+  show "?rhs \<Longrightarrow> ?lhs"
+    using openin_subset 
+    by (fastforce simp: closedin_def openin_Alexandroff_compactification)
+qed
+
+lemma openin_Alexandroff_compactification_image_Some [simp]:
+   "openin(Alexandroff_compactification X) (Some ` U) \<longleftrightarrow> openin X U"
+  by (auto simp: openin_Alexandroff_compactification inj_image_eq_iff)
+
+lemma closedin_Alexandroff_compactification_image_Some [simp]:
+   "closedin (Alexandroff_compactification X) (Some ` K) \<longleftrightarrow> compactin X K \<and> closedin X K"
+  by (auto simp: closedin_Alexandroff_compactification inj_image_eq_iff)
+
+lemma open_map_Some: "open_map X (Alexandroff_compactification X) Some"
+  using open_map_def openin_Alexandroff_compactification by blast
+
+lemma continuous_map_Some: "continuous_map X (Alexandroff_compactification X) Some"
+  unfolding continuous_map_def 
+proof (intro conjI strip)
+  fix U
+  assume "openin (Alexandroff_compactification X) U"
+  then consider V where "openin X V" "U = Some ` V" 
+    | C where "compactin X C" "closedin X C" "U = insert None (Some ` (topspace X - C))" 
+    by (auto simp: openin_Alexandroff_compactification)
+  then show "openin X {x \<in> topspace X. Some x \<in> U}"
+  proof cases
+    case 1
+    then show ?thesis
+      using openin_subopen openin_subset by fastforce
+  next
+    case 2
+    then show ?thesis
+      by (simp add: closedin_def image_iff set_diff_eq)
+  qed
+qed auto
+
+
+lemma embedding_map_Some: "embedding_map X (Alexandroff_compactification X) Some"
+  by (simp add: continuous_map_Some injective_open_imp_embedding_map open_map_Some)
+
+lemma compact_space_Alexandroff_compactification [simp]:
+   "compact_space(Alexandroff_compactification X)"
+proof (clarsimp simp: compact_space_alt image_subset_iff)
+  fix \<U> U
+  assume ope [rule_format]: "\<forall>U\<in>\<U>. openin (Alexandroff_compactification X) U"
+      and cover: "\<forall>x\<in>topspace X. \<exists>X\<in>\<U>. Some x \<in> X"
+      and "U \<in> \<U>" "None \<in> U"
+  then have Usub: "U \<subseteq> insert None (Some ` topspace X)"
+    by (metis openin_subset topspace_Alexandroff_compactification)
+  with ope [OF \<open>U \<in> \<U>\<close>] \<open>None \<in> U\<close>
+  obtain C where C: "compactin X C \<and> closedin X C \<and>
+          insert None (Some ` topspace X) - U = Some ` C"
+    by (auto simp: openin_closedin closedin_Alexandroff_compactification)
+  then have D: "compactin (Alexandroff_compactification X) (insert None (Some ` topspace X) - U)"
+    by (metis continuous_map_Some image_compactin)
+  consider V where "openin X V" "U = Some ` V" 
+    | C where "compactin X C" "closedin X C" "U = insert None (Some ` (topspace X - C))" 
+    using ope [OF \<open>U \<in> \<U>\<close>] by (auto simp: openin_Alexandroff_compactification)
+  then show "\<exists>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<and> (\<exists>X\<in>\<F>. None \<in> X) \<and> (\<forall>x\<in>topspace X. \<exists>X\<in>\<F>. Some x \<in> X)"
+  proof cases
+    case 1
+    then show ?thesis
+      using \<open>None \<in> U\<close> by blast      
+  next
+    case 2
+    obtain \<F> where "finite \<F>" "\<F> \<subseteq> \<U>" "insert None (Some ` topspace X) - U \<subseteq> \<Union>\<F>"
+      by (smt (verit, del_insts) C D Union_iff compactinD compactin_subset_topspace cover image_subset_iff ope subsetD)
+    with \<open>U \<in> \<U>\<close> show ?thesis
+      by (rule_tac x="insert U \<F>" in exI) auto
+  qed
+qed
+
+lemma topspace_Alexandroff_compactification_delete:
+   "topspace(Alexandroff_compactification X) - {None} = Some ` topspace X"
+  by simp
+
+lemma Alexandroff_compactification_dense:
+  assumes "\<not> compact_space X"
+  shows "(Alexandroff_compactification X) closure_of (Some ` topspace X) =
+         topspace(Alexandroff_compactification X)"
+  unfolding topspace_Alexandroff_compactification_delete [symmetric]
+proof (intro one_point_compactification_dense)
+  show "\<not> compactin (Alexandroff_compactification X) (topspace (Alexandroff_compactification X) - {None})"
+    using assms compact_space_proper_map_preimage compact_space_subtopology embedding_map_Some embedding_map_def homeomorphic_imp_proper_map by fastforce
+qed auto
+
+
+lemma t0_space_one_point_compactification:
+  assumes "compact_space X \<and> openin X (topspace X - {a})"
+  shows "t0_space X \<longleftrightarrow> t0_space (subtopology X (topspace X - {a}))"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show "?lhs \<Longrightarrow> ?rhs"
+    using t0_space_subtopology by blast
+  show "?rhs \<Longrightarrow> ?lhs"
+    using assms
+    unfolding t0_space_def by (bestsimp simp flip: Int_Diff dest: openin_trans_full)
+qed
+
+lemma t0_space_Alexandroff_compactification [simp]:
+   "t0_space (Alexandroff_compactification X) \<longleftrightarrow> t0_space X"
+  using t0_space_one_point_compactification [of "Alexandroff_compactification X" None]
+  using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_t0_space by fastforce
+
+lemma t1_space_one_point_compactification:
+  assumes Xa: "openin X (topspace X - {a})"
+    and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
+  shows "t1_space X \<longleftrightarrow> t1_space (subtopology X (topspace X - {a}))"  (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show "?lhs \<Longrightarrow> ?rhs"
+    using t1_space_subtopology by blast
+  assume R: ?rhs
+  show ?lhs
+    unfolding t1_space_closedin_singleton
+  proof (intro strip)
+    fix x
+    assume "x \<in> topspace X"
+    show "closedin X {x}"
+    proof (cases "x=a")
+      case True
+      then show ?thesis
+        using \<open>x \<in> topspace X\<close> Xa closedin_def by blast
+    next
+      case False
+      show ?thesis
+        by (simp add: "\<section>" False R \<open>x \<in> topspace X\<close> closedin_t1_singleton)
+    qed
+  qed
+qed
+
+lemma closedin_Alexandroff_I: 
+  assumes "compactin (Alexandroff_compactification X) K" "K \<subseteq> Some ` topspace X"
+          "closedin (Alexandroff_compactification X) T" "K = T \<inter> Some ` topspace X"
+  shows "closedin (Alexandroff_compactification X) K"
+proof -
+  obtain S where S: "S \<subseteq> topspace X" "K = Some ` S"
+    by (meson \<open>K \<subseteq> Some ` topspace X\<close> subset_imageE)
+  with assms have "compactin X S"
+    by (metis compactin_subtopology embedding_map_Some embedding_map_def homeomorphic_map_compactness)
+  moreover have "closedin X S"
+    using assms S
+    by (metis closedin_subtopology embedding_map_Some embedding_map_def homeomorphic_map_closedness)
+  ultimately show ?thesis
+    by (simp add: S)
+qed
+
+
+lemma t1_space_Alexandroff_compactification [simp]:
+  "t1_space(Alexandroff_compactification X) \<longleftrightarrow> t1_space X"
+proof -
+  have "openin (Alexandroff_compactification X) (topspace (Alexandroff_compactification X) - {None})"
+    by auto
+  then show ?thesis
+    using t1_space_one_point_compactification [of "Alexandroff_compactification X" None]
+    using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_t1_space 
+    by (fastforce simp add: compactin_subtopology closedin_Alexandroff_I closedin_subtopology)
+qed
+
+
+lemma kc_space_one_point_compactification:
+  assumes "compact_space X"
+    and ope: "openin X (topspace X - {a})"
+    and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk>
+                \<Longrightarrow> closedin X K"
+  shows "kc_space X \<longleftrightarrow>
+         k_space (subtopology X (topspace X - {a})) \<and> kc_space (subtopology X (topspace X - {a}))"
+proof -
+  have "closedin X K"
+    if "kc_space (subtopology X (topspace X - {a}))" and "compactin X K" "a \<notin> K" for K
+    using that unfolding kc_space_def 
+    by (metis "\<section>" Diff_empty compactin_subspace compactin_subtopology subset_Diff_insert)
+  then show ?thesis
+    by (metis \<open>compact_space X\<close> kc_space_one_point_compactification_gen ope)
+qed
+
+lemma kc_space_Alexandroff_compactification:
+  "kc_space(Alexandroff_compactification X) \<longleftrightarrow> (k_space X \<and> kc_space X)" (is "kc_space ?Y = _")
+proof -
+  have "kc_space (Alexandroff_compactification X) \<longleftrightarrow>
+      (k_space (subtopology ?Y (topspace ?Y - {None})) \<and> kc_space (subtopology ?Y (topspace ?Y - {None})))"
+    by (rule kc_space_one_point_compactification) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
+  also have "... \<longleftrightarrow> k_space X \<and> kc_space X"
+    using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_k_space homeomorphic_kc_space by simp blast
+  finally show ?thesis .
+qed
+
+
+lemma regular_space_one_point_compactification:
+  assumes "compact_space X" and ope: "openin X (topspace X - {a})"
+    and \<section>: "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
+  shows "regular_space X \<longleftrightarrow>
+           regular_space (subtopology X (topspace X - {a})) \<and> locally_compact_space (subtopology X (topspace X - {a}))" 
+    (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show "?lhs \<Longrightarrow> ?rhs"
+    using assms(1) compact_imp_locally_compact_space locally_compact_space_open_subset ope regular_space_subtopology by blast
+  assume R: ?rhs
+  let ?Xa = "subtopology X (topspace X - {a})"
+  show ?lhs
+    unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of imp_conjL
+  proof (intro strip)
+    fix W x
+    assume "openin X W" and "x \<in> W"
+    show "\<exists>U V. openin X U \<and> closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+    proof (cases "x=a")
+      case True
+      have "compactin ?Xa (topspace X - W)"
+        using \<open>openin X W\<close> assms(1) closedin_compact_space
+        by (metis Diff_mono True \<open>x \<in> W\<close> compactin_subtopology empty_subsetI insert_subset openin_closedin_eq order_refl)
+      then obtain V K where V: "openin ?Xa V" and K: "compactin ?Xa K" "closedin ?Xa K" and "topspace X - W \<subseteq> V" "V \<subseteq> K"
+        by (metis locally_compact_space_compact_closed_compact R)
+      show ?thesis
+      proof (intro exI conjI)
+        show "openin X (topspace X - K)"
+          using "\<section>" K by blast
+        show "closedin X (topspace X - V)"
+          using V ope openin_trans_full by blast
+        show "x \<in> topspace X - K"
+        proof (rule)
+          show "x \<in> topspace X"
+            using \<open>openin X W\<close> \<open>x \<in> W\<close> openin_subset by blast
+          show "x \<notin> K"
+            using K True closedin_imp_subset by blast
+        qed
+        show "topspace X - K \<subseteq> topspace X - V"
+          by (simp add: Diff_mono \<open>V \<subseteq> K\<close>)
+        show "topspace X - V \<subseteq> W"
+          using \<open>topspace X - W \<subseteq> V\<close> by auto
+      qed
+    next
+      case False
+      have "openin ?Xa ((topspace X - {a}) \<inter> W)"
+        using \<open>openin X W\<close> openin_subtopology_Int2 by blast
+      moreover have "x \<in> (topspace X - {a}) \<inter> W"
+        using \<open>openin X W\<close> \<open>x \<in> W\<close> openin_subset False by blast
+      ultimately obtain U V where "openin ?Xa U" "compactin ?Xa V" "closedin ?Xa V"
+               "x \<in> U" "U \<subseteq> V" "V \<subseteq> (topspace X - {a}) \<inter> W"
+        using R locally_compact_regular_space_neighbourhood_base neighbourhood_base_of
+        by (metis (no_types, lifting))
+      then show ?thesis
+        by (meson "\<section>" le_infE ope openin_trans_full)
+    qed
+  qed
+qed
+
+
+lemma regular_space_Alexandroff_compactification:
+  "regular_space(Alexandroff_compactification X) \<longleftrightarrow> regular_space X \<and> locally_compact_space X" 
+  (is "regular_space ?Y = ?rhs")
+proof -
+  have "regular_space ?Y \<longleftrightarrow>
+        regular_space (subtopology ?Y (topspace ?Y - {None})) \<and> locally_compact_space (subtopology ?Y (topspace ?Y - {None}))"
+    by (rule regular_space_one_point_compactification) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
+  also have "... \<longleftrightarrow> regular_space X \<and> locally_compact_space X"
+    using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_locally_compact_space homeomorphic_regular_space 
+      by fastforce
+  finally show ?thesis .
+qed
+
+
+lemma Hausdorff_space_one_point_compactification:
+  assumes "compact_space X" and  "openin X (topspace X - {a})"
+    and "\<And>K. \<lbrakk>compactin (subtopology X (topspace X - {a})) K; closedin (subtopology X (topspace X - {a})) K\<rbrakk> \<Longrightarrow> closedin X K"
+  shows "Hausdorff_space X \<longleftrightarrow>
+           Hausdorff_space (subtopology X (topspace X - {a})) \<and> locally_compact_space (subtopology X (topspace X - {a}))" 
+    (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show ?rhs if ?lhs
+  proof -
+    have "locally_compact_space (subtopology X (topspace X - {a}))"
+      using assms that compact_imp_locally_compact_space locally_compact_space_open_subset 
+      by blast
+    with that show ?rhs
+      by (simp add: Hausdorff_space_subtopology)
+  qed
+next
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (metis assms locally_compact_Hausdorff_or_regular regular_space_one_point_compactification
+        regular_t1_eq_Hausdorff_space t1_space_one_point_compactification)
+qed
+
+lemma Hausdorff_space_Alexandroff_compactification:
+   "Hausdorff_space(Alexandroff_compactification X) \<longleftrightarrow> Hausdorff_space X \<and> locally_compact_space X"
+  by (meson compact_Hausdorff_imp_regular_space compact_space_Alexandroff_compactification 
+      locally_compact_Hausdorff_or_regular regular_space_Alexandroff_compactification 
+      regular_t1_eq_Hausdorff_space t1_space_Alexandroff_compactification)
+
+lemma completely_regular_space_Alexandroff_compactification:
+   "completely_regular_space(Alexandroff_compactification X) \<longleftrightarrow>
+        completely_regular_space X \<and> locally_compact_space X"
+  by (metis regular_space_Alexandroff_compactification completely_regular_eq_regular_space
+      compact_imp_locally_compact_space compact_space_Alexandroff_compactification)
+
+lemma Hausdorff_space_one_point_compactification_asymmetric_prod:
+  assumes "compact_space X"
+  shows "Hausdorff_space X \<longleftrightarrow>
+         kc_space (prod_topology X (subtopology X (topspace X - {a}))) \<and>
+         k_space (prod_topology X (subtopology X (topspace X - {a})))"  (is "?lhs \<longleftrightarrow> ?rhs")
+proof (cases "a \<in> topspace X")
+  case True
+  show ?thesis
+  proof 
+    show ?rhs if ?lhs
+    proof
+      show "kc_space (prod_topology X (subtopology X (topspace X - {a})))"
+        using Hausdorff_imp_kc_space kc_space_prod_topology_right kc_space_subtopology that by blast
+      show "k_space (prod_topology X (subtopology X (topspace X - {a})))"
+        by (meson Hausdorff_imp_kc_space assms compact_imp_locally_compact_space k_space_prod_topology_left 
+            kc_space_one_point_compactification_gen that)
+    qed
+  next
+    assume R: ?rhs
+    define D where "D \<equiv> (\<lambda>x. (x,x)) ` (topspace X - {a})"
+    show ?lhs
+    proof (cases "topspace X = {a}")
+      case True
+      then show ?thesis
+        by (simp add: Hausdorff_space_def)
+    next
+      case False
+      then have "kc_space X"
+        using kc_space_retraction_map_image [of "prod_topology X (subtopology X (topspace X - {a}))" X fst]
+        by (metis Diff_subset R True insert_Diff retraction_map_fst topspace_subtopology_subset)
+      have "closedin (subtopology (prod_topology X (subtopology X (topspace X - {a}))) K) (K \<inter> D)" 
+        if "compactin (prod_topology X (subtopology X (topspace X - {a}))) K" for K
+      proof (intro closedin_subtopology_Int_subset[where V=K] closedin_subset_topspace)
+        show "fst ` K \<times> snd ` K \<inter> D \<subseteq> fst ` K \<times> snd ` K" "K \<subseteq> fst ` K \<times> snd ` K"
+          by force+
+        have eq: "(fst ` K \<times> snd ` K \<inter> D) = ((\<lambda>x. (x,x)) ` (fst ` K \<inter> snd ` K))"
+          using compactin_subset_topspace that by (force simp: D_def image_iff)
+        have "compactin (prod_topology X (subtopology X (topspace X - {a}))) (fst ` K \<times> snd ` K \<inter> D)"
+          unfolding eq
+        proof (rule image_compactin [of "subtopology X (topspace X - {a})"])
+          have "compactin X (fst ` K)" "compactin X (snd ` K)"
+            by (meson compactin_subtopology continuous_map_fst continuous_map_snd image_compactin that)+
+          moreover have "fst ` K \<inter> snd ` K \<subseteq> topspace X - {a}"
+            using compactin_subset_topspace that by force
+          ultimately
+          show "compactin (subtopology X (topspace X - {a})) (fst ` K \<inter> snd ` K)"
+            unfolding compactin_subtopology
+            by (meson \<open>kc_space X\<close> closed_Int_compactin kc_space_def)
+          show "continuous_map (subtopology X (topspace X - {a})) (prod_topology X (subtopology X (topspace X - {a}))) (\<lambda>x. (x,x))"
+            by (simp add: continuous_map_paired)
+        qed
+        then show "closedin (prod_topology X (subtopology X (topspace X - {a}))) (fst ` K \<times> snd ` K \<inter> D)"
+          using R compactin_imp_closedin_gen by blast
+      qed
+      moreover have "D \<subseteq> topspace X \<times> (topspace X \<inter> (topspace X - {a}))"
+        by (auto simp: D_def)
+      ultimately have *: "closedin (prod_topology X (subtopology X (topspace X - {a}))) D"
+        using R by (auto simp: k_space)
+      have "x=y"
+        if "x \<in> topspace X" "y \<in> topspace X" 
+          and \<section>: "\<And>T. \<lbrakk>(x,y) \<in> T; openin (prod_topology X X) T\<rbrakk> \<Longrightarrow> \<exists>z \<in> topspace X. (z,z) \<in> T" for x y
+      proof (cases "x=a \<and> y=a")
+        case False
+        then consider "x\<noteq>a" | "y\<noteq>a"
+          by blast
+        then show ?thesis
+        proof cases
+          case 1
+          have "\<exists>z \<in> topspace X - {a}. (z,z) \<in> T"
+            if "(y,x) \<in> T" "openin (prod_topology X (subtopology X (topspace X - {a}))) T" for T
+          proof -
+            have "(x,y) \<in> {z \<in> topspace (prod_topology X X). (snd z,fst z) \<in> T \<inter> topspace X \<times> (topspace X - {a})}"
+              by (simp add: "1" \<open>x \<in> topspace X\<close> \<open>y \<in> topspace X\<close> that)
+            moreover have "openin (prod_topology X X) {z \<in> topspace (prod_topology X X). (snd z,fst z) \<in> T \<inter> topspace X \<times> (topspace X - {a})}"
+            proof (rule openin_continuous_map_preimage)
+              show "continuous_map (prod_topology X X) (prod_topology X X) (\<lambda>x. (snd x, fst x))"
+                by (simp add: continuous_map_fst continuous_map_pairedI continuous_map_snd)
+              have "openin (prod_topology X X) (topspace X \<times> (topspace X - {a}))"
+                using \<open>kc_space X\<close> assms kc_space_one_point_compactification_gen openin_prod_Times_iff by fastforce
+              moreover have "openin (prod_topology X X) T"
+                using kc_space_one_point_compactification_gen [OF \<open>compact_space X\<close>] \<open>kc_space X\<close> that
+                by (metis openin_prod_Times_iff openin_topspace openin_trans_full prod_topology_subtopology(2))
+              ultimately show "openin (prod_topology X X) (T \<inter> topspace X \<times> (topspace X - {a}))"
+                by blast
+            qed
+            ultimately show ?thesis
+              by (smt (verit) \<section> Int_iff fst_conv mem_Collect_eq mem_Sigma_iff snd_conv)
+          qed
+          then have "(y,x) \<in> prod_topology X (subtopology X (topspace X - {a})) closure_of D"
+            by (simp add: "1" D_def in_closure_of that)
+          then show ?thesis
+            using that "*" D_def closure_of_closedin by fastforce
+        next
+          case 2
+          have "\<exists>z \<in> topspace X - {a}. (z,z) \<in> T"
+            if "(x,y) \<in> T" "openin (prod_topology X (subtopology X (topspace X - {a}))) T" for T
+          proof -
+            have "openin (prod_topology X X) (topspace X \<times> (topspace X - {a}))"
+              using \<open>kc_space X\<close> assms kc_space_one_point_compactification_gen openin_prod_Times_iff by fastforce
+            moreover have XXT: "openin (prod_topology X X) T"
+              using kc_space_one_point_compactification_gen [OF \<open>compact_space X\<close>] \<open>kc_space X\<close> that
+              by (metis openin_prod_Times_iff openin_topspace openin_trans_full prod_topology_subtopology(2))
+            ultimately have "openin (prod_topology X X) (T \<inter> topspace X \<times> (topspace X - {a}))"
+              by blast
+            then show ?thesis
+              by (smt (verit) "\<section>" Diff_subset XXT mem_Sigma_iff openin_subset subsetD that topspace_prod_topology topspace_subtopology_subset)
+          qed
+          then have "(x,y) \<in> prod_topology X (subtopology X (topspace X - {a})) closure_of D"
+            by (simp add: "2" D_def in_closure_of that)
+          then show ?thesis
+            using that "*" D_def closure_of_closedin by fastforce
+        qed
+      qed auto
+      then show ?thesis
+        unfolding Hausdorff_space_closedin_diagonal closure_of_subset_eq [symmetric] 
+          by (force simp add: closure_of_def)
+    qed
+  qed
+next
+  case False
+  then show ?thesis
+    by (simp add: assms compact_imp_k_space compact_space_prod_topology kc_space_compact_prod_topology)
+qed
+
+
+lemma Hausdorff_space_Alexandroff_compactification_asymmetric_prod:
+   "Hausdorff_space(Alexandroff_compactification X) \<longleftrightarrow>
+        kc_space(prod_topology (Alexandroff_compactification X) X) \<and>
+        k_space(prod_topology (Alexandroff_compactification X) X)"
+    (is "Hausdorff_space ?Y = ?rhs")
+proof -
+  have *: "subtopology (Alexandroff_compactification X)
+     (topspace (Alexandroff_compactification X) -
+      {None}) homeomorphic_space X"
+    using embedding_map_Some embedding_map_imp_homeomorphic_space homeomorphic_space_sym by fastforce
+  have "Hausdorff_space (Alexandroff_compactification X) \<longleftrightarrow>
+      (kc_space (prod_topology ?Y (subtopology ?Y (topspace ?Y - {None}))) \<and>
+       k_space (prod_topology ?Y (subtopology ?Y (topspace ?Y - {None}))))"
+    by (rule Hausdorff_space_one_point_compactification_asymmetric_prod) (auto simp: compactin_subtopology closedin_subtopology closedin_Alexandroff_I)
+  also have "... \<longleftrightarrow> ?rhs"
+    using homeomorphic_k_space homeomorphic_kc_space homeomorphic_space_prod_topology 
+          homeomorphic_space_refl * by blast
+  finally show ?thesis .
+qed
+
+lemma kc_space_as_compactification_unique:
+  assumes "kc_space X" "compact_space X"
+  shows "openin X U \<longleftrightarrow>
+         (if a \<in> U then U \<subseteq> topspace X \<and> compactin X (topspace X - U)
+                   else openin (subtopology X (topspace X - {a})) U)"
+proof (cases "a \<in> U")
+  case True
+  then show ?thesis
+    by (meson assms closedin_compact_space compactin_imp_closedin_gen openin_closedin_eq)
+next
+  case False
+  then show ?thesis
+  by (metis Diff_empty kc_space_one_point_compactification_gen openin_open_subtopology openin_subset subset_Diff_insert assms)
+qed
+
+lemma kc_space_as_compactification_unique_explicit:
+  assumes "kc_space X" "compact_space X"
+  shows "openin X U \<longleftrightarrow>
+         (if a \<in> U then U \<subseteq> topspace X \<and>
+                     compactin (subtopology X (topspace X - {a})) (topspace X - U) \<and>
+                     closedin (subtopology X (topspace X - {a})) (topspace X - U)
+                else openin (subtopology X (topspace X - {a})) U)"
+  apply (simp add: kc_space_subtopology compactin_imp_closedin_gen assms compactin_subtopology cong: conj_cong)
+  by (metis Diff_mono assms bot.extremum insert_subset kc_space_as_compactification_unique subset_refl)
+
+lemma Alexandroff_compactification_unique:
+  assumes "kc_space X" "compact_space X" and a: "a \<in> topspace X"
+  shows "Alexandroff_compactification (subtopology X (topspace X - {a})) homeomorphic_space X"
+        (is "?Y homeomorphic_space X")
+proof -
+  have [simp]: "topspace X \<inter> (topspace X - {a}) = topspace X - {a}"  
+    by auto
+  have [simp]: "insert None (Some ` A) = insert None (Some ` B) \<longleftrightarrow> A = B" 
+               "insert None (Some ` A) \<noteq> Some ` B" for A B
+    by auto
+  have "quotient_map X ?Y (\<lambda>x. if x = a then None else Some x)"
+    unfolding quotient_map_def
+  proof (intro conjI strip)
+    show "(\<lambda>x. if x = a then None else Some x) ` topspace X = topspace ?Y"
+      using \<open>a \<in> topspace X\<close>  by force
+    show "openin X {x \<in> topspace X. (if x = a then None else Some x) \<in> U} = openin ?Y U" (is "?L = ?R")
+      if "U \<subseteq> topspace ?Y" for U
+    proof (cases "None \<in> U")
+      case True
+      then obtain T where T[simp]: "U = insert None (Some ` T)"
+        by (metis Int_insert_right UNIV_I UNIV_option_conv inf.orderE inf_le2 subsetI subset_imageE)
+      have Tsub: "T \<subseteq> topspace X - {a}"
+        using in_these_eq that by auto
+      then have "{x \<in> topspace X. (if x = a then None else Some x) \<in> U} = insert a T"
+        by (auto simp: a image_iff cong: conj_cong)
+      then have "?L \<longleftrightarrow> openin X (insert a T)"
+        by metis
+      also have "\<dots> \<longleftrightarrow> ?R"
+        using Tsub assms
+        apply (simp add: openin_Alexandroff_compactification kc_space_as_compactification_unique_explicit [where a=a])
+        by (smt (verit, best) Diff_insert2 Diff_subset closedin_imp_subset double_diff)
+      finally show ?thesis .
+    next
+      case False
+      then obtain T where [simp]: "U = Some ` T"
+        by (metis Int_insert_right UNIV_I UNIV_option_conv inf.orderE inf_le2 subsetI subset_imageE)
+      have **: "\<And>V. openin X V \<Longrightarrow> openin X (V - {a})"
+        by (simp add: assms compactin_imp_closedin_gen openin_diff)
+      have Tsub: "T \<subseteq> topspace X - {a}"
+        using in_these_eq that by auto
+      then have "{x \<in> topspace X. (if x = a then None else Some x) \<in> U} = T"
+        by (auto simp: image_iff cong: conj_cong)
+      then show ?thesis
+        by (simp add: "**" Tsub openin_open_subtopology)
+    qed
+  qed
+  moreover have "inj_on (\<lambda>x. if x = a then None else Some x) (topspace X)"
+    by (auto simp: inj_on_def)
+  ultimately show ?thesis
+    using homeomorphic_space_sym homeomorphic_space homeomorphic_map_def by blast
+qed
+
+end