# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1683367823 -3600
# Node ID c35f06b0931e7a0fb3a8aa17b9dae20f6f4f8f79
# Parent  2b07535e0d2726a222fc4d8a267bfcb778ace1f7
new material ported from HOL Light's metric.ml

diff -r 2b07535e0d27 -r c35f06b0931e src/HOL/Analysis/Abstract_Topological_Spaces.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Abstract_Topological_Spaces.thy	Sat May 06 11:10:23 2023 +0100
@@ -0,0 +1,2914 @@
+(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light] *)
+
+section \<open>Various Forms of Topological Spaces\<close>
+
+theory Abstract_Topological_Spaces
+  imports
+    Lindelof_Spaces Locally Sum_Topology
+begin
+
+
+subsection\<open>Connected topological spaces\<close>
+
+lemma connected_space_eq_frontier_eq_empty:
+   "connected_space X \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<and> X frontier_of S = {} \<longrightarrow> S = {} \<or> S = topspace X)"
+  by (meson clopenin_eq_frontier_of connected_space_clopen_in)
+
+lemma connected_space_frontier_eq_empty:
+   "connected_space X \<and> S \<subseteq> topspace X
+        \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> S = {} \<or> S = topspace X)"
+  by (meson connected_space_eq_frontier_eq_empty frontier_of_empty frontier_of_topspace)
+
+lemma connectedin_eq_subset_separated_union:
+   "connectedin X C \<longleftrightarrow>
+        C \<subseteq> topspace X \<and> (\<forall>S T. separatedin X S T \<and> C \<subseteq> S \<union> T \<longrightarrow> C \<subseteq> S \<or> C \<subseteq> T)" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+  using connectedin_subset_topspace connectedin_subset_separated_union by blast
+next
+  assume ?rhs
+  then show ?lhs
+  by (metis closure_of_subset connectedin_separation dual_order.eq_iff inf.orderE separatedin_def sup.boundedE)
+qed
+
+
+lemma connectedin_clopen_cases:
+   "\<lbrakk>connectedin X C; closedin X T; openin X T\<rbrakk> \<Longrightarrow> C \<subseteq> T \<or> disjnt C T"
+  by (metis Diff_eq_empty_iff Int_empty_right clopenin_eq_frontier_of connectedin_Int_frontier_of disjnt_def)
+
+lemma connected_space_quotient_map_image:
+   "\<lbrakk>quotient_map X X' q; connected_space X\<rbrakk> \<Longrightarrow> connected_space X'"
+  by (metis connectedin_continuous_map_image connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map)
+
+lemma connected_space_retraction_map_image:
+   "\<lbrakk>retraction_map X X' r; connected_space X\<rbrakk> \<Longrightarrow> connected_space X'"
+  using connected_space_quotient_map_image retraction_imp_quotient_map by blast
+
+lemma connectedin_imp_perfect_gen:
+  assumes X: "t1_space X" and S: "connectedin X S" and nontriv: "\<nexists>a. S = {a}"
+  shows "S \<subseteq> X derived_set_of S"
+unfolding derived_set_of_def
+proof (intro subsetI CollectI conjI strip)
+  show XS: "x \<in> topspace X" if "x \<in> S" for x
+    using that S connectedin by fastforce 
+  show "\<exists>y. y \<noteq> x \<and> y \<in> S \<and> y \<in> T"
+    if "x \<in> S" and "x \<in> T \<and> openin X T" for x T
+  proof -
+    have opeXx: "openin X (topspace X - {x})"
+      by (meson X openin_topspace t1_space_openin_delete_alt)
+    moreover
+    have "S \<subseteq> T \<union> (topspace X - {x})"
+      using XS that(2) by auto
+    moreover have "(topspace X - {x}) \<inter> S \<noteq> {}"
+      by (metis Diff_triv S connectedin double_diff empty_subsetI inf_commute insert_subsetI nontriv that(1))
+    ultimately show ?thesis
+      using that connectedinD [OF S, of T "topspace X - {x}"]
+      by blast
+  qed
+qed
+
+lemma connectedin_imp_perfect:
+  "\<lbrakk>Hausdorff_space X; connectedin X S; \<nexists>a. S = {a}\<rbrakk> \<Longrightarrow> S \<subseteq> X derived_set_of S"
+  by (simp add: Hausdorff_imp_t1_space connectedin_imp_perfect_gen)
+
+
+proposition connected_space_prod_topology:
+   "connected_space(prod_topology X Y) \<longleftrightarrow>
+    topspace(prod_topology X Y) = {} \<or> connected_space X \<and> connected_space Y" (is "?lhs=?rhs")
+proof (cases "topspace(prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    using connected_space_topspace_empty by blast
+next
+  case False
+  then have nonempty: "topspace X \<noteq> {}" "topspace Y \<noteq> {}"
+    by force+
+  show ?thesis 
+  proof
+    assume ?lhs
+    then show ?rhs
+      by (meson connected_space_quotient_map_image nonempty quotient_map_fst quotient_map_snd)
+  next
+    assume ?rhs
+    then have conX: "connected_space X" and conY: "connected_space Y"
+      using False by blast+
+    have False
+      if "openin (prod_topology X Y) U" and "openin (prod_topology X Y) V"
+        and UV: "topspace X \<times> topspace Y \<subseteq> U \<union> V" "U \<inter> V = {}" 
+        and "U \<noteq> {}" and "V \<noteq> {}"
+      for U V
+    proof -
+      have Usub: "U \<subseteq> topspace X \<times> topspace Y" and Vsub: "V \<subseteq> topspace X \<times> topspace Y"
+        using that by (metis openin_subset topspace_prod_topology)+
+      obtain a b where ab: "(a,b) \<in> U" and a: "a \<in> topspace X" and b: "b \<in> topspace Y"
+        using \<open>U \<noteq> {}\<close> Usub by auto
+      have "\<not> topspace X \<times> topspace Y \<subseteq> U"
+        using Usub Vsub \<open>U \<inter> V = {}\<close> \<open>V \<noteq> {}\<close> by auto
+      then obtain x y where x: "x \<in> topspace X" and y: "y \<in> topspace Y" and "(x,y) \<notin> U"
+        by blast
+      have oX: "openin X {x \<in> topspace X. (x,y) \<in> U}" "openin X {x \<in> topspace X. (x,y) \<in> V}"
+       and oY: "openin Y {y \<in> topspace Y. (a,y) \<in> U}" "openin Y {y \<in> topspace Y. (a,y) \<in> V}"
+        by (force intro: openin_continuous_map_preimage [where Y = "prod_topology X Y"] 
+            simp: that continuous_map_pairwise o_def x y a)+
+      have 1: "topspace Y \<subseteq> {y \<in> topspace Y. (a,y) \<in> U} \<union> {y \<in> topspace Y. (a,y) \<in> V}"
+        using a that(3) by auto
+      have 2: "{y \<in> topspace Y. (a,y) \<in> U} \<inter> {y \<in> topspace Y. (a,y) \<in> V} = {}"
+        using that(4) by auto
+      have 3: "{y \<in> topspace Y. (a,y) \<in> U} \<noteq> {}"
+        using ab b by auto
+      have 4: "{y \<in> topspace Y. (a,y) \<in> V} \<noteq> {}"
+      proof -
+        show ?thesis
+          using connected_spaceD [OF conX oX] UV \<open>(x,y) \<notin> U\<close> a x y
+                disjoint_iff_not_equal by blast
+      qed
+      show ?thesis
+        using connected_spaceD [OF conY oY 1 2 3 4] by auto
+    qed
+    then show ?lhs
+      unfolding connected_space_def topspace_prod_topology by blast 
+  qed
+qed
+
+lemma connectedin_Times:
+   "connectedin (prod_topology X Y) (S \<times> T) \<longleftrightarrow>
+        S = {} \<or> T = {} \<or> connectedin X S \<and> connectedin Y T"
+  by (force simp: connectedin_def subtopology_Times connected_space_prod_topology)
+
+
+subsection\<open>The notion of "separated between" (complement of "connected between)"\<close>
+
+definition separated_between 
+  where "separated_between X S T \<equiv>
+        \<exists>U V. openin X U \<and> openin X V \<and> U \<union> V = topspace X \<and> disjnt U V \<and> S \<subseteq> U \<and> T \<subseteq> V"
+
+lemma separated_between_alt:
+   "separated_between X S T \<longleftrightarrow>
+        (\<exists>U V. closedin X U \<and> closedin X V \<and> U \<union> V = topspace X \<and> disjnt U V \<and> S \<subseteq> U \<and> T \<subseteq> V)"
+  unfolding separated_between_def
+  by (metis separatedin_open_sets separation_closedin_Un_gen subtopology_topspace 
+            separatedin_closed_sets separation_openin_Un_gen)
+
+lemma separated_between:
+   "separated_between X S T \<longleftrightarrow>
+        (\<exists>U. closedin X U \<and> openin X U \<and> S \<subseteq> U \<and> T \<subseteq> topspace X - U)"
+  unfolding separated_between_def closedin_def disjnt_def
+  by (smt (verit, del_insts) Diff_cancel Diff_disjoint Diff_partition Un_Diff Un_Diff_Int openin_subset)
+
+lemma separated_between_mono:
+   "\<lbrakk>separated_between X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separated_between X S' T'"
+  by (meson order.trans separated_between)
+
+lemma separated_between_refl:
+   "separated_between X S S \<longleftrightarrow> S = {}"
+  unfolding separated_between_def
+  by (metis Un_empty_right disjnt_def disjnt_empty2 disjnt_subset2 disjnt_sym le_iff_inf openin_empty openin_topspace)
+
+lemma separated_between_sym:
+   "separated_between X S T \<longleftrightarrow> separated_between X T S"
+  by (metis disjnt_sym separated_between_alt sup_commute)
+
+lemma separated_between_imp_subset:
+   "separated_between X S T \<Longrightarrow> S \<subseteq> topspace X \<and> T \<subseteq> topspace X"
+  by (metis le_supI1 le_supI2 separated_between_def)
+
+lemma separated_between_empty: 
+  "(separated_between X {} S \<longleftrightarrow> S \<subseteq> topspace X) \<and> (separated_between X S {} \<longleftrightarrow> S \<subseteq> topspace X)"
+  by (metis Diff_empty bot.extremum closedin_empty openin_empty separated_between separated_between_imp_subset separated_between_sym)
+
+
+lemma separated_between_Un: 
+  "separated_between X S (T \<union> U) \<longleftrightarrow> separated_between X S T \<and> separated_between X S U"
+  by (auto simp: separated_between)
+
+lemma separated_between_Un': 
+  "separated_between X (S \<union> T) U \<longleftrightarrow> separated_between X S U \<and> separated_between X T U"
+  by (simp add: separated_between_Un separated_between_sym)
+
+lemma separated_between_imp_disjoint:
+   "separated_between X S T \<Longrightarrow> disjnt S T"
+  by (meson disjnt_iff separated_between_def subsetD)
+
+lemma separated_between_imp_separatedin:
+   "separated_between X S T \<Longrightarrow> separatedin X S T"
+  by (meson separated_between_def separatedin_mono separatedin_open_sets)
+
+lemma separated_between_full:
+  assumes "S \<union> T = topspace X"
+  shows "separated_between X S T \<longleftrightarrow> disjnt S T \<and> closedin X S \<and> openin X S \<and> closedin X T \<and> openin X T"
+proof -
+  have "separated_between X S T \<longrightarrow> separatedin X S T"
+    by (simp add: separated_between_imp_separatedin)
+  then show ?thesis
+    unfolding separated_between_def
+    by (metis assms separation_closedin_Un_gen separation_openin_Un_gen subset_refl subtopology_topspace)
+qed
+
+lemma separated_between_eq_separatedin:
+   "S \<union> T = topspace X \<Longrightarrow> (separated_between X S T \<longleftrightarrow> separatedin X S T)"
+  by (simp add: separated_between_full separatedin_full)
+
+lemma separated_between_pointwise_left:
+  assumes "compactin X S"
+  shows "separated_between X S T \<longleftrightarrow>
+         (S = {} \<longrightarrow> T \<subseteq> topspace X) \<and> (\<forall>x \<in> S. separated_between X {x} T)"  (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using separated_between_imp_subset separated_between_mono by fastforce
+next
+  assume R: ?rhs
+  then have "T \<subseteq> topspace X"
+    by (meson equals0I separated_between_imp_subset)
+  show ?lhs
+  proof -
+    obtain U where U: "\<forall>x \<in> S. openin X (U x)"
+      "\<forall>x \<in> S. \<exists>V. openin X V \<and> U x \<union> V = topspace X \<and> disjnt (U x) V \<and> {x} \<subseteq> U x \<and> T \<subseteq> V"
+      using R unfolding separated_between_def by metis
+    then have "S \<subseteq> \<Union>(U ` S)"
+      by blast
+    then obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> (\<Union>i\<in>K. U i)"
+      using assms U unfolding compactin_def by (smt (verit) finite_subset_image imageE)
+    show ?thesis
+      unfolding separated_between
+    proof (intro conjI exI)
+      have "\<And>x. x \<in> K \<Longrightarrow> closedin X (U x)"
+        by (smt (verit) \<open>K \<subseteq> S\<close> Diff_cancel U(2) Un_Diff Un_Diff_Int disjnt_def openin_closedin_eq subsetD)
+      then show "closedin X (\<Union> (U ` K))"
+        by (metis (mono_tags, lifting) \<open>finite K\<close> closedin_Union finite_imageI image_iff)
+      show "openin X (\<Union> (U ` K))"
+        using U(1) \<open>K \<subseteq> S\<close> by blast
+      show "S \<subseteq> \<Union> (U ` K)"
+        by (simp add: K)
+      have "\<And>x i. \<lbrakk>x \<in> T; i \<in> K; x \<in> U i\<rbrakk> \<Longrightarrow> False"
+        by (meson U(2) \<open>K \<subseteq> S\<close> disjnt_iff subsetD)
+      then show "T \<subseteq> topspace X - \<Union> (U ` K)"
+        using \<open>T \<subseteq> topspace X\<close> by auto
+    qed
+  qed
+qed
+
+lemma separated_between_pointwise_right:
+   "compactin X T
+        \<Longrightarrow> separated_between X S T \<longleftrightarrow> (T = {} \<longrightarrow> S \<subseteq> topspace X) \<and> (\<forall>y \<in> T. separated_between X S {y})"
+  by (meson separated_between_pointwise_left separated_between_sym)
+
+lemma separated_between_closure_of:
+  "S \<subseteq> topspace X \<Longrightarrow> separated_between X (X closure_of S) T \<longleftrightarrow> separated_between X S T"
+  by (meson closure_of_minimal_eq separated_between_alt)
+
+
+lemma separated_between_closure_of':
+ "T \<subseteq> topspace X \<Longrightarrow> separated_between X S (X closure_of T) \<longleftrightarrow> separated_between X S T"
+  by (meson separated_between_closure_of separated_between_sym)
+
+lemma separated_between_closure_of_eq:
+ "separated_between X S T \<longleftrightarrow> S \<subseteq> topspace X \<and> separated_between X (X closure_of S) T"
+  by (metis separated_between_closure_of separated_between_imp_subset)
+
+lemma separated_between_closure_of_eq':
+ "separated_between X S T \<longleftrightarrow> T \<subseteq> topspace X \<and> separated_between X S (X closure_of T)"
+  by (metis separated_between_closure_of' separated_between_imp_subset)
+
+lemma separated_between_frontier_of_eq':
+  "separated_between X S T \<longleftrightarrow>
+   T \<subseteq> topspace X \<and> disjnt S T \<and> separated_between X S (X frontier_of T)" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis interior_of_union_frontier_of separated_between_Un separated_between_closure_of_eq' 
+        separated_between_imp_disjoint)
+next
+  assume R: ?rhs
+  then obtain U where U: "closedin X U" "openin X U" "S \<subseteq> U" "X closure_of T - X interior_of T \<subseteq> topspace X - U"
+    by (metis frontier_of_def separated_between)
+  show ?lhs
+  proof (rule separated_between_mono [of _ S "X closure_of T"])
+    have "separated_between X S T"
+      unfolding separated_between
+    proof (intro conjI exI)
+      show "S \<subseteq> U - T" "T \<subseteq> topspace X - (U - T)"
+        using R U(3) by (force simp: disjnt_iff)+
+      have "T \<subseteq> X closure_of T"
+        by (simp add: R closure_of_subset)
+      then have *: "U - T = U - X interior_of T"
+        using U(4) interior_of_subset by fastforce
+      then show "closedin X (U - T)"
+        by (simp add: U(1) closedin_diff)
+      have "U \<inter> X frontier_of T = {}"
+        using U(4) frontier_of_def by fastforce
+      then show "openin X (U - T)"
+        by (metis * Diff_Un U(2) Un_Diff_Int Un_Int_eq(1) closedin_closure_of interior_of_union_frontier_of openin_diff sup_bot_right)
+    qed
+    then show "separated_between X S (X closure_of T)"
+      by (simp add: R separated_between_closure_of')
+  qed (auto simp: R closure_of_subset)
+qed
+
+lemma separated_between_frontier_of_eq:
+  "separated_between X S T \<longleftrightarrow> S \<subseteq> topspace X \<and> disjnt S T \<and> separated_between X (X frontier_of S) T"
+  by (metis disjnt_sym separated_between_frontier_of_eq' separated_between_sym)
+
+lemma separated_between_frontier_of:
+  "\<lbrakk>S \<subseteq> topspace X; disjnt S T\<rbrakk>
+   \<Longrightarrow> (separated_between X (X frontier_of S) T \<longleftrightarrow> separated_between X S T)"
+  using separated_between_frontier_of_eq by blast
+
+lemma separated_between_frontier_of':
+ "\<lbrakk>T \<subseteq> topspace X; disjnt S T\<rbrakk>
+   \<Longrightarrow> (separated_between X S (X frontier_of T) \<longleftrightarrow> separated_between X S T)"
+  using separated_between_frontier_of_eq' by auto
+
+lemma connected_space_separated_between:
+  "connected_space X \<longleftrightarrow> (\<forall>S T. separated_between X S T \<longrightarrow> S = {} \<or> T = {})" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis Diff_cancel connected_space_clopen_in separated_between subset_empty)
+next
+  assume ?rhs then show ?lhs
+    by (meson connected_space_eq_not_separated separated_between_eq_separatedin)
+qed
+
+lemma connected_space_imp_separated_between_trivial:
+   "connected_space X
+        \<Longrightarrow> (separated_between X S T \<longleftrightarrow> S = {} \<and> T \<subseteq> topspace X \<or> S \<subseteq> topspace X \<and> T = {})"
+  by (metis connected_space_separated_between separated_between_empty)
+
+
+subsection\<open>Connected components\<close>
+
+lemma connected_component_of_subtopology_eq:
+   "connected_component_of (subtopology X U) a = connected_component_of X a \<longleftrightarrow>
+    connected_component_of_set X a \<subseteq> U"
+  by (force simp: connected_component_of_set connectedin_subtopology connected_component_of_def fun_eq_iff subset_iff)
+
+lemma connected_components_of_subtopology:
+  assumes "C \<in> connected_components_of X" "C \<subseteq> U"
+  shows "C \<in> connected_components_of (subtopology X U)"
+proof -
+  obtain a where a: "connected_component_of_set X a \<subseteq> U" and "a \<in> topspace X"
+             and Ceq: "C = connected_component_of_set X a"
+    using assms by (force simp: connected_components_of_def)
+  then have "a \<in> U"
+    by (simp add: connected_component_of_refl in_mono)
+  then have "connected_component_of_set X a = connected_component_of_set (subtopology X U) a"
+    by (metis a connected_component_of_subtopology_eq)
+  then show ?thesis
+    by (simp add: Ceq \<open>a \<in> U\<close> \<open>a \<in> topspace X\<close> connected_component_in_connected_components_of)
+qed
+
+thm connected_space_iff_components_eq
+
+lemma open_in_finite_connected_components:
+  assumes "finite(connected_components_of X)" "C \<in> connected_components_of X"
+  shows "openin X C"
+proof -
+  have "closedin X (topspace X - C)"
+    by (metis DiffD1 assms closedin_Union closedin_connected_components_of complement_connected_components_of_Union finite_Diff)
+  then show ?thesis
+    by (simp add: assms connected_components_of_subset openin_closedin)
+qed
+thm connected_component_of_eq_overlap
+
+lemma connected_components_of_disjoint:
+  assumes "C \<in> connected_components_of X" "C' \<in> connected_components_of X"
+    shows "(disjnt C C' \<longleftrightarrow> (C \<noteq> C'))"
+proof -
+  have "C \<noteq> {}"
+    using nonempty_connected_components_of assms by blast
+  with assms show ?thesis
+    by (metis disjnt_self_iff_empty pairwiseD pairwise_disjoint_connected_components_of)
+qed
+
+lemma connected_components_of_overlap:
+   "\<lbrakk>C \<in> connected_components_of X; C' \<in> connected_components_of X\<rbrakk> \<Longrightarrow> C \<inter> C' \<noteq> {} \<longleftrightarrow> C = C'"
+  by (meson connected_components_of_disjoint disjnt_def)
+
+lemma pairwise_separated_connected_components_of:
+   "pairwise (separatedin X) (connected_components_of X)"
+  by (simp add: closedin_connected_components_of connected_components_of_disjoint pairwiseI separatedin_closed_sets)
+
+lemma finite_connected_components_of_finite:
+   "finite(topspace X) \<Longrightarrow> finite(connected_components_of X)"
+  by (simp add: Union_connected_components_of finite_UnionD)
+
+lemma connected_component_of_unique:
+   "\<lbrakk>x \<in> C; connectedin X C; \<And>C'. x \<in> C' \<and> connectedin X C' \<Longrightarrow> C' \<subseteq> C\<rbrakk>
+        \<Longrightarrow> connected_component_of_set X x = C"
+  by (meson connected_component_of_maximal connectedin_connected_component_of subsetD subset_antisym)
+
+lemma closedin_connected_component_of_subtopology:
+   "\<lbrakk>C \<in> connected_components_of (subtopology X s); X closure_of C \<subseteq> s\<rbrakk> \<Longrightarrow> closedin X C"
+  by (metis closedin_Int_closure_of closedin_connected_components_of closure_of_eq inf.absorb_iff2)
+
+lemma connected_component_of_discrete_topology:
+   "connected_component_of_set (discrete_topology U) x = (if x \<in> U then {x} else {})"
+  by (simp add: locally_path_connected_space_discrete_topology flip: path_component_eq_connected_component_of)
+
+lemma connected_components_of_discrete_topology:
+   "connected_components_of (discrete_topology U) = (\<lambda>x. {x}) ` U"
+  by (simp add: connected_component_of_discrete_topology connected_components_of_def)
+
+lemma connected_component_of_continuous_image:
+   "\<lbrakk>continuous_map X Y f; connected_component_of X x y\<rbrakk>
+        \<Longrightarrow> connected_component_of Y (f x) (f y)"
+  by (meson connected_component_of_def connectedin_continuous_map_image image_eqI)
+
+lemma homeomorphic_map_connected_component_of:
+  assumes "homeomorphic_map X Y f" and x: "x \<in> topspace X"
+  shows "connected_component_of_set Y (f x) = f ` (connected_component_of_set X x)"
+proof -
+  obtain g where g: "continuous_map X Y f"
+    "continuous_map Y X g " "\<And>x. x \<in> topspace X \<Longrightarrow> g (f x) = x" 
+    "\<And>y. y \<in> topspace Y \<Longrightarrow> f (g y) = y"
+    using assms(1) homeomorphic_map_maps homeomorphic_maps_def by fastforce
+  show ?thesis
+    using connected_component_in_topspace [of Y] x g
+          connected_component_of_continuous_image [of X Y f]
+          connected_component_of_continuous_image [of Y X g]
+    by force
+qed
+
+lemma homeomorphic_map_connected_components_of:
+  assumes "homeomorphic_map X Y f"
+  shows "connected_components_of Y = (image f) ` (connected_components_of X)"
+proof -
+  have "topspace Y = f ` topspace X"
+    by (metis assms homeomorphic_imp_surjective_map)
+  with homeomorphic_map_connected_component_of [OF assms] show ?thesis
+    by (auto simp: connected_components_of_def image_iff)
+qed
+
+lemma connected_component_of_pair:
+   "connected_component_of_set (prod_topology X Y) (x,y) =
+        connected_component_of_set X x \<times> connected_component_of_set Y y"
+proof (cases "x \<in> topspace X \<and> y \<in> topspace Y")
+  case True
+  show ?thesis
+  proof (rule connected_component_of_unique)
+    show "(x, y) \<in> connected_component_of_set X x \<times> connected_component_of_set Y y"
+      using True by (simp add: connected_component_of_refl)
+    show "connectedin (prod_topology X Y) (connected_component_of_set X x \<times> connected_component_of_set Y y)"
+      by (metis connectedin_Times connectedin_connected_component_of)
+    show "C \<subseteq> connected_component_of_set X x \<times> connected_component_of_set Y y"
+      if "(x, y) \<in> C \<and> connectedin (prod_topology X Y) C" for C 
+      using that unfolding connected_component_of_def
+      apply clarsimp
+      by (metis (no_types) connectedin_continuous_map_image continuous_map_fst continuous_map_snd fst_conv imageI snd_conv)
+  qed
+next
+  case False then show ?thesis
+    by (metis Sigma_empty1 Sigma_empty2 connected_component_of_eq_empty mem_Sigma_iff topspace_prod_topology)
+qed
+
+lemma connected_components_of_prod_topology:
+  "connected_components_of (prod_topology X Y) =
+    {C \<times> D |C D. C \<in> connected_components_of X \<and> D \<in> connected_components_of Y}" (is "?lhs=?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    apply (clarsimp simp: connected_components_of_def)
+    by (metis (no_types) connected_component_of_pair imageI)
+next
+  show "?rhs \<subseteq> ?lhs"
+    using connected_component_of_pair
+    by (fastforce simp: connected_components_of_def)
+qed
+
+
+lemma connected_component_of_product_topology:
+   "connected_component_of_set (product_topology X I) x =
+    (if x \<in> extensional I then PiE I (\<lambda>i. connected_component_of_set (X i) (x i)) else {})"
+    (is "?lhs = If _ ?R _")    
+proof (cases "x \<in> topspace(product_topology X I)")
+  case True
+  have "?lhs = (\<Pi>\<^sub>E i\<in>I. connected_component_of_set (X i) (x i))"
+    if xX: "\<And>i. i\<in>I \<Longrightarrow> x i \<in> topspace (X i)" and ext: "x \<in> extensional I"
+  proof (rule connected_component_of_unique)
+    show "x \<in> ?R"
+      by (simp add: PiE_iff connected_component_of_refl local.ext xX)
+    show "connectedin (product_topology X I) ?R"
+      by (simp add: connectedin_PiE connectedin_connected_component_of)
+    show "C \<subseteq> ?R"
+      if "x \<in> C \<and> connectedin (product_topology X I) C" for C 
+    proof -
+      have "C \<subseteq> extensional I"
+        using PiE_def connectedin_subset_topspace that by fastforce
+      have "\<And>y. y \<in> C \<Longrightarrow> y \<in> (\<Pi> i\<in>I. connected_component_of_set (X i) (x i))"
+        apply (simp add: connected_component_of_def Pi_def)
+        by (metis connectedin_continuous_map_image continuous_map_product_projection imageI that)
+      then show ?thesis
+        using PiE_def \<open>C \<subseteq> extensional I\<close> by fastforce
+    qed
+  qed
+  with True show ?thesis
+    by (simp add: PiE_iff)
+next
+  case False
+  then show ?thesis
+    apply (simp add: PiE_iff)
+    by (smt (verit) Collect_empty_eq False PiE_eq_empty_iff PiE_iff connected_component_of_eq_empty)
+qed
+
+
+lemma connected_components_of_product_topology:
+   "connected_components_of (product_topology X I) =
+    {PiE I B |B. \<forall>i \<in> I. B i \<in> connected_components_of(X i)}"  (is "?lhs=?rhs")
+proof
+  show "?lhs \<subseteq> ?rhs"
+    by (auto simp: connected_components_of_def connected_component_of_product_topology PiE_iff)
+  show "?rhs \<subseteq> ?lhs"
+  proof
+    fix F
+    assume "F \<in> ?rhs"
+    then obtain B where Feq: "F = Pi\<^sub>E I B" and
+      "\<forall>i\<in>I. \<exists>x\<in>topspace (X i). B i = connected_component_of_set (X i) x"
+      by (force simp: connected_components_of_def connected_component_of_product_topology image_iff)
+    then obtain f where
+      f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i) \<and> B i = connected_component_of_set (X i) (f i)"
+      by metis
+    then have "(\<lambda>i\<in>I. f i) \<in> ((\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> extensional I)"
+      by simp
+    with f show "F \<in> ?lhs"
+      unfolding Feq connected_components_of_def connected_component_of_product_topology image_iff
+      by (smt (verit, del_insts) PiE_cong restrict_PiE_iff restrict_apply' restrict_extensional topspace_product_topology)
+  qed
+qed
+
+
+subsection \<open>Monotone maps (in the general topological sense)\<close>
+
+
+definition monotone_map 
+  where "monotone_map X Y f ==
+        f ` (topspace X) \<subseteq> topspace Y \<and>
+        (\<forall>y \<in> topspace Y. connectedin X {x \<in> topspace X. f x = y})"
+
+lemma monotone_map:
+  "monotone_map X Y f \<longleftrightarrow>
+   f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>y. connectedin X {x \<in> topspace X. f x = y})"
+  apply (simp add: monotone_map_def)
+  by (metis (mono_tags, lifting) connectedin_empty [of X] Collect_empty_eq image_subset_iff) 
+
+
+lemma monotone_map_in_subtopology:
+   "monotone_map X (subtopology Y S) f \<longleftrightarrow> monotone_map X Y f \<and> f ` (topspace X) \<subseteq> S"
+  by (smt (verit, del_insts) le_inf_iff monotone_map topspace_subtopology)
+
+lemma monotone_map_from_subtopology:
+  assumes "monotone_map X Y f" 
+    "\<And>x y. x \<in> topspace X \<and> y \<in> topspace X \<and> x \<in> S \<and> f x = f y \<Longrightarrow> y \<in> S"
+  shows "monotone_map (subtopology X S) Y f"
+  using assms
+  unfolding monotone_map_def connectedin_subtopology
+  by (smt (verit, del_insts) Collect_cong Collect_empty_eq IntE IntI connectedin_empty image_subset_iff mem_Collect_eq subsetI topspace_subtopology)
+
+lemma monotone_map_restriction:
+  "monotone_map X Y f \<and> {x \<in> topspace X. f x \<in> v} = u
+        \<Longrightarrow> monotone_map (subtopology X u) (subtopology Y v) f"
+  by (smt (verit, best) IntI Int_Collect image_subset_iff mem_Collect_eq monotone_map monotone_map_from_subtopology topspace_subtopology)
+
+lemma injective_imp_monotone_map:
+  assumes "f ` topspace X \<subseteq> topspace Y"  "inj_on f (topspace X)"
+  shows "monotone_map X Y f"
+  unfolding monotone_map_def
+proof (intro conjI assms strip)
+  fix y
+  assume "y \<in> topspace Y"
+  then have "{x \<in> topspace X. f x = y} = {} \<or> (\<exists>a \<in> topspace X. {x \<in> topspace X. f x = y} = {a})"
+    using assms(2) unfolding inj_on_def by blast
+  then show "connectedin X {x \<in> topspace X. f x = y}"
+    by (metis (no_types, lifting) connectedin_empty connectedin_sing)
+qed
+
+lemma embedding_imp_monotone_map:
+   "embedding_map X Y f \<Longrightarrow> monotone_map X Y f"
+  by (metis (no_types) embedding_map_def homeomorphic_eq_everything_map inf.absorb_iff2 injective_imp_monotone_map topspace_subtopology)
+
+lemma section_imp_monotone_map:
+   "section_map X Y f \<Longrightarrow> monotone_map X Y f"
+  by (simp add: embedding_imp_monotone_map section_imp_embedding_map)
+
+lemma homeomorphic_imp_monotone_map:
+   "homeomorphic_map X Y f \<Longrightarrow> monotone_map X Y f"
+  by (meson section_and_retraction_eq_homeomorphic_map section_imp_monotone_map)
+
+proposition connected_space_monotone_quotient_map_preimage:
+  assumes f: "monotone_map X Y f" "quotient_map X Y f" and "connected_space Y"
+  shows "connected_space X"
+proof (rule ccontr)
+  assume "\<not> connected_space X"
+  then obtain U V where "openin X U" "openin X V" "U \<inter> V = {}"
+    "U \<noteq> {}" "V \<noteq> {}" and topUV: "topspace X \<subseteq> U \<union> V"
+    by (auto simp: connected_space_def)
+  then have UVsub: "U \<subseteq> topspace X" "V \<subseteq> topspace X"
+    by (auto simp: openin_subset)
+  have "\<not> connected_space Y"
+    unfolding connected_space_def not_not
+  proof (intro exI conjI)
+    show "topspace Y \<subseteq> f`U \<union> f`V"
+      by (metis f(2) image_Un quotient_imp_surjective_map subset_Un_eq topUV)
+    show "f`U \<noteq> {}"
+      by (simp add: \<open>U \<noteq> {}\<close>)
+    show "(f`V) \<noteq> {}"
+      by (simp add: \<open>V \<noteq> {}\<close>)
+    have *: "y \<notin> f ` V" if "y \<in> f ` U" for y
+    proof -
+      have \<section>: "connectedin X {x \<in> topspace X. f x = y}"
+        using f(1) monotone_map by fastforce
+      show ?thesis
+        using connectedinD [OF \<section> \<open>openin X U\<close> \<open>openin X V\<close>] UVsub topUV \<open>U \<inter> V = {}\<close> that
+        by (force simp: disjoint_iff)
+    qed
+    then show "f`U \<inter> f`V = {}"
+      by blast
+    show "openin Y (f`U)"
+      using f \<open>openin X U\<close> topUV * unfolding quotient_map_saturated_open by force
+    show "openin Y (f`V)"
+      using f \<open>openin X V\<close> topUV * unfolding quotient_map_saturated_open by force
+  qed
+  then show False
+    by (simp add: assms)
+qed
+
+lemma connectedin_monotone_quotient_map_preimage:
+  assumes "monotone_map X Y f" "quotient_map X Y f" "connectedin Y C" "openin Y C \<or> closedin Y C"
+  shows "connectedin X {x \<in> topspace X. f x \<in> C}"
+proof -
+  have "connected_space (subtopology X {x \<in> topspace X. f x \<in> C})"
+  proof -
+    have "connected_space (subtopology Y C)"
+      using \<open>connectedin Y C\<close> connectedin_def by blast
+    moreover have "quotient_map (subtopology X {a \<in> topspace X. f a \<in> C}) (subtopology Y C) f"
+      by (simp add: assms quotient_map_restriction)
+    ultimately show ?thesis
+      using \<open>monotone_map X Y f\<close> connected_space_monotone_quotient_map_preimage monotone_map_restriction by blast
+  qed
+  then show ?thesis
+    by (simp add: connectedin_def)
+qed
+
+lemma monotone_open_map:
+  assumes "continuous_map X Y f" "open_map X Y f" and fim: "f ` (topspace X) = topspace Y"
+  shows "monotone_map X Y f \<longleftrightarrow> (\<forall>C. connectedin Y C \<longrightarrow> connectedin X {x \<in> topspace X. f x \<in> C})"
+         (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  show ?rhs
+    unfolding connectedin_def
+  proof (intro strip conjI)
+    fix C
+    assume C: "C \<subseteq> topspace Y \<and> connected_space (subtopology Y C)"
+    show "connected_space (subtopology X {x \<in> topspace X. f x \<in> C})"
+    proof (rule connected_space_monotone_quotient_map_preimage)
+      show "monotone_map (subtopology X {x \<in> topspace X. f x \<in> C}) (subtopology Y C) f"
+        by (simp add: L monotone_map_restriction)
+      show "quotient_map (subtopology X {x \<in> topspace X. f x \<in> C}) (subtopology Y C) f"
+      proof (rule continuous_open_imp_quotient_map)
+        show "continuous_map (subtopology X {x \<in> topspace X. f x \<in> C}) (subtopology Y C) f"
+          using assms continuous_map_from_subtopology continuous_map_in_subtopology by fastforce
+      qed (use open_map_restriction assms in fastforce)+
+    qed (simp add: C)
+  qed auto
+next
+  assume ?rhs 
+  then have "\<forall>y. connectedin Y {y} \<longrightarrow> connectedin X {x \<in> topspace X. f x = y}"
+    by (smt (verit) Collect_cong singletonD singletonI)
+  then show ?lhs
+    by (simp add: fim monotone_map_def)
+qed
+
+lemma monotone_closed_map:
+  assumes "continuous_map X Y f" "closed_map X Y f" and fim: "f ` (topspace X) = topspace Y"
+  shows "monotone_map X Y f \<longleftrightarrow> (\<forall>C. connectedin Y C \<longrightarrow> connectedin X {x \<in> topspace X. f x \<in> C})" 
+         (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  show ?rhs
+    unfolding connectedin_def
+  proof (intro strip conjI)
+    fix C
+    assume C: "C \<subseteq> topspace Y \<and> connected_space (subtopology Y C)"
+    show "connected_space (subtopology X {x \<in> topspace X. f x \<in> C})"
+    proof (rule connected_space_monotone_quotient_map_preimage)
+      show "monotone_map (subtopology X {x \<in> topspace X. f x \<in> C}) (subtopology Y C) f"
+        by (simp add: L monotone_map_restriction)
+      show "quotient_map (subtopology X {x \<in> topspace X. f x \<in> C}) (subtopology Y C) f"
+      proof (rule continuous_closed_imp_quotient_map)
+        show "continuous_map (subtopology X {x \<in> topspace X. f x \<in> C}) (subtopology Y C) f"
+          using assms continuous_map_from_subtopology continuous_map_in_subtopology by fastforce
+      qed (use closed_map_restriction assms in fastforce)+
+    qed (simp add: C)
+  qed auto
+next
+  assume ?rhs 
+  then have "\<forall>y. connectedin Y {y} \<longrightarrow> connectedin X {x \<in> topspace X. f x = y}"
+    by (smt (verit) Collect_cong singletonD singletonI)
+  then show ?lhs
+    by (simp add: fim monotone_map_def)
+qed
+
+subsection\<open>Other countability properties\<close>
+
+definition second_countable
+  where "second_countable X \<equiv>
+         \<exists>\<B>. countable \<B> \<and> (\<forall>V \<in> \<B>. openin X V) \<and>
+             (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U))"
+
+definition first_countable
+  where "first_countable X \<equiv>
+        \<forall>x \<in> topspace X.
+         \<exists>\<B>. countable \<B> \<and> (\<forall>V \<in> \<B>. openin X V) \<and>
+             (\<forall>U. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U))"
+
+definition separable_space
+  where "separable_space X \<equiv>
+        \<exists>C. countable C \<and> C \<subseteq> topspace X \<and> X closure_of C = topspace X"
+
+lemma second_countable:
+   "second_countable X \<longleftrightarrow>
+        (\<exists>\<B>. countable \<B> \<and> openin X = arbitrary union_of (\<lambda>x. x \<in> \<B>))"
+  by (smt (verit) openin_topology_base_unique second_countable_def)
+
+lemma second_countable_subtopology:
+  assumes "second_countable X"
+  shows "second_countable (subtopology X S)"
+proof -
+  obtain \<B> where \<B>: "countable \<B>" "\<And>V. V \<in> \<B> \<Longrightarrow> openin X V"
+    "\<And>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U)"
+    using assms by (auto simp: second_countable_def)
+  show ?thesis
+    unfolding second_countable_def
+  proof (intro exI conjI)
+    show "\<forall>V\<in>((\<inter>)S) ` \<B>. openin (subtopology X S) V"
+      using openin_subtopology_Int2 \<B> by blast
+    show "\<forall>U x. openin (subtopology X S) U \<and> x \<in> U \<longrightarrow> (\<exists>V\<in>((\<inter>)S) ` \<B>. x \<in> V \<and> V \<subseteq> U)"
+      using \<B> unfolding openin_subtopology
+      by (smt (verit, del_insts) IntI image_iff inf_commute inf_le1 subset_iff)
+  qed (use \<B> in auto)
+qed
+
+
+lemma second_countable_discrete_topology:
+   "second_countable(discrete_topology U) \<longleftrightarrow> countable U" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then
+  obtain \<B> where \<B>: "countable \<B>" "\<And>V. V \<in> \<B> \<Longrightarrow> V \<subseteq> U"
+    "\<And>W x. W \<subseteq> U \<and> x \<in> W \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> W)"
+    by (auto simp: second_countable_def)
+  then have "{x} \<in> \<B>" if "x \<in> U" for x
+    by (metis empty_subsetI insertCI insert_subset subset_antisym that)
+  then show ?rhs
+    by (smt (verit) countable_subset image_subsetI \<open>countable \<B>\<close> countable_image_inj_on [OF _ inj_singleton])
+next
+  assume ?rhs 
+  then show ?lhs
+    unfolding second_countable_def
+    by (rule_tac x="(\<lambda>x. {x}) ` U" in exI) auto
+qed
+
+lemma second_countable_open_map_image:
+  assumes "continuous_map X Y f" "open_map X Y f" 
+   and fim: "f ` (topspace X) = topspace Y" and "second_countable X"
+ shows "second_countable Y"
+proof -
+  have openXYf: "\<And>U. openin X U \<longrightarrow> openin Y (f ` U)"
+    using assms by (auto simp: open_map_def)
+  obtain \<B> where \<B>: "countable \<B>" "\<And>V. V \<in> \<B> \<Longrightarrow> openin X V"
+    and *: "\<And>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U)"
+    using assms by (auto simp: second_countable_def)
+  show ?thesis
+    unfolding second_countable_def
+  proof (intro exI conjI strip)
+    fix V y
+    assume V: "openin Y V \<and> y \<in> V"
+    then obtain x where "x \<in> topspace X" and x: "f x = y"
+      by (metis fim image_iff openin_subset subsetD)
+
+    then obtain W where "W\<in>\<B>" "x \<in> W" "W \<subseteq> {x \<in> topspace X. f x \<in> V}"
+      using * [of "{x \<in> topspace X. f x \<in> V}" x] V assms openin_continuous_map_preimage 
+      by force
+    then show "\<exists>W \<in> (image f) ` \<B>. y \<in> W \<and> W \<subseteq> V"
+      using x by auto
+  qed (use \<B> openXYf in auto)
+qed
+
+lemma homeomorphic_space_second_countability:
+   "X homeomorphic_space Y \<Longrightarrow> (second_countable X \<longleftrightarrow> second_countable Y)"
+  by (meson homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym second_countable_open_map_image)
+
+lemma second_countable_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; second_countable X\<rbrakk> \<Longrightarrow> second_countable Y"
+  using hereditary_imp_retractive_property homeomorphic_space_second_countability second_countable_subtopology by blast
+
+lemma second_countable_imp_first_countable:
+   "second_countable X \<Longrightarrow> first_countable X"
+  by (metis first_countable_def second_countable_def)
+
+lemma first_countable_subtopology:
+  assumes "first_countable X"
+  shows "first_countable (subtopology X S)"
+  unfolding first_countable_def
+proof
+  fix x
+  assume "x \<in> topspace (subtopology X S)"
+  then obtain \<B> where "countable \<B>" and \<B>: "\<And>V. V \<in> \<B> \<Longrightarrow> openin X V"
+    "\<And>U. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U)"
+    using assms first_countable_def by force
+  show "\<exists>\<B>. countable \<B> \<and> (\<forall>V\<in>\<B>. openin (subtopology X S) V) \<and> (\<forall>U. openin (subtopology X S) U \<and> x \<in> U \<longrightarrow> (\<exists>V\<in>\<B>. x \<in> V \<and> V \<subseteq> U))"
+  proof (intro exI conjI strip)
+    show "countable (((\<inter>)S) ` \<B>)"
+      using \<open>countable \<B>\<close> by blast
+    show "openin (subtopology X S) V" if "V \<in> ((\<inter>)S) ` \<B>" for V
+      using \<B> openin_subtopology_Int2 that by fastforce
+    show "\<exists>V\<in>((\<inter>)S) ` \<B>. x \<in> V \<and> V \<subseteq> U"
+      if "openin (subtopology X S) U \<and> x \<in> U" for U 
+      using that \<B>(2) by (clarsimp simp: openin_subtopology) (meson le_infI2)
+  qed
+qed
+
+lemma first_countable_discrete_topology:
+   "first_countable (discrete_topology U)"
+  unfolding first_countable_def topspace_discrete_topology openin_discrete_topology
+proof
+  fix x assume "x \<in> U"
+  show "\<exists>\<B>. countable \<B> \<and> (\<forall>V\<in>\<B>. V \<subseteq> U) \<and> (\<forall>Ua. Ua \<subseteq> U \<and> x \<in> Ua \<longrightarrow> (\<exists>V\<in>\<B>. x \<in> V \<and> V \<subseteq> Ua))"
+    using \<open>x \<in> U\<close> by (rule_tac x="{{x}}" in exI) auto
+qed
+
+lemma first_countable_open_map_image:
+  assumes "continuous_map X Y f" "open_map X Y f" 
+   and fim: "f ` (topspace X) = topspace Y" and "first_countable X"
+ shows "first_countable Y"
+  unfolding first_countable_def
+proof
+  fix y
+  assume "y \<in> topspace Y"
+  have openXYf: "\<And>U. openin X U \<longrightarrow> openin Y (f ` U)"
+    using assms by (auto simp: open_map_def)
+  then obtain x where x: "x \<in> topspace X" "f x = y"
+    by (metis \<open>y \<in> topspace Y\<close> fim imageE)
+  obtain \<B> where \<B>: "countable \<B>" "\<And>V. V \<in> \<B> \<Longrightarrow> openin X V"
+    and *: "\<And>U. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U)"
+    using assms x first_countable_def by force
+  show "\<exists>\<B>. countable \<B> \<and>
+              (\<forall>V\<in>\<B>. openin Y V) \<and> (\<forall>U. openin Y U \<and> y \<in> U \<longrightarrow> (\<exists>V\<in>\<B>. y \<in> V \<and> V \<subseteq> U))"
+  proof (intro exI conjI strip)
+    fix V assume "openin Y V \<and> y \<in> V"
+    then have "\<exists>W\<in>\<B>. x \<in> W \<and> W \<subseteq> {x \<in> topspace X. f x \<in> V}"
+      using * [of "{x \<in> topspace X. f x \<in> V}"] assms openin_continuous_map_preimage x 
+      by fastforce
+    then show "\<exists>V' \<in> (image f) ` \<B>. y \<in> V' \<and> V' \<subseteq> V"
+      using image_mono x by auto 
+  qed (use \<B> openXYf in force)+
+qed
+
+lemma homeomorphic_space_first_countability:
+  "X homeomorphic_space Y \<Longrightarrow> first_countable X \<longleftrightarrow> first_countable Y"
+  by (meson first_countable_open_map_image homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym)
+
+lemma first_countable_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; first_countable X\<rbrakk> \<Longrightarrow> first_countable Y"
+  using first_countable_subtopology hereditary_imp_retractive_property homeomorphic_space_first_countability by blast
+
+lemma separable_space_open_subset:
+  assumes "separable_space X" "openin X S"
+  shows "separable_space (subtopology X S)"
+proof -
+  obtain C where C: "countable C" "C \<subseteq> topspace X" "X closure_of C = topspace X"
+    by (meson assms separable_space_def)
+  then have "\<And>x T. \<lbrakk>x \<in> topspace X; x \<in> T; openin (subtopology X S) T\<rbrakk>
+           \<Longrightarrow> \<exists>y. y \<in> S \<and> y \<in> C \<and> y \<in> T"
+    by (smt (verit) \<open>openin X S\<close> in_closure_of openin_open_subtopology subsetD)
+  with C \<open>openin X S\<close> show ?thesis
+    unfolding separable_space_def
+    by (rule_tac x="S \<inter> C" in exI) (force simp: in_closure_of)
+qed
+
+lemma separable_space_continuous_map_image:
+  assumes "separable_space X" "continuous_map X Y f" 
+    and fim: "f ` (topspace X) = topspace Y"
+  shows "separable_space Y"
+proof -
+  have cont: "\<And>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
+    by (simp add: assms continuous_map_image_closure_subset)
+  obtain C where C: "countable C" "C \<subseteq> topspace X" "X closure_of C = topspace X"
+    by (meson assms separable_space_def)
+  then show ?thesis
+    unfolding separable_space_def
+    by (metis cont fim closure_of_subset_topspace countable_image image_mono subset_antisym)
+qed
+
+lemma separable_space_quotient_map_image:
+  "\<lbrakk>quotient_map X Y q; separable_space X\<rbrakk> \<Longrightarrow> separable_space Y"
+  by (meson quotient_imp_continuous_map quotient_imp_surjective_map separable_space_continuous_map_image)
+
+lemma separable_space_retraction_map_image:
+  "\<lbrakk>retraction_map X Y r; separable_space X\<rbrakk> \<Longrightarrow> separable_space Y"
+  using retraction_imp_quotient_map separable_space_quotient_map_image by blast
+
+lemma homeomorphic_separable_space:
+  "X homeomorphic_space Y \<Longrightarrow> (separable_space X \<longleftrightarrow> separable_space Y)"
+  by (meson homeomorphic_eq_everything_map homeomorphic_maps_map homeomorphic_space_def separable_space_continuous_map_image)
+
+lemma separable_space_discrete_topology:
+   "separable_space(discrete_topology U) \<longleftrightarrow> countable U"
+  by (metis countable_Int2 discrete_topology_closure_of dual_order.refl inf.orderE separable_space_def topspace_discrete_topology)
+
+lemma second_countable_imp_separable_space:
+  assumes "second_countable X"
+  shows "separable_space X"
+proof -
+  obtain \<B> where \<B>: "countable \<B>" "\<And>V. V \<in> \<B> \<Longrightarrow> openin X V"
+    and *: "\<And>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U)"
+    using assms by (auto simp: second_countable_def)
+  obtain c where c: "\<And>V. \<lbrakk>V \<in> \<B>; V \<noteq> {}\<rbrakk> \<Longrightarrow> c V \<in> V"
+    by (metis all_not_in_conv)
+  then have **: "\<And>x. x \<in> topspace X \<Longrightarrow> x \<in> X closure_of c ` (\<B> - {{}})"
+    using * by (force simp: closure_of_def)
+  show ?thesis
+    unfolding separable_space_def
+  proof (intro exI conjI)
+    show "countable (c ` (\<B>-{{}}))"
+      using \<B>(1) by blast
+    show "(c ` (\<B>-{{}})) \<subseteq> topspace X"
+      using \<B>(2) c openin_subset by fastforce
+    show "X closure_of (c ` (\<B>-{{}})) = topspace X"
+      by (meson ** closure_of_subset_topspace subsetI subset_antisym)
+  qed
+qed
+
+lemma second_countable_imp_Lindelof_space:
+  assumes "second_countable X"
+  shows "Lindelof_space X"
+unfolding Lindelof_space_def
+proof clarify
+  fix \<U>
+  assume "\<forall>U \<in> \<U>. openin X U" and UU: "\<Union>\<U> = topspace X"
+  obtain \<B> where \<B>: "countable \<B>" "\<And>V. V \<in> \<B> \<Longrightarrow> openin X V"
+    and *: "\<And>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \<B>. x \<in> V \<and> V \<subseteq> U)"
+    using assms by (auto simp: second_countable_def)
+  define \<B>' where "\<B>' = {B \<in> \<B>. \<exists>U. U \<in> \<U> \<and> B \<subseteq> U}"
+  have \<B>': "countable \<B>'" "\<Union>\<B>' = \<Union>\<U>"
+    using \<B> using "*" \<open>\<forall>U\<in>\<U>. openin X U\<close> by (fastforce simp: \<B>'_def)+
+  have "\<And>b. \<exists>U. b \<in> \<B>' \<longrightarrow> U \<in> \<U> \<and> b \<subseteq> U" 
+    by (simp add: \<B>'_def)
+  then obtain G where G: "\<And>b. b \<in> \<B>' \<longrightarrow> G b \<in> \<U> \<and> b \<subseteq> G b" 
+    by metis
+  with \<B>' UU show "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \<U> \<and> \<Union>\<V> = topspace X"
+    by (rule_tac x="G ` \<B>'" in exI) fastforce
+qed
+
+subsection \<open>Neigbourhood bases EXTRAS\<close>
+(* Neigbourhood bases (useful for "local" properties of various kind).       *)
+
+lemma openin_topology_neighbourhood_base_unique:
+   "openin X = arbitrary union_of P \<longleftrightarrow>
+        (\<forall>u. P u \<longrightarrow> openin X u) \<and> neighbourhood_base_of P X"
+  by (smt (verit, best) open_neighbourhood_base_of openin_topology_base_unique)
+
+lemma neighbourhood_base_at_topology_base:
+   "        openin X = arbitrary union_of b
+        \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow>
+             (\<forall>w. b w \<and> x \<in> w \<longrightarrow> (\<exists>u v. openin X u \<and> P v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> w)))"
+  apply (simp add: neighbourhood_base_at_def)
+  by (smt (verit, del_insts) openin_topology_base_unique subset_trans)
+
+lemma neighbourhood_base_of_unlocalized:
+  assumes "\<And>S t. P S \<and> openin X t \<and> (t \<noteq> {}) \<and> t \<subseteq> S \<Longrightarrow> P t"
+  shows "neighbourhood_base_of P X \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. \<exists>u v. openin X u \<and> P v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> topspace X)"
+  apply (simp add: neighbourhood_base_of_def)
+  by (smt (verit, ccfv_SIG) assms empty_iff neighbourhood_base_at_unlocalized)
+
+lemma neighbourhood_base_at_discrete_topology:
+   "neighbourhood_base_at x P (discrete_topology u) \<longleftrightarrow> x \<in> u \<Longrightarrow> P {x}"
+  apply (simp add: neighbourhood_base_at_def)
+  by (smt (verit) empty_iff empty_subsetI insert_subset singletonI subsetD subset_singletonD)
+
+lemma neighbourhood_base_of_discrete_topology:
+   "neighbourhood_base_of P (discrete_topology u) \<longleftrightarrow> (\<forall>x \<in> u. P {x})"
+  apply (simp add: neighbourhood_base_of_def)
+  using neighbourhood_base_at_discrete_topology[of _ P u]
+  by (metis empty_subsetI insert_subset neighbourhood_base_at_def openin_discrete_topology singletonI)
+
+lemma second_countable_neighbourhood_base_alt:
+  "second_countable X \<longleftrightarrow> 
+  (\<exists>\<B>. countable \<B> \<and> (\<forall>V \<in> \<B>. openin X V) \<and> neighbourhood_base_of (\<lambda>A. A\<in>\<B>) X)"
+  by (metis (full_types) openin_topology_neighbourhood_base_unique second_countable)
+
+lemma first_countable_neighbourhood_base_alt:
+   "first_countable X \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. \<exists>\<B>. countable \<B> \<and> (\<forall>V \<in> \<B>. openin X V) \<and> neighbourhood_base_at x (\<lambda>V. V \<in> \<B>) X)"
+  unfolding first_countable_def
+  apply (intro ball_cong refl ex_cong conj_cong)
+  by (metis (mono_tags, lifting) open_neighbourhood_base_at)
+
+lemma second_countable_neighbourhood_base:
+   "second_countable X \<longleftrightarrow>
+        (\<exists>\<B>. countable \<B> \<and> neighbourhood_base_of (\<lambda>V. V \<in> \<B>) X)" (is "?lhs=?rhs")
+proof
+  assume ?lhs 
+  then show ?rhs
+    using second_countable_neighbourhood_base_alt by blast
+next
+  assume ?rhs 
+  then obtain \<B> where "countable \<B>"
+    and \<B>: "\<And>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. openin X U \<and> (\<exists>V. V \<in> \<B> \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
+    by (metis neighbourhood_base_of)
+  then show ?lhs
+    unfolding second_countable_neighbourhood_base_alt neighbourhood_base_of
+    apply (rule_tac x="(\<lambda>u. X interior_of u) ` \<B>" in exI)
+    by (smt (verit, best) interior_of_eq interior_of_mono countable_image image_iff openin_interior_of)
+qed
+
+lemma first_countable_neighbourhood_base:
+   "first_countable X \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. \<exists>\<B>. countable \<B> \<and> neighbourhood_base_at x (\<lambda>V. V \<in> \<B>) X)" (is "?lhs=?rhs")
+proof
+  assume ?lhs 
+  then show ?rhs
+    by (metis first_countable_neighbourhood_base_alt)
+next
+  assume R: ?rhs 
+  show ?lhs
+    unfolding first_countable_neighbourhood_base_alt
+  proof
+    fix x
+    assume "x \<in> topspace X"
+    with R obtain \<B> where "countable \<B>" and \<B>: "neighbourhood_base_at x (\<lambda>V. V \<in> \<B>) X"
+      by blast
+    then
+    show "\<exists>\<B>. countable \<B> \<and> Ball \<B> (openin X) \<and> neighbourhood_base_at x (\<lambda>V. V \<in> \<B>) X"
+      unfolding neighbourhood_base_at_def
+      apply (rule_tac x="(\<lambda>u. X interior_of u) ` \<B>" in exI)
+      by (smt (verit, best) countable_image image_iff interior_of_eq interior_of_mono openin_interior_of)
+  qed
+qed
+
+
+subsection\<open>T_0 spaces and the Kolmogorov quotient\<close>
+
+definition t0_space where
+  "t0_space X \<equiv>
+     \<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x \<noteq> y \<longrightarrow> (\<exists>U. openin X U \<and> (x \<notin> U \<longleftrightarrow> y \<in> U))"
+
+lemma t0_space_expansive:
+   "\<lbrakk>topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> t0_space X \<Longrightarrow> t0_space Y"
+  by (metis t0_space_def)
+
+lemma t1_imp_t0_space: "t1_space X \<Longrightarrow> t0_space X"
+  by (metis t0_space_def t1_space_def)
+
+lemma t1_eq_symmetric_t0_space_alt:
+   "t1_space X \<longleftrightarrow>
+      t0_space X \<and>
+      (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x \<in> X closure_of {y} \<longleftrightarrow> y \<in> X closure_of {x})"
+  apply (simp add: t0_space_def t1_space_def closure_of_def)
+  by (smt (verit, best) openin_topspace)
+
+lemma t1_eq_symmetric_t0_space:
+  "t1_space X \<longleftrightarrow> t0_space X \<and> (\<forall>x y. x \<in> X closure_of {y} \<longleftrightarrow> y \<in> X closure_of {x})"
+  by (auto simp: t1_eq_symmetric_t0_space_alt in_closure_of)
+
+lemma Hausdorff_imp_t0_space:
+   "Hausdorff_space X \<Longrightarrow> t0_space X"
+  by (simp add: Hausdorff_imp_t1_space t1_imp_t0_space)
+
+lemma t0_space:
+   "t0_space X \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x \<noteq> y \<longrightarrow> (\<exists>C. closedin X C \<and> (x \<notin> C \<longleftrightarrow> y \<in> C)))"
+  unfolding t0_space_def by (metis Diff_iff closedin_def openin_closedin_eq)
+
+lemma homeomorphic_t0_space:
+  assumes "X homeomorphic_space Y"
+  shows "t0_space X \<longleftrightarrow> t0_space Y"
+proof -
+  obtain f where f: "homeomorphic_map X Y f" and F: "inj_on f (topspace X)" and "topspace Y = f ` topspace X"
+    by (metis assms homeomorphic_imp_injective_map homeomorphic_imp_surjective_map homeomorphic_space)
+  with inj_on_image_mem_iff [OF F] 
+  show ?thesis
+    apply (simp add: t0_space_def homeomorphic_eq_everything_map continuous_map_def open_map_def inj_on_def)
+    by (smt (verit)  mem_Collect_eq openin_subset)
+qed
+
+lemma t0_space_closure_of_sing:
+   "t0_space X \<longleftrightarrow>
+    (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. X closure_of {x} = X closure_of {y} \<longrightarrow> x = y)"
+  by (simp add: t0_space_def closure_of_def set_eq_iff) (smt (verit))
+
+lemma t0_space_discrete_topology: "t0_space (discrete_topology S)"
+  by (simp add: Hausdorff_imp_t0_space)
+
+lemma t0_space_subtopology: "t0_space X \<Longrightarrow> t0_space (subtopology X U)"
+  by (simp add: t0_space_def openin_subtopology) (metis Int_iff)
+
+lemma t0_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; t0_space X\<rbrakk> \<Longrightarrow> t0_space Y"
+  using hereditary_imp_retractive_property homeomorphic_t0_space t0_space_subtopology by blast
+
+lemma XY: "{x}\<times>{y} = {(x,y)}"
+  by simp
+
+lemma t0_space_prod_topologyI: "\<lbrakk>t0_space X; t0_space Y\<rbrakk> \<Longrightarrow> t0_space (prod_topology X Y)"
+  by (simp add: t0_space_closure_of_sing closure_of_Times closure_of_eq_empty_gen times_eq_iff flip: XY insert_Times_insert)
+
+
+lemma t0_space_prod_topology_iff:
+   "t0_space (prod_topology X Y) \<longleftrightarrow> topspace (prod_topology X Y) = {} \<or> t0_space X \<and> t0_space Y" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (metis Sigma_empty1 Sigma_empty2 retraction_map_fst retraction_map_snd t0_space_retraction_map_image topspace_prod_topology)
+qed (metis empty_iff t0_space_def t0_space_prod_topologyI)
+
+proposition t0_space_product_topology:
+   "t0_space (product_topology X I) \<longleftrightarrow>
+        topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t0_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (meson retraction_map_product_projection t0_space_retraction_map_image)
+next
+  assume R: ?rhs 
+  show ?lhs
+  proof (cases "topspace(product_topology X I) = {}")
+    case True
+    then show ?thesis
+      by (simp add: t0_space_def)
+  next
+    case False
+    show ?thesis
+      unfolding t0_space
+    proof (intro strip)
+      fix x y
+      assume x: "x \<in> topspace (product_topology X I)"
+        and y: "y \<in> topspace (product_topology X I)"
+        and "x \<noteq> y"
+      then obtain i where "i \<in> I" "x i \<noteq> y i"
+        by (metis PiE_ext topspace_product_topology)
+      then have "t0_space (X i)"
+        using False R by blast
+      then obtain U where "closedin (X i) U" "(x i \<notin> U \<longleftrightarrow> y i \<in> U)"
+        by (metis t0_space PiE_mem \<open>i \<in> I\<close> \<open>x i \<noteq> y i\<close> topspace_product_topology x y)
+      with \<open>i \<in> I\<close> x y show "\<exists>U. closedin (product_topology X I) U \<and> (x \<notin> U) = (y \<in> U)"
+        by (rule_tac x="PiE I (\<lambda>j. if j = i then U else topspace(X j))" in exI)
+          (simp add: closedin_product_topology PiE_iff)
+    qed
+  qed
+qed
+
+
+subsection \<open>Kolmogorov quotients\<close>
+
+definition Kolmogorov_quotient 
+  where "Kolmogorov_quotient X \<equiv> \<lambda>x. @y. \<forall>U. openin X U \<longrightarrow> (y \<in> U \<longleftrightarrow> x \<in> U)"
+
+lemma Kolmogorov_quotient_in_open:
+   "openin X U \<Longrightarrow> (Kolmogorov_quotient X x \<in> U \<longleftrightarrow> x \<in> U)"
+  by (smt (verit, ccfv_SIG) Kolmogorov_quotient_def someI_ex)
+
+lemma Kolmogorov_quotient_in_topspace:
+   "Kolmogorov_quotient X x \<in> topspace X \<longleftrightarrow> x \<in> topspace X"
+  by (simp add: Kolmogorov_quotient_in_open)
+
+lemma Kolmogorov_quotient_in_closed:
+  "closedin X C \<Longrightarrow> (Kolmogorov_quotient X x \<in> C \<longleftrightarrow> x \<in> C)"
+  unfolding closedin_def
+  by (meson DiffD2 DiffI Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace in_mono)
+ 
+lemma continuous_map_Kolmogorov_quotient:
+   "continuous_map X X (Kolmogorov_quotient X)"
+  using Kolmogorov_quotient_in_open openin_subopen openin_subset 
+    by (fastforce simp: continuous_map_def Kolmogorov_quotient_in_topspace)
+
+lemma open_map_Kolmogorov_quotient_explicit:
+   "openin X U \<Longrightarrow> Kolmogorov_quotient X ` U = Kolmogorov_quotient X ` topspace X \<inter> U"
+  using Kolmogorov_quotient_in_open openin_subset by fastforce
+
+
+lemma open_map_Kolmogorov_quotient_gen:
+   "open_map (subtopology X S) (subtopology X (image (Kolmogorov_quotient X) S)) (Kolmogorov_quotient X)"
+proof (clarsimp simp: open_map_def openin_subtopology_alt image_iff)
+  fix U
+  assume "openin X U"
+  then have "Kolmogorov_quotient X ` (S \<inter> U) = Kolmogorov_quotient X ` S \<inter> U"
+    using Kolmogorov_quotient_in_open [of X U] by auto
+  then show "\<exists>V. openin X V \<and> Kolmogorov_quotient X ` (S \<inter> U) = Kolmogorov_quotient X ` S \<inter> V"
+    using \<open>openin X U\<close> by blast
+qed
+
+lemma open_map_Kolmogorov_quotient:
+   "open_map X (subtopology X (Kolmogorov_quotient X ` topspace X))
+     (Kolmogorov_quotient X)"
+  by (metis open_map_Kolmogorov_quotient_gen subtopology_topspace)
+
+lemma closed_map_Kolmogorov_quotient_explicit:
+   "closedin X U \<Longrightarrow> Kolmogorov_quotient X ` U = Kolmogorov_quotient X ` topspace X \<inter> U"
+  using closedin_subset by (fastforce simp: Kolmogorov_quotient_in_closed)
+
+lemma closed_map_Kolmogorov_quotient_gen:
+   "closed_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S))
+     (Kolmogorov_quotient X)"
+  using Kolmogorov_quotient_in_closed by (force simp: closed_map_def closedin_subtopology_alt image_iff)
+
+lemma closed_map_Kolmogorov_quotient:
+   "closed_map X (subtopology X (Kolmogorov_quotient X ` topspace X))
+     (Kolmogorov_quotient X)"
+  by (metis closed_map_Kolmogorov_quotient_gen subtopology_topspace)
+
+lemma quotient_map_Kolmogorov_quotient_gen:
+  "quotient_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
+proof (intro continuous_open_imp_quotient_map)
+  show "continuous_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
+    by (simp add: continuous_map_Kolmogorov_quotient continuous_map_from_subtopology continuous_map_in_subtopology image_mono)
+  show "open_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
+    using open_map_Kolmogorov_quotient_gen by blast
+  show "Kolmogorov_quotient X ` topspace (subtopology X S) = topspace (subtopology X (Kolmogorov_quotient X ` S))"
+    by (force simp: Kolmogorov_quotient_in_open)
+qed
+
+lemma quotient_map_Kolmogorov_quotient:
+   "quotient_map X (subtopology X (Kolmogorov_quotient X ` topspace X)) (Kolmogorov_quotient X)"
+  by (metis quotient_map_Kolmogorov_quotient_gen subtopology_topspace)
+
+lemma Kolmogorov_quotient_eq:
+   "Kolmogorov_quotient X x = Kolmogorov_quotient X y \<longleftrightarrow>
+    (\<forall>U. openin X U \<longrightarrow> (x \<in> U \<longleftrightarrow> y \<in> U))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis Kolmogorov_quotient_in_open)
+next
+  assume ?rhs then show ?lhs
+    by (simp add: Kolmogorov_quotient_def)
+qed
+
+lemma Kolmogorov_quotient_eq_alt:
+   "Kolmogorov_quotient X x = Kolmogorov_quotient X y \<longleftrightarrow>
+    (\<forall>U. closedin X U \<longrightarrow> (x \<in> U \<longleftrightarrow> y \<in> U))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis Kolmogorov_quotient_in_closed)
+next
+  assume ?rhs then show ?lhs
+    by (smt (verit) Diff_iff Kolmogorov_quotient_eq closedin_topspace in_mono openin_closedin_eq)
+qed
+
+lemma Kolmogorov_quotient_continuous_map:
+  assumes "continuous_map X Y f" "t0_space Y" and x: "x \<in> topspace X"
+  shows "f (Kolmogorov_quotient X x) = f x"
+  using assms unfolding continuous_map_def t0_space_def
+  by (smt (verit, ccfv_SIG) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace x mem_Collect_eq)
+
+lemma t0_space_Kolmogorov_quotient:
+  "t0_space (subtopology X (Kolmogorov_quotient X ` topspace X))"
+  apply (clarsimp simp: t0_space_def )
+  by (smt (verit, best) Kolmogorov_quotient_eq imageE image_eqI open_map_Kolmogorov_quotient open_map_def)
+
+lemma Kolmogorov_quotient_id:
+   "t0_space X \<Longrightarrow> x \<in> topspace X \<Longrightarrow> Kolmogorov_quotient X x = x"
+  by (metis Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace t0_space_def)
+
+lemma Kolmogorov_quotient_idemp:
+   "Kolmogorov_quotient X (Kolmogorov_quotient X x) = Kolmogorov_quotient X x"
+  by (simp add: Kolmogorov_quotient_eq Kolmogorov_quotient_in_open)
+
+lemma retraction_maps_Kolmogorov_quotient:
+   "retraction_maps X
+     (subtopology X (Kolmogorov_quotient X ` topspace X))
+     (Kolmogorov_quotient X) id"
+  unfolding retraction_maps_def continuous_map_in_subtopology
+  using Kolmogorov_quotient_idemp continuous_map_Kolmogorov_quotient by force
+
+lemma retraction_map_Kolmogorov_quotient:
+   "retraction_map X
+     (subtopology X (Kolmogorov_quotient X ` topspace X))
+     (Kolmogorov_quotient X)"
+  using retraction_map_def retraction_maps_Kolmogorov_quotient by blast
+
+lemma retract_of_space_Kolmogorov_quotient_image:
+   "Kolmogorov_quotient X ` topspace X retract_of_space X"
+proof -
+  have "continuous_map X X (Kolmogorov_quotient X)"
+    by (simp add: continuous_map_Kolmogorov_quotient)
+  then have "Kolmogorov_quotient X ` topspace X \<subseteq> topspace X"
+    by (simp add: continuous_map_image_subset_topspace)
+  then show ?thesis
+    by (meson retract_of_space_retraction_maps retraction_maps_Kolmogorov_quotient)
+qed
+
+lemma Kolmogorov_quotient_lift_exists:
+  assumes "S \<subseteq> topspace X" "t0_space Y" and f: "continuous_map (subtopology X S) Y f"
+  obtains g where "continuous_map (subtopology X (image (Kolmogorov_quotient X) S)) Y g"
+              "\<And>x. x \<in> S \<Longrightarrow> g(Kolmogorov_quotient X x) = f x"
+proof -
+  have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S; Kolmogorov_quotient X x = Kolmogorov_quotient X y\<rbrakk>
+            \<Longrightarrow> f x = f y"
+    using assms
+    apply (simp add: Kolmogorov_quotient_eq t0_space_def continuous_map_def Int_absorb1 openin_subtopology)
+    by (smt (verit, del_insts) Int_iff mem_Collect_eq)
+  then obtain g where g: "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
+    "g ` (topspace X \<inter> Kolmogorov_quotient X ` S) = f ` S"
+    "\<And>x. x \<in> S \<Longrightarrow> g (Kolmogorov_quotient X x) = f x"
+    using quotient_map_lift_exists [OF quotient_map_Kolmogorov_quotient_gen [of X S] f]
+    by (metis assms(1) topspace_subtopology topspace_subtopology_subset) 
+  show ?thesis
+    proof qed (use g in auto)
+qed
+
+subsection\<open>Closed diagonals and graphs\<close>
+
+lemma Hausdorff_space_closedin_diagonal:
+  "Hausdorff_space X \<longleftrightarrow>
+        closedin (prod_topology X X) ((\<lambda>x. (x,x)) ` topspace X)"
+proof -
+  have \<section>: "((\<lambda>x. (x, x)) ` topspace X) \<subseteq> topspace X \<times> topspace X"
+    by auto
+  show ?thesis
+    apply (simp add: closedin_def openin_prod_topology_alt Hausdorff_space_def disjnt_iff \<section>)
+    apply (intro all_cong1 imp_cong ex_cong1 conj_cong refl)
+    by (force dest!: openin_subset)+
+qed
+
+lemma closed_map_diag_eq:
+   "closed_map X (prod_topology X X) (\<lambda>x. (x,x)) \<longleftrightarrow> Hausdorff_space X"
+proof -
+  have "section_map X (prod_topology X X) (\<lambda>x. (x, x))"
+    unfolding section_map_def retraction_maps_def
+    by (smt (verit) continuous_map_fst continuous_map_of_fst continuous_map_on_empty continuous_map_pairwise fst_conv fst_diag_fst snd_diag_fst)
+  then have "embedding_map X (prod_topology X X) (\<lambda>x. (x, x))"
+    by (rule section_imp_embedding_map)
+  then show ?thesis
+    using Hausdorff_space_closedin_diagonal embedding_imp_closed_map_eq by blast
+qed
+
+lemma closedin_continuous_maps_eq:
+  assumes "Hausdorff_space Y" and f: "continuous_map X Y f" and g: "continuous_map X Y g"
+  shows "closedin X {x \<in> topspace X. f x = g x}"
+proof -
+  have \<section>:"{x \<in> topspace X. f x = g x} = {x \<in> topspace X. (f x,g x) \<in> ((\<lambda>y.(y,y)) ` topspace Y)}"
+    using f continuous_map_image_subset_topspace by fastforce
+  show ?thesis
+    unfolding \<section>
+  proof (intro closedin_continuous_map_preimage)
+    show "continuous_map X (prod_topology Y Y) (\<lambda>x. (f x, g x))"
+      by (simp add: continuous_map_pairedI f g)
+    show "closedin (prod_topology Y Y) ((\<lambda>y. (y, y)) ` topspace Y)"
+      using Hausdorff_space_closedin_diagonal assms by blast
+  qed
+qed
+
+lemma retract_of_space_imp_closedin:
+  assumes "Hausdorff_space X" and S: "S retract_of_space X"
+  shows "closedin X S"
+proof -
+  obtain r where r: "continuous_map X (subtopology X S) r" "\<forall>x\<in>S. r x = x"
+    using assms by (meson retract_of_space_def)
+  then have \<section>: "S = {x \<in> topspace X. r x = x}"
+    using S retract_of_space_imp_subset by (force simp: continuous_map_def)
+  show ?thesis
+    unfolding \<section> 
+    using r continuous_map_into_fulltopology assms
+    by (force intro: closedin_continuous_maps_eq)
+qed
+
+lemma homeomorphic_maps_graph:
+   "homeomorphic_maps X (subtopology (prod_topology X Y) ((\<lambda>x. (x, f x)) ` (topspace X)))
+         (\<lambda>x. (x, f x)) fst  \<longleftrightarrow>  continuous_map X Y f" 
+   (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then 
+  have h: "homeomorphic_map X (subtopology (prod_topology X Y) ((\<lambda>x. (x, f x)) ` topspace X)) (\<lambda>x. (x, f x))"
+    by (auto simp: homeomorphic_maps_map)
+  have "f = snd \<circ> (\<lambda>x. (x, f x))"
+    by force
+  then show ?rhs
+    by (metis (no_types, lifting) h continuous_map_in_subtopology continuous_map_snd_of homeomorphic_eq_everything_map)
+next
+  assume ?rhs
+  then show ?lhs
+    unfolding homeomorphic_maps_def
+    by (smt (verit, ccfv_threshold) continuous_map_eq continuous_map_subtopology_fst embedding_map_def embedding_map_graph homeomorphic_eq_everything_map  image_cong image_iff prod.collapse prod.inject)
+qed
+
+
+subsection \<open> KC spaces, those where all compact sets are closed.\<close>
+
+definition kc_space 
+  where "kc_space X \<equiv> \<forall>S. compactin X S \<longrightarrow> closedin X S"
+
+lemma kc_space_expansive:
+   "\<lbrakk>kc_space X; topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk>
+      \<Longrightarrow> kc_space Y"
+  by (meson compactin_contractive kc_space_def topology_finer_closedin)
+
+lemma compactin_imp_closedin_gen:
+   "\<lbrakk>kc_space X; compactin X S\<rbrakk> \<Longrightarrow> closedin X S"
+  using kc_space_def by blast
+
+lemma Hausdorff_imp_kc_space: "Hausdorff_space X \<Longrightarrow> kc_space X"
+  by (simp add: compactin_imp_closedin kc_space_def)
+
+lemma kc_imp_t1_space: "kc_space X \<Longrightarrow> t1_space X"
+  by (simp add: finite_imp_compactin kc_space_def t1_space_closedin_finite)
+
+lemma kc_space_subtopology:
+   "kc_space X \<Longrightarrow> kc_space(subtopology X S)"
+  by (metis closedin_Int_closure_of closure_of_eq compactin_subtopology inf.absorb2 kc_space_def)
+
+lemma kc_space_discrete_topology:
+   "kc_space(discrete_topology U)"
+  using Hausdorff_space_discrete_topology compactin_imp_closedin kc_space_def by blast
+
+lemma kc_space_continuous_injective_map_preimage:
+  assumes "kc_space Y" "continuous_map X Y f" and injf: "inj_on f (topspace X)"
+  shows "kc_space X"
+  unfolding kc_space_def
+proof (intro strip)
+  fix S
+  assume S: "compactin X S"
+  have "S = {x \<in> topspace X. f x \<in> f ` S}"
+    using S compactin_subset_topspace inj_onD [OF injf] by blast
+  with assms S show "closedin X S"
+    by (metis (no_types, lifting) Collect_cong closedin_continuous_map_preimage compactin_imp_closedin_gen image_compactin)
+qed
+
+lemma kc_space_retraction_map_image:
+  assumes "retraction_map X Y r" "kc_space X"
+  shows "kc_space Y"
+proof -
+  obtain s where s: "continuous_map X Y r" "continuous_map Y X s" "\<And>x. x \<in> topspace Y \<Longrightarrow> r (s x) = x"
+    using assms by (force simp: retraction_map_def retraction_maps_def)
+  then have inj: "inj_on s (topspace Y)"
+    by (metis inj_on_def)
+  show ?thesis
+    unfolding kc_space_def
+  proof (intro strip)
+    fix S
+    assume S: "compactin Y S"
+    have "S = {x \<in> topspace Y. s x \<in> s ` S}"
+      using S compactin_subset_topspace inj_onD [OF inj] by blast
+    with assms S show "closedin Y S"
+      by (meson compactin_imp_closedin_gen inj kc_space_continuous_injective_map_preimage s(2))
+  qed
+qed
+
+lemma homeomorphic_kc_space:
+   "X homeomorphic_space Y \<Longrightarrow> kc_space X \<longleftrightarrow> kc_space Y"
+  by (meson homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym kc_space_continuous_injective_map_preimage)
+
+lemma compact_kc_eq_maximal_compact_space:
+  assumes "compact_space X"
+  shows "kc_space X \<longleftrightarrow>
+         (\<forall>Y. topspace Y = topspace X \<and> (\<forall>S. openin X S \<longrightarrow> openin Y S) \<and> compact_space Y \<longrightarrow> Y = X)" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (metis closedin_compact_space compactin_contractive kc_space_def topology_eq topology_finer_closedin)    
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding kc_space_def
+  proof (intro strip)
+    fix S
+    assume S: "compactin X S"
+    define Y where 
+      "Y \<equiv> topology (arbitrary union_of (finite intersection_of (\<lambda>A. A = topspace X - S \<or> openin X A)
+                           relative_to (topspace X)))"
+    have "topspace Y = topspace X"
+      by (auto simp: Y_def)
+    have "openin X T \<longrightarrow> openin Y T" for T
+      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset)
+    have "compact_space Y"
+    proof (rule Alexander_subbase_alt)
+      show "\<exists>\<F>'. finite \<F>' \<and> \<F>' \<subseteq> \<C> \<and> topspace X \<subseteq> \<Union> \<F>'" 
+        if \<C>: "\<C> \<subseteq> insert (topspace X - S) (Collect (openin X))" and sub: "topspace X \<subseteq> \<Union>\<C>" for \<C>
+      proof -
+        consider "\<C> \<subseteq> Collect (openin X)" | \<V> where "\<C> = insert (topspace X - S) \<V>" "\<V> \<subseteq> Collect (openin X)"
+          using \<C> by (metis insert_Diff subset_insert_iff)
+        then show ?thesis
+        proof cases
+          case 1
+          then show ?thesis
+            by (metis assms compact_space_alt mem_Collect_eq subsetD that(2))
+        next
+          case 2
+          then have "S \<subseteq> \<Union>\<V>"
+            using S sub compactin_subset_topspace by blast
+          with 2 obtain \<F> where "finite \<F> \<and> \<F> \<subseteq> \<V> \<and> S \<subseteq> \<Union>\<F>"
+            using S unfolding compactin_def by (metis Ball_Collect)
+          with 2 show ?thesis
+            by (rule_tac x="insert (topspace X - S) \<F>" in exI) blast
+        qed
+      qed
+    qed (auto simp: Y_def)
+    have "Y = X"
+      using R \<open>\<And>S. openin X S \<longrightarrow> openin Y S\<close> \<open>compact_space Y\<close> \<open>topspace Y = topspace X\<close> by blast
+    moreover have "openin Y (topspace X - S)"
+      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset)
+    ultimately show "closedin X S"
+      unfolding closedin_def using S compactin_subset_topspace by blast
+  qed
+qed
+
+lemma continuous_imp_closed_map_gen:
+   "\<lbrakk>compact_space X; kc_space Y; continuous_map X Y f\<rbrakk> \<Longrightarrow> closed_map X Y f"
+  by (meson closed_map_def closedin_compact_space compactin_imp_closedin_gen image_compactin)
+
+lemma kc_space_compact_subtopologies:
+  "kc_space X \<longleftrightarrow> (\<forall>K. compactin X K \<longrightarrow> kc_space(subtopology X K))" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (auto simp: kc_space_def closedin_closed_subtopology compactin_subtopology)
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding kc_space_def
+  proof (intro strip)
+    fix K
+    assume K: "compactin X K"
+    then have "K \<subseteq> topspace X"
+      by (simp add: compactin_subset_topspace)
+    moreover have "X closure_of K \<subseteq> K"
+    proof
+      fix x
+      assume x: "x \<in> X closure_of K"
+      have "kc_space (subtopology X K)"
+        by (simp add: R \<open>compactin X K\<close>)
+      have "compactin X (insert x K)"
+        by (metis K x compactin_Un compactin_sing in_closure_of insert_is_Un)
+      then show "x \<in> K"
+        by (metis R x K Int_insert_left_if1 closedin_Int_closure_of compact_imp_compactin_subtopology 
+            insertCI kc_space_def subset_insertI)
+    qed
+    ultimately show "closedin X K"
+      using closure_of_subset_eq by blast
+  qed
+qed
+
+lemma kc_space_compact_prod_topology:
+  assumes "compact_space X"
+  shows "kc_space(prod_topology X X) \<longleftrightarrow> Hausdorff_space X" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs
+  show ?rhs
+    unfolding closed_map_diag_eq [symmetric]
+  proof (intro continuous_imp_closed_map_gen)
+    show "continuous_map X (prod_topology X X) (\<lambda>x. (x, x))"
+      by (intro continuous_intros)
+  qed (use L assms in auto)
+next
+  assume ?rhs then show ?lhs
+    by (simp add: Hausdorff_imp_kc_space Hausdorff_space_prod_topology)
+qed
+
+lemma kc_space_prod_topology:
+   "kc_space(prod_topology X X) \<longleftrightarrow> (\<forall>K. compactin X K \<longrightarrow> Hausdorff_space(subtopology X K))" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (metis compactin_subspace kc_space_compact_prod_topology kc_space_subtopology subtopology_Times)
+next
+  assume R: ?rhs  
+  have "kc_space (subtopology (prod_topology X X) L)" if "compactin (prod_topology X X) L" for L 
+  proof -
+    define K where "K \<equiv> fst ` L \<union> snd ` L"
+    have "L \<subseteq> K \<times> K"
+      by (force simp: K_def)
+    have "compactin X K"
+      by (metis K_def compactin_Un continuous_map_fst continuous_map_snd image_compactin that)
+    then have "Hausdorff_space (subtopology X K)"
+      by (simp add: R)
+    then have "kc_space (prod_topology (subtopology X K) (subtopology X K))"
+      by (simp add: \<open>compactin X K\<close> compact_space_subtopology kc_space_compact_prod_topology)
+    then have "kc_space (subtopology (prod_topology (subtopology X K) (subtopology X K)) L)"
+      using kc_space_subtopology by blast
+    then show ?thesis
+      using \<open>L \<subseteq> K \<times> K\<close> subtopology_Times subtopology_subtopology
+      by (metis (no_types, lifting) Sigma_cong inf.absorb_iff2)
+  qed
+  then show ?lhs
+    using kc_space_compact_subtopologies by blast
+qed
+
+lemma kc_space_prod_topology_alt:
+   "kc_space(prod_topology X X) \<longleftrightarrow>
+        kc_space X \<and>
+        (\<forall>K. compactin X K \<longrightarrow> Hausdorff_space(subtopology X K))"
+  using Hausdorff_imp_kc_space kc_space_compact_subtopologies kc_space_prod_topology by blast
+
+proposition kc_space_prod_topology_left:
+  assumes X: "kc_space X" and Y: "Hausdorff_space Y"
+  shows "kc_space (prod_topology X Y)"
+  unfolding kc_space_def
+proof (intro strip)
+  fix K
+  assume K: "compactin (prod_topology X Y) K"
+  then have "K \<subseteq> topspace X \<times> topspace Y"
+    using compactin_subset_topspace topspace_prod_topology by blast
+  moreover have "\<exists>T. openin (prod_topology X Y) T \<and> (a,b) \<in> T \<and> T \<subseteq> (topspace X \<times> topspace Y) - K"
+    if ab: "(a,b) \<in> (topspace X \<times> topspace Y) - K" for a b
+  proof - 
+    have "compactin Y {b}"
+      using that by force
+    moreover 
+    have "compactin Y {y \<in> topspace Y. (a,y) \<in> K}"
+    proof -
+      have "compactin (prod_topology X Y) (K \<inter> {a} \<times> topspace Y)"
+        using that compact_Int_closedin [OF K]
+        by (simp add: X closedin_prod_Times_iff compactin_imp_closedin_gen)
+      moreover have "subtopology (prod_topology X Y) (K \<inter> {a} \<times> topspace Y)  homeomorphic_space 
+                     subtopology Y {y \<in> topspace Y. (a, y) \<in> K}"
+        unfolding homeomorphic_space_def homeomorphic_maps_def
+        using that
+        apply (rule_tac x="snd" in exI)
+        apply (rule_tac x="Pair a" in exI)
+        by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology continuous_map_subtopology_snd continuous_map_paired)
+      ultimately show ?thesis
+        by (simp add: compactin_subspace homeomorphic_compact_space) 
+    qed
+    moreover have "disjnt {b} {y \<in> topspace Y. (a,y) \<in> K}"
+      using ab by force
+    ultimately obtain V U where VU: "openin Y V" "openin Y U" "{b} \<subseteq> V" "{y \<in> topspace Y. (a,y) \<in> K} \<subseteq> U" "disjnt V U"
+      using Hausdorff_space_compact_separation [OF Y] by blast
+    define V' where "V' \<equiv> topspace Y - U"
+    have W: "closedin Y V'" "{y \<in> topspace Y. (a,y) \<in> K} \<subseteq> topspace Y - V'" "disjnt V (topspace Y - V')"
+      using VU by (auto simp: V'_def disjnt_iff)
+    with VU obtain "V \<subseteq> topspace Y" "V' \<subseteq> topspace Y"
+      by (meson closedin_subset openin_closedin_eq)
+    then obtain "b \<in> V" "disjnt {y \<in> topspace Y. (a,y) \<in> K} V'" "V \<subseteq> V'"
+      using VU unfolding disjnt_iff V'_def by force
+    define C where "C \<equiv> image fst (K \<inter> {z \<in> topspace(prod_topology X Y). snd z \<in> V'})"
+    have "closedin (prod_topology X Y) {z \<in> topspace (prod_topology X Y). snd z \<in> V'}"
+        using closedin_continuous_map_preimage \<open>closedin Y V'\<close> continuous_map_snd by blast
+    then have "compactin X C"
+      unfolding C_def by (meson K compact_Int_closedin continuous_map_fst image_compactin)
+    then have "closedin X C"
+      using assms by (auto simp: kc_space_def)
+    show ?thesis
+      apply (rule_tac x="(topspace X - C) \<times> V" in exI)
+      using VU
+      apply (auto simp:  )
+          apply (metis VU(1) \<open>closedin X C\<close> closedin_def openin_prod_Times_iff)
+      using that apply blast
+        apply (auto simp: C_def image_iff Ball_def)
+      using V'_def VU(4) apply auto[1]
+       apply (simp add: \<open>b \<in> V\<close>)
+      using \<open>V \<subseteq> topspace Y\<close> apply blast
+      using \<open>V \<subseteq> V'\<close> \<open>V \<subseteq> topspace Y\<close> by blast
+  qed
+  ultimately show "closedin (prod_topology X Y) K"
+    by (metis surj_pair closedin_def openin_subopen topspace_prod_topology)
+qed
+
+lemma kc_space_prod_topology_right:
+   "\<lbrakk>Hausdorff_space X; kc_space Y\<rbrakk> \<Longrightarrow> kc_space (prod_topology X Y)"
+  using kc_space_prod_topology_left homeomorphic_kc_space homeomorphic_space_prod_topology_swap by blast
+
+
+subsection \<open>Regular spaces\<close>
+
+text \<open>Regular spaces. These are *not* a priori assumed to be Hausdorff/T_1\<close>
+
+
+definition regular_space 
+  where "regular_space X \<equiv>
+        \<forall>C a. closedin X C \<and> a \<in> topspace X - C
+                \<longrightarrow> (\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V)"
+
+lemma homeomorphic_regular_space_aux:
+  assumes hom: "X homeomorphic_space Y" and X: "regular_space X"
+  shows "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 regular_space_def
+  proof clarify
+    fix C a
+    assume Y: "closedin Y C" "a \<in> topspace Y" and "a \<notin> C"
+    then obtain "closedin X (g ` C)" "g a \<in> topspace X" "g a \<notin> g ` C"
+      using \<open>closedin Y C\<close> hmg homeomorphic_map_closedness_eq
+      by (smt (verit, ccfv_SIG) fg homeomorphic_imp_surjective_map image_iff in_mono) 
+    then obtain S T where ST: "openin X S" "openin X T" "g a \<in> S" "g`C \<subseteq> T" "disjnt S T"
+      using X unfolding regular_space_def by (metis DiffI)
+    then have "openin Y (f`S)" "openin Y (f`T)"
+      by (meson hmf homeomorphic_map_openness_eq)+
+    moreover have "a \<in> f`S \<and> C \<subseteq> f`T"
+      using ST by (smt (verit, best) Y closedin_subset fg image_eqI subset_iff)   
+    moreover have "disjnt (f`S) (f`T)"
+      using ST by (smt (verit, ccfv_SIG) disjnt_iff fg image_iff openin_subset subsetD)
+    ultimately show "\<exists>U V. openin Y U \<and> openin Y V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
+      by metis
+  qed
+qed
+
+lemma homeomorphic_regular_space:
+   "X homeomorphic_space Y
+        \<Longrightarrow> (regular_space X \<longleftrightarrow> regular_space Y)"
+  by (meson homeomorphic_regular_space_aux homeomorphic_space_sym)
+
+lemma regular_space:
+   "regular_space X \<longleftrightarrow>
+        (\<forall>C a. closedin X C \<and> a \<in> topspace X - C
+              \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> disjnt C (X closure_of U)))"
+  unfolding regular_space_def
+proof (intro all_cong1 imp_cong refl ex_cong1)
+  fix C a U
+  assume C: "closedin X C \<and> a \<in> topspace X - C"
+  show "(\<exists>V. openin X U \<and> openin X V \<and> a \<in> U \<and> C \<subseteq> V \<and> disjnt U V)  
+    \<longleftrightarrow> (openin X U \<and> a \<in> U \<and> disjnt C (X closure_of U))" (is "?lhs=?rhs")
+  proof
+    assume ?lhs
+    then show ?rhs
+      by (smt (verit, best) disjnt_iff in_closure_of subsetD)
+  next
+    assume R: ?rhs
+    then have "disjnt U (topspace X - X closure_of U)"
+      by (meson DiffD2 closure_of_subset disjnt_iff openin_subset subsetD)
+    moreover have "C \<subseteq> topspace X - X closure_of U"
+      by (meson C DiffI R closedin_subset disjnt_iff subset_eq)
+    ultimately show ?lhs
+      using R by (rule_tac x="topspace X - X closure_of U" in exI) auto
+    qed
+qed
+
+lemma neighbourhood_base_of_closedin:
+  "neighbourhood_base_of (closedin X) X \<longleftrightarrow> regular_space X" (is "?lhs=?rhs")
+proof -
+  have "?lhs \<longleftrightarrow> (\<forall>W x. openin X W \<and> x \<in> W \<longrightarrow>
+                  (\<exists>U. openin X U \<and> (\<exists>V. closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)))"
+    by (simp add: neighbourhood_base_of)
+  also have "\<dots> \<longleftrightarrow> (\<forall>W x. closedin X W \<and> x \<in> topspace X - W \<longrightarrow>
+                     (\<exists>U. openin X U \<and> (\<exists>V. closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> topspace X - W)))"
+    by (smt (verit) Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
+  also have "\<dots> \<longleftrightarrow> ?rhs"
+  proof -
+    have \<section>: "(\<exists>V. closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> topspace X - W) 
+         \<longleftrightarrow> (\<exists>V. openin X V \<and> x \<in> U \<and> W \<subseteq> V \<and> disjnt U V)" (is "?lhs=?rhs")
+      if "openin X U"  "closedin X W" "x \<in> topspace X" "x \<notin> W" for W U x
+    proof
+      assume ?lhs with \<open>closedin X W\<close> show ?rhs
+        unfolding closedin_def by (smt (verit) Diff_mono disjnt_Diff1 double_diff subset_eq)
+    next
+      assume ?rhs with \<open>openin X U\<close> show ?lhs
+        unfolding openin_closedin_eq disjnt_def
+        by (smt (verit) Diff_Diff_Int Diff_disjoint Diff_eq_empty_iff Int_Diff inf.orderE)
+    qed
+    show ?thesis
+      unfolding regular_space_def
+      by (intro all_cong1 ex_cong1 imp_cong refl) (metis \<section> DiffE)
+  qed
+  finally show ?thesis .
+qed
+
+lemma regular_space_discrete_topology:
+   "regular_space (discrete_topology S)"
+  using neighbourhood_base_of_closedin neighbourhood_base_of_discrete_topology by fastforce
+
+lemma regular_space_subtopology:
+ "regular_space X \<Longrightarrow> regular_space (subtopology X S)"
+  unfolding regular_space_def openin_subtopology_alt closedin_subtopology_alt disjnt_iff
+  by clarsimp (smt (verit, best) inf.orderE inf_le1 le_inf_iff)
+
+
+lemma regular_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; regular_space X\<rbrakk> \<Longrightarrow> regular_space Y"
+  using hereditary_imp_retractive_property homeomorphic_regular_space regular_space_subtopology by blast
+
+lemma regular_t0_imp_Hausdorff_space:
+   "\<lbrakk>regular_space X; t0_space X\<rbrakk> \<Longrightarrow> Hausdorff_space X"
+  apply (clarsimp simp: regular_space_def t0_space Hausdorff_space_def)
+  by (metis disjnt_sym subsetD)
+
+lemma regular_t0_eq_Hausdorff_space:
+   "regular_space X \<Longrightarrow> (t0_space X \<longleftrightarrow> Hausdorff_space X)"
+  using Hausdorff_imp_t0_space regular_t0_imp_Hausdorff_space by blast
+
+lemma regular_t1_imp_Hausdorff_space:
+   "\<lbrakk>regular_space X; t1_space X\<rbrakk> \<Longrightarrow> Hausdorff_space X"
+  by (simp add: regular_t0_imp_Hausdorff_space t1_imp_t0_space)
+
+lemma regular_t1_eq_Hausdorff_space:
+   "regular_space X \<Longrightarrow> t1_space X \<longleftrightarrow> Hausdorff_space X"
+  using regular_t0_imp_Hausdorff_space t1_imp_t0_space t1_or_Hausdorff_space by blast
+
+lemma compact_Hausdorff_imp_regular_space:
+  assumes "compact_space X" "Hausdorff_space X"
+  shows "regular_space X"
+  unfolding regular_space_def
+proof clarify
+  fix S a
+  assume "closedin X S" and "a \<in> topspace X" and "a \<notin> S"
+  then show "\<exists>U V. openin X U \<and> openin X V \<and> a \<in> U \<and> S \<subseteq> V \<and> disjnt U V"
+    using assms unfolding Hausdorff_space_compact_sets
+    by (metis closedin_compact_space compactin_sing disjnt_empty1 insert_subset disjnt_insert1)
+qed
+
+lemma regular_space_topspace_empty: "topspace X = {} \<Longrightarrow> regular_space X"
+  by (simp add: Hausdorff_space_topspace_empty compact_Hausdorff_imp_regular_space compact_space_topspace_empty)
+
+lemma neighbourhood_base_of_closed_Hausdorff_space:
+   "regular_space X \<and> Hausdorff_space X \<longleftrightarrow>
+    neighbourhood_base_of (\<lambda>C. closedin X C \<and> Hausdorff_space(subtopology X C)) X" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: Hausdorff_space_subtopology neighbourhood_base_of_closedin)
+next
+  assume ?rhs then show ?lhs
+  by (metis (mono_tags, lifting) Hausdorff_space_closed_neighbourhood neighbourhood_base_of neighbourhood_base_of_closedin openin_topspace)
+qed
+
+lemma locally_compact_imp_kc_eq_Hausdorff_space:
+   "neighbourhood_base_of (compactin X) X \<Longrightarrow> kc_space X \<longleftrightarrow> Hausdorff_space X"
+  by (metis Hausdorff_imp_kc_space kc_imp_t1_space kc_space_def neighbourhood_base_of_closedin neighbourhood_base_of_mono regular_t1_imp_Hausdorff_space)
+
+lemma regular_space_compact_closed_separation:
+  assumes X: "regular_space X"
+      and S: "compactin X S"
+      and T: "closedin X T"
+      and "disjnt S T"
+    shows "\<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={}")
+  case True
+  then show ?thesis
+    by (meson T closedin_def disjnt_empty1 empty_subsetI openin_empty openin_topspace)
+next
+  case False
+  then have "\<exists>U V. x \<in> S \<longrightarrow> openin X U \<and> openin X V \<and> x \<in> U \<and> T \<subseteq> V \<and> disjnt U V" for x
+    using assms unfolding regular_space_def
+    by (smt (verit) Diff_iff compactin_subset_topspace disjnt_iff subsetD)
+  then obtain U V where UV: "\<And>x. x \<in> S \<Longrightarrow> openin X (U x) \<and> openin X (V x) \<and> x \<in> (U x) \<and> T \<subseteq> (V x) \<and> disjnt (U x) (V x)" 
+    by metis
+  then obtain \<F> where "finite \<F>" "\<F> \<subseteq> U ` S" "S \<subseteq> \<Union> \<F>"
+    using S unfolding compactin_def by (smt (verit) UN_iff image_iff subsetI)
+  then obtain K where "finite K" "K \<subseteq> S" and K: "S \<subseteq> \<Union>(U ` K)"
+    by (metis finite_subset_image)
+  show ?thesis 
+  proof (intro exI conjI)
+    show "openin X (\<Union>(U ` K))"
+      using \<open>K \<subseteq> S\<close> UV by blast
+    show "openin X (\<Inter>(V ` K))"
+      using False K UV \<open>K \<subseteq> S\<close> \<open>finite K\<close> by blast
+    show "S \<subseteq> \<Union>(U ` K)"
+      by (simp add: K)
+    show "T \<subseteq> \<Inter>(V ` K)"
+      using UV \<open>K \<subseteq> S\<close> by blast
+    show "disjnt (\<Union>(U ` K)) (\<Inter>(V ` K))"
+      by (smt (verit) Inter_iff UN_E UV \<open>K \<subseteq> S\<close> disjnt_iff image_eqI subset_iff)
+  qed
+qed
+
+lemma regular_space_compact_closed_sets:
+   "regular_space X \<longleftrightarrow>
+        (\<forall>S T. compactin X S \<and> closedin X T \<and> disjnt 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))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using regular_space_compact_closed_separation by fastforce
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding regular_space
+  proof clarify
+    fix S x
+    assume "closedin X S" and "x \<in> topspace X" and "x \<notin> S"
+    then obtain U V where "openin X U \<and> openin X V \<and> {x} \<subseteq> U \<and> S \<subseteq> V \<and> disjnt U V"
+      by (metis R compactin_sing disjnt_empty1 disjnt_insert1)
+    then show "\<exists>U. openin X U \<and> x \<in> U \<and> disjnt S (X closure_of U)"
+      by (smt (verit, best) disjnt_iff in_closure_of insert_subset subsetD)
+  qed
+qed
+
+
+lemma regular_space_prod_topology:
+   "regular_space (prod_topology X Y) \<longleftrightarrow>
+        topspace X = {} \<or> topspace Y = {} \<or> regular_space X \<and> regular_space Y" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (metis regular_space_retraction_map_image retraction_map_fst retraction_map_snd)
+next
+  assume R: ?rhs  
+  show ?lhs
+  proof (cases "topspace X = {} \<or> topspace Y = {}")
+    case True
+    then show ?thesis
+      by (simp add: regular_space_topspace_empty)
+  next
+    case False
+    then have "regular_space X" "regular_space Y"
+      using R by auto
+    show ?thesis
+      unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of
+    proof clarify
+      fix W x y
+      assume W: "openin (prod_topology X Y) W" and "(x,y) \<in> W"
+      then obtain U V where U: "openin X U" "x \<in> U" and V: "openin Y V" "y \<in> V" 
+        and "U \<times> V \<subseteq> W"
+        by (metis openin_prod_topology_alt)
+      obtain D1 C1 where 1: "openin X D1" "closedin X C1" "x \<in> D1" "D1 \<subseteq> C1" "C1 \<subseteq> U"
+        by (metis \<open>regular_space X\<close> U neighbourhood_base_of neighbourhood_base_of_closedin)
+      obtain D2 C2 where 2: "openin Y D2" "closedin Y C2" "y \<in> D2" "D2 \<subseteq> C2" "C2 \<subseteq> V"
+        by (metis \<open>regular_space Y\<close> V neighbourhood_base_of neighbourhood_base_of_closedin)
+      show "\<exists>U V. openin (prod_topology X Y) U \<and> closedin (prod_topology X Y) V \<and>
+                  (x,y) \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+      proof (intro conjI exI)
+        show "openin (prod_topology X Y) (D1 \<times> D2)"
+          by (simp add: 1 2 openin_prod_Times_iff)
+        show "closedin (prod_topology X Y) (C1 \<times> C2)"
+          by (simp add: 1 2 closedin_prod_Times_iff)
+      qed (use 1 2 \<open>U \<times> V \<subseteq> W\<close> in auto)
+    qed
+  qed
+qed
+
+lemma regular_space_product_topology:
+   "regular_space (product_topology X I) \<longleftrightarrow>
+    topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. regular_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (meson regular_space_retraction_map_image retraction_map_product_projection)
+next
+  assume R: ?rhs  
+  show ?lhs
+  proof (cases "topspace(product_topology X I) = {}")
+    case True
+    then show ?thesis
+      by (simp add: regular_space_topspace_empty)
+  next
+    case False
+    then obtain x where x: "x \<in> topspace (product_topology X I)"
+      by blast
+    define \<F> where "\<F> \<equiv> {Pi\<^sub>E I U |U. finite {i \<in> I. U i \<noteq> topspace (X i)}
+                        \<and> (\<forall>i\<in>I. openin (X i) (U i))}"
+    have oo: "openin (product_topology X I) = arbitrary union_of (\<lambda>W. W \<in> \<F>)"
+      by (simp add: \<F>_def openin_product_topology product_topology_base_alt)
+    have "\<exists>U V. openin (product_topology X I) U \<and> closedin (product_topology X I) V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> Pi\<^sub>E I W"
+      if fin: "finite {i \<in> I. W i \<noteq> topspace (X i)}" 
+        and opeW: "\<And>k. k \<in> I \<Longrightarrow> openin (X k) (W k)" and x: "x \<in> PiE I W" for W x
+    proof -
+      have "\<And>i. i \<in> I \<Longrightarrow> \<exists>U V. openin (X i) U \<and> closedin (X i) V \<and> x i \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W i"
+        by (metis False PiE_iff R neighbourhood_base_of neighbourhood_base_of_closedin opeW x)
+      then obtain U C where UC: 
+        "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> closedin (X i) (C i) \<and> x i \<in> U i \<and> U i \<subseteq> C i \<and> C i \<subseteq> W i"
+        by metis
+      define PI where "PI \<equiv> \<lambda>V. PiE I (\<lambda>i. if W i = topspace(X i) then topspace(X i) else V i)"
+      show ?thesis
+      proof (intro conjI exI)
+        have "\<forall>i\<in>I. W i \<noteq> topspace (X i) \<longrightarrow> openin (X i) (U i)"
+          using UC by force
+        with fin show "openin (product_topology X I) (PI U)"
+          by (simp add: Collect_mono_iff PI_def openin_PiE_gen rev_finite_subset)
+        show "closedin (product_topology X I) (PI C)"
+          by (simp add: UC closedin_product_topology PI_def)
+        show "x \<in> PI U"
+          using UC x by (fastforce simp: PI_def)
+        show "PI U \<subseteq> PI C"
+          by (smt (verit) UC Orderings.order_eq_iff PiE_mono PI_def)
+        show "PI C \<subseteq> Pi\<^sub>E I W"
+          by (simp add: UC PI_def subset_PiE)
+      qed
+    qed
+    then have "neighbourhood_base_of (closedin (product_topology X I)) (product_topology X I)"
+      unfolding neighbourhood_base_of_topology_base [OF oo] by (force simp: \<F>_def)
+    then show ?thesis
+      by (simp add: neighbourhood_base_of_closedin)
+  qed
+qed
+
+lemma closed_map_paired_gen_aux:
+  assumes "regular_space Y" and f: "closed_map Z X f" and g: "closed_map Z Y g"
+    and clo: "\<And>y. y \<in> topspace X \<Longrightarrow> closedin Z {x \<in> topspace Z. f x = y}"
+    and contg: "continuous_map Z Y g"
+  shows "closed_map Z (prod_topology X Y) (\<lambda>x. (f x, g x))"
+  unfolding closed_map_def
+proof (intro strip)
+  fix C assume "closedin Z C"
+  then have "C \<subseteq> topspace Z"
+    by (simp add: closedin_subset)
+  have "f ` topspace Z \<subseteq> topspace X" "g ` topspace Z \<subseteq> topspace Y"
+    by (simp_all add: assms closed_map_imp_subset_topspace)
+  show "closedin (prod_topology X Y) ((\<lambda>x. (f x, g x)) ` C)"
+    unfolding closedin_def topspace_prod_topology
+  proof (intro conjI)
+    have "closedin Y (g ` C)"
+      using \<open>closedin Z C\<close> assms(3) closed_map_def by blast
+    with assms show "(\<lambda>x. (f x, g x)) ` C \<subseteq> topspace X \<times> topspace Y"
+      using \<open>C \<subseteq> topspace Z\<close> \<open>f ` topspace Z \<subseteq> topspace X\<close> continuous_map_closedin subsetD by fastforce
+    have *: "\<exists>T. openin (prod_topology X Y) T \<and> (y1,y2) \<in> T \<and> T \<subseteq> topspace X \<times> topspace Y - (\<lambda>x. (f x, g x)) ` C"
+      if "(y1,y2) \<notin> (\<lambda>x. (f x, g x)) ` C" and y1: "y1 \<in> topspace X" and y2: "y2 \<in> topspace Y"
+      for y1 y2
+    proof -
+      define A where "A \<equiv> topspace Z - (C \<inter> {x \<in> topspace Z. f x = y1})"
+      have A: "openin Z A" "{x \<in> topspace Z. g x = y2} \<subseteq> A"
+        using that \<open>closedin Z C\<close> clo that(2) by (auto simp: A_def)
+      obtain V0 where "openin Y V0 \<and> y2 \<in> V0" and UA: "{x \<in> topspace Z. g x \<in> V0} \<subseteq> A"
+        using g A y2 unfolding closed_map_fibre_neighbourhood by blast
+      then obtain V V' where VV: "openin Y V \<and> closedin Y V' \<and> y2 \<in> V \<and> V \<subseteq> V'" and "V' \<subseteq> V0"
+        by (metis (no_types, lifting) \<open>regular_space Y\<close> neighbourhood_base_of neighbourhood_base_of_closedin)
+      with UA have subA: "{x \<in> topspace Z. g x \<in> V'} \<subseteq> A"
+        by blast
+      show ?thesis
+      proof -
+        define B where "B \<equiv> topspace Z - (C \<inter> {x \<in> topspace Z. g x \<in> V'})"
+        have "openin Z B"
+          using VV \<open>closedin Z C\<close> contg by (fastforce simp: B_def continuous_map_closedin)
+        have "{x \<in> topspace Z. f x = y1} \<subseteq> B"
+          using A_def subA by (auto simp: A_def B_def)
+        then obtain U where "openin X U" "y1 \<in> U" and subB: "{x \<in> topspace Z. f x \<in> U} \<subseteq> B"
+          using \<open>openin Z B\<close> y1 f unfolding closed_map_fibre_neighbourhood by meson
+        show ?thesis
+        proof (intro conjI exI)
+          show "openin (prod_topology X Y) (U \<times> V)"
+            by (metis VV \<open>openin X U\<close> openin_prod_Times_iff)
+          show "(y1, y2) \<in> U \<times> V"
+            by (simp add: VV \<open>y1 \<in> U\<close>)
+          show "U \<times> V \<subseteq> topspace X \<times> topspace Y - (\<lambda>x. (f x, g x)) ` C"
+            using VV \<open>C \<subseteq> topspace Z\<close> \<open>openin X U\<close> subB
+            by (force simp: image_iff B_def subset_iff dest: openin_subset)
+        qed
+      qed
+    qed
+    then show "openin (prod_topology X Y) (topspace X \<times> topspace Y - (\<lambda>x. (f x, g x)) ` C)"
+      by (smt (verit, ccfv_threshold) Diff_iff SigmaE openin_subopen)
+  qed
+qed
+
+
+lemma closed_map_paired_gen:
+  assumes f: "closed_map Z X f" and g: "closed_map Z Y g"
+  and D: "(regular_space X \<and> continuous_map Z X f \<and> (\<forall>z \<in> topspace Y. closedin Z {x \<in> topspace Z. g x = z})
+         \<or> regular_space Y \<and> continuous_map Z Y g \<and> (\<forall>y \<in> topspace X. closedin Z {x \<in> topspace Z. f x = y}))"
+         (is "?RSX \<or> ?RSY")
+       shows "closed_map Z (prod_topology X Y) (\<lambda>x. (f x, g x))"
+  using D
+proof
+  assume RSX: ?RSX
+  have eq: "(\<lambda>x. (f x, g x)) = (\<lambda>(x,y). (y,x)) \<circ> (\<lambda>x. (g x, f x))"
+    by auto
+  show ?thesis
+    unfolding eq
+  proof (rule closed_map_compose)
+    show "closed_map Z (prod_topology Y X) (\<lambda>x. (g x, f x))"
+      using RSX closed_map_paired_gen_aux f g by fastforce
+    show "closed_map (prod_topology Y X) (prod_topology X Y) (\<lambda>(x, y). (y, x))"
+      using homeomorphic_imp_closed_map homeomorphic_map_swap by blast
+  qed
+qed (blast intro: assms closed_map_paired_gen_aux)
+
+lemma closed_map_paired:
+  assumes "closed_map Z X f" and contf: "continuous_map Z X f"
+          "closed_map Z Y g" and contg: "continuous_map Z Y g"
+  and D: "t1_space X \<and> regular_space Y \<or> regular_space X \<and> t1_space Y"
+  shows "closed_map Z (prod_topology X Y) (\<lambda>x. (f x, g x))"
+proof (rule closed_map_paired_gen)
+  show "regular_space X \<and> continuous_map Z X f \<and> (\<forall>z\<in>topspace Y. closedin Z {x \<in> topspace Z. g x = z}) \<or> regular_space Y \<and> continuous_map Z Y g \<and> (\<forall>y\<in>topspace X. closedin Z {x \<in> topspace Z. f x = y})"
+    using D contf contg
+    by (smt (verit, del_insts) Collect_cong closedin_continuous_map_preimage t1_space_closedin_singleton singleton_iff)
+qed (use assms in auto)
+
+lemma closed_map_pairwise:
+  assumes  "closed_map Z X (fst \<circ> f)" "continuous_map Z X (fst \<circ> f)"
+    "closed_map Z Y (snd \<circ> f)" "continuous_map Z Y (snd \<circ> f)"
+    "t1_space X \<and> regular_space Y \<or> regular_space X \<and> t1_space Y"
+  shows "closed_map Z (prod_topology X Y) f"
+proof -
+  have "closed_map Z (prod_topology X Y) (\<lambda>a. ((fst \<circ> f) a, (snd \<circ> f) a))"
+    using assms closed_map_paired by blast
+  then show ?thesis
+    by auto
+qed
+
+
+lemma tube_lemma_right:
+  assumes W: "openin (prod_topology X Y) W" and C: "compactin Y C" 
+    and x: "x \<in> topspace X" and subW: "{x} \<times> C \<subseteq> W"
+  shows "\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> C \<subseteq> V \<and> U \<times> V \<subseteq> W"
+proof (cases "C = {}")
+  case True
+  with x show ?thesis by auto
+next
+  case False
+  have "\<exists>U V. openin X U \<and> openin Y V \<and> x \<in> U \<and> y \<in> V \<and> U \<times> V \<subseteq> W" 
+    if "y \<in> C" for y
+    using W openin_prod_topology_alt subW subsetD that by fastforce
+  then obtain U V where UV: "\<And>y. y \<in> C \<Longrightarrow> openin X (U y) \<and> openin Y (V y) \<and> x \<in> U y \<and> y \<in> V y \<and> U y \<times> V y \<subseteq> W" 
+    by metis
+  then obtain D where D: "finite D" "D \<subseteq> C" "C \<subseteq> \<Union> (V ` D)"
+    using compactinD [OF C, of "V`C"]
+    by (smt (verit) UN_I finite_subset_image imageE subsetI)
+  show ?thesis
+  proof (intro exI conjI)
+    show "openin X (\<Inter> (U ` D))" "openin Y (\<Union> (V ` D))"
+      using D False UV by blast+
+    show "x \<in> \<Inter> (U ` D)" "C \<subseteq> \<Union> (V ` D)" "\<Inter> (U ` D) \<times> \<Union> (V ` D) \<subseteq> W"
+      using D UV by force+
+  qed
+qed
+
+
+lemma closed_map_fst:
+  assumes "compact_space Y"
+  shows "closed_map (prod_topology X Y) X fst"
+proof -
+  have *: "{x \<in> topspace X \<times> topspace Y. fst x \<in> U} = U \<times> topspace Y"
+    if "U \<subseteq> topspace X" for U
+    using that by force
+  have **: "\<And>U y. \<lbrakk>openin (prod_topology X Y) U; y \<in> topspace X;
+            {x \<in> topspace X \<times> topspace Y. fst x = y} \<subseteq> U\<rbrakk>
+           \<Longrightarrow> \<exists>V. openin X V \<and> y \<in> V \<and> V \<times> topspace Y \<subseteq> U"
+    using tube_lemma_right[of X Y _ "topspace Y"] assms compact_space_def
+    by force
+  show ?thesis
+    unfolding closed_map_fibre_neighbourhood
+    by (force simp: * openin_subset cong: conj_cong intro: **)
+qed
+
+lemma closed_map_snd:
+  assumes "compact_space X"
+  shows "closed_map (prod_topology X Y) Y snd"
+proof -
+  have "snd = fst o prod.swap"
+    by force
+  moreover have "closed_map (prod_topology X Y) Y (fst o prod.swap)"
+  proof (rule closed_map_compose)
+    show "closed_map (prod_topology X Y) (prod_topology Y X) prod.swap"
+      by (metis (no_types, lifting) homeomorphic_imp_closed_map homeomorphic_map_eq homeomorphic_map_swap prod.swap_def split_beta)
+    show "closed_map (prod_topology Y X) Y fst"
+      by (simp add: closed_map_fst assms)
+  qed
+  ultimately show ?thesis
+    by metis
+qed
+
+lemma closed_map_paired_closed_map_right:
+   "\<lbrakk>closed_map X Y f; regular_space X;
+     \<And>y. y \<in> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x = y}\<rbrakk>
+    \<Longrightarrow> closed_map X (prod_topology X Y) (\<lambda>x. (x, f x))"
+  by (rule closed_map_paired_gen [OF closed_map_id, unfolded id_def]) auto
+
+lemma closed_map_paired_closed_map_left:
+  assumes "closed_map X Y f"  "regular_space X"
+    "\<And>y. y \<in> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x = y}"
+  shows "closed_map X (prod_topology Y X) (\<lambda>x. (f x, x))"
+proof -
+  have eq: "(\<lambda>x. (f x, x)) = (\<lambda>(x,y). (y,x)) \<circ> (\<lambda>x. (x, f x))"
+    by auto
+  show ?thesis
+    unfolding eq
+  proof (rule closed_map_compose)
+    show "closed_map X (prod_topology X Y) (\<lambda>x. (x, f x))"
+      by (simp add: assms closed_map_paired_closed_map_right)
+    show "closed_map (prod_topology X Y) (prod_topology Y X) (\<lambda>(x, y). (y, x))"
+      using homeomorphic_imp_closed_map homeomorphic_map_swap by blast
+  qed
+qed
+
+lemma closed_map_imp_closed_graph:
+  assumes "closed_map X Y f" "regular_space X"
+          "\<And>y. y \<in> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x = y}"
+  shows "closedin (prod_topology X Y) ((\<lambda>x. (x, f x)) ` topspace X)"
+  using assms closed_map_def closed_map_paired_closed_map_right by blast
+
+lemma proper_map_paired_closed_map_right:
+  assumes "closed_map X Y f" "regular_space X"
+    "\<And>y. y \<in> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x = y}"
+  shows "proper_map X (prod_topology X Y) (\<lambda>x. (x, f x))"
+  by (simp add: assms closed_injective_imp_proper_map inj_on_def closed_map_paired_closed_map_right)
+
+lemma proper_map_paired_closed_map_left:
+  assumes "closed_map X Y f" "regular_space X"
+    "\<And>y. y \<in> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x = y}"
+  shows "proper_map X (prod_topology Y X) (\<lambda>x. (f x, x))"
+  by (simp add: assms closed_injective_imp_proper_map inj_on_def closed_map_paired_closed_map_left)
+
+proposition regular_space_continuous_proper_map_image:
+  assumes "regular_space X" and contf: "continuous_map X Y f" and pmapf: "proper_map X Y f"
+    and fim: "f ` (topspace X) = topspace Y"
+  shows "regular_space Y"
+  unfolding regular_space_def
+proof clarify
+  fix C y
+  assume "closedin Y C" and "y \<in> topspace Y" and "y \<notin> C"
+  have "closed_map X Y f" "(\<forall>y \<in> topspace Y. compactin X {x \<in> topspace X. f x = y})"
+    using pmapf proper_map_def by force+
+  moreover have "closedin X {z \<in> topspace X. f z \<in> C}"
+    using \<open>closedin Y C\<close> contf continuous_map_closedin by fastforce
+  moreover have "disjnt {z \<in> topspace X. f z = y} {z \<in> topspace X. f z \<in> C}"
+    using \<open>y \<notin> C\<close> disjnt_iff by blast
+  ultimately
+  obtain U V where UV: "openin X U" "openin X V" "{z \<in> topspace X. f z = y} \<subseteq> U" "{z \<in> topspace X. f z \<in> C} \<subseteq> V"
+                  and dUV: "disjnt U V"
+    using \<open>y \<in> topspace Y\<close> \<open>regular_space X\<close> unfolding regular_space_compact_closed_sets
+    by meson
+
+  have *: "\<And>U T. openin X U \<and> T \<subseteq> topspace Y \<and> {x \<in> topspace X. f x \<in> T} \<subseteq> U \<longrightarrow>
+         (\<exists>V. openin Y V \<and> T \<subseteq> V \<and> {x \<in> topspace X. f x \<in> V} \<subseteq> U)"
+   using \<open>closed_map X Y f\<close> unfolding closed_map_preimage_neighbourhood by blast
+  obtain V1 where V1: "openin Y V1 \<and> y \<in> V1" and sub1: "{x \<in> topspace X. f x \<in> V1} \<subseteq> U"
+    using * [of U "{y}"] UV \<open>y \<in> topspace Y\<close> by auto
+  moreover
+  obtain V2 where "openin Y V2 \<and> C \<subseteq> V2" and sub2: "{x \<in> topspace X. f x \<in> V2} \<subseteq> V"
+    by (smt (verit, ccfv_SIG) * UV \<open>closedin Y C\<close> closedin_subset mem_Collect_eq subset_iff)
+  moreover have "disjnt V1 V2"
+  proof -
+    have "\<And>x. \<lbrakk>\<forall>x. x \<in> U \<longrightarrow> x \<notin> V; x \<in> V1; x \<in> V2\<rbrakk> \<Longrightarrow> False"
+      by (smt (verit) V1 fim image_iff mem_Collect_eq openin_subset sub1 sub2 subsetD)
+    with dUV show ?thesis by (auto simp: disjnt_iff)
+  qed
+  ultimately show "\<exists>U V. openin Y U \<and> openin Y V \<and> y \<in> U \<and> C \<subseteq> V \<and> disjnt U V"
+    by meson
+qed
+
+lemma regular_space_perfect_map_image:
+   "\<lbrakk>regular_space X; perfect_map X Y f\<rbrakk> \<Longrightarrow> regular_space Y"
+  by (meson perfect_map_def regular_space_continuous_proper_map_image)
+
+proposition regular_space_perfect_map_image_eq:
+  assumes "Hausdorff_space X" and perf: "perfect_map X Y f"
+  shows "regular_space X \<longleftrightarrow> regular_space Y" (is "?lhs=?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    using perf regular_space_perfect_map_image by blast
+next
+  assume R: ?rhs  
+  have "continuous_map X Y f" "proper_map X Y f" and fim: "f ` (topspace X) = topspace Y"
+    using perf by (auto simp: perfect_map_def)
+  then have "closed_map X Y f" and preYf: "(\<forall>y \<in> topspace Y. compactin X {x \<in> topspace X. f x = y})"
+    by (simp_all add: proper_map_def)
+  show ?lhs
+    unfolding regular_space_def
+  proof clarify
+    fix C x
+    assume "closedin X C" and "x \<in> topspace X" and "x \<notin> C"
+    obtain U1 U2 where "openin X U1" "openin X U2" "{x} \<subseteq> U1" and "disjnt U1 U2"
+      and subV: "C \<inter> {z \<in> topspace X. f z = f x} \<subseteq> U2"
+    proof (rule Hausdorff_space_compact_separation [of X "{x}" "C \<inter> {z \<in> topspace X. f z = f x}", OF \<open>Hausdorff_space X\<close>])
+      show "compactin X {x}"
+        by (simp add: \<open>x \<in> topspace X\<close>)
+      show "compactin X (C \<inter> {z \<in> topspace X. f z = f x})"
+        using \<open>closedin X C\<close> fim \<open>x \<in> topspace X\<close> closed_Int_compactin preYf by fastforce
+      show "disjnt {x} (C \<inter> {z \<in> topspace X. f z = f x})"
+        using \<open>x \<notin> C\<close> by force
+    qed
+    have "closedin Y (f ` (C - U2))"
+      using \<open>closed_map X Y f\<close> \<open>closedin X C\<close> \<open>openin X U2\<close> closed_map_def by blast
+    moreover
+    have "f x \<in> topspace Y - f ` (C - U2)"
+      using \<open>closedin X C\<close> \<open>continuous_map X Y f\<close> \<open>x \<in> topspace X\<close> closedin_subset continuous_map_def subV by fastforce
+    ultimately
+    obtain V1 V2 where VV: "openin Y V1" "openin Y V2" "f x \<in> V1" 
+                and subV2: "f ` (C - U2) \<subseteq> V2" and "disjnt V1 V2"
+      by (meson R regular_space_def)
+    show "\<exists>U U'. openin X U \<and> openin X U' \<and> x \<in> U \<and> C \<subseteq> U' \<and> disjnt U U'"
+    proof (intro exI conjI)
+      show "openin X (U1 \<inter> {x \<in> topspace X. f x \<in> V1})"
+        using VV(1) \<open>continuous_map X Y f\<close> \<open>openin X U1\<close> continuous_map by fastforce
+      show "openin X (U2 \<union> {x \<in> topspace X. f x \<in> V2})"
+        using VV(2) \<open>continuous_map X Y f\<close> \<open>openin X U2\<close> continuous_map by fastforce
+      show "x \<in> U1 \<inter> {x \<in> topspace X. f x \<in> V1}"
+        using VV(3) \<open>x \<in> topspace X\<close> \<open>{x} \<subseteq> U1\<close> by auto
+      show "C \<subseteq> U2 \<union> {x \<in> topspace X. f x \<in> V2}"
+        using \<open>closedin X C\<close> closedin_subset subV2 by auto
+      show "disjnt (U1 \<inter> {x \<in> topspace X. f x \<in> V1}) (U2 \<union> {x \<in> topspace X. f x \<in> V2})"
+        using \<open>disjnt U1 U2\<close> \<open>disjnt V1 V2\<close> by (auto simp: disjnt_iff)
+    qed
+  qed
+qed
+
+
+
+subsection\<open>Locally compact spaces\<close>
+
+definition locally_compact_space 
+  where "locally_compact_space X \<equiv>
+    \<forall>x \<in> topspace X. \<exists>U K. openin X U \<and> compactin X K \<and> x \<in> U \<and> U \<subseteq> K"
+
+lemma homeomorphic_locally_compact_spaceD:
+  assumes X: "locally_compact_space X" and "X homeomorphic_space Y"
+  shows "locally_compact_space Y"
+proof -
+  obtain f where hmf: "homeomorphic_map X Y f"
+    using assms homeomorphic_space by blast
+  then have eq: "topspace Y = f ` (topspace X)"
+    by (simp add: homeomorphic_imp_surjective_map)
+  have "\<exists>V K. openin Y V \<and> compactin Y K \<and> f x \<in> V \<and> V \<subseteq> K"
+    if "x \<in> topspace X" "openin X U" "compactin X K" "x \<in> U" "U \<subseteq> K" for x U K
+    using that 
+    by (meson hmf homeomorphic_map_compactness_eq homeomorphic_map_openness_eq image_mono image_eqI)
+  with X show ?thesis
+    by (smt (verit) eq image_iff locally_compact_space_def)
+qed
+
+lemma homeomorphic_locally_compact_space:
+  assumes "X homeomorphic_space Y"
+  shows "locally_compact_space X \<longleftrightarrow> locally_compact_space Y"
+  by (meson assms homeomorphic_locally_compact_spaceD homeomorphic_space_sym)
+
+lemma locally_compact_space_retraction_map_image:
+  assumes "retraction_map X Y r" and X: "locally_compact_space X"
+  shows "locally_compact_space Y"
+proof -
+  obtain s where s: "retraction_maps X Y r s"
+    using assms retraction_map_def by blast
+  obtain T where "T retract_of_space X" and Teq: "T = s ` topspace Y"
+    using retraction_maps_section_image1 s by blast
+  then obtain r where r: "continuous_map X (subtopology X T) r" "\<forall>x\<in>T. r x = x"
+    by (meson retract_of_space_def)
+  have "locally_compact_space (subtopology X T)"
+    unfolding locally_compact_space_def openin_subtopology_alt
+  proof clarsimp
+    fix x
+    assume "x \<in> topspace X" "x \<in> T"
+    obtain U K where UK: "openin X U \<and> compactin X K \<and> x \<in> U \<and> U \<subseteq> K"
+      by (meson X \<open>x \<in> topspace X\<close> locally_compact_space_def)
+    then have "compactin (subtopology X T) (r ` K) \<and> T \<inter> U \<subseteq> r ` K"
+      by (smt (verit) IntD1 image_compactin image_iff inf_le2 r subset_iff)
+    then show "\<exists>U. openin X U \<and> (\<exists>K. compactin (subtopology X T) K \<and> x \<in> U \<and> T \<inter> U \<subseteq> K)"
+      using UK by auto
+  qed
+  with Teq show ?thesis
+    using homeomorphic_locally_compact_space retraction_maps_section_image2 s by blast
+qed
+
+lemma compact_imp_locally_compact_space:
+   "compact_space X \<Longrightarrow> locally_compact_space X"
+  using compact_space_def locally_compact_space_def by blast
+
+lemma neighbourhood_base_imp_locally_compact_space:
+   "neighbourhood_base_of (compactin X) X \<Longrightarrow> locally_compact_space X"
+  by (metis locally_compact_space_def neighbourhood_base_of openin_topspace)
+
+lemma locally_compact_imp_neighbourhood_base:
+  assumes loc: "locally_compact_space X" and reg: "regular_space X"
+  shows "neighbourhood_base_of (compactin X) X"
+  unfolding neighbourhood_base_of
+proof clarify
+  fix W x
+  assume "openin X W" and "x \<in> W"
+  then obtain U K where "openin X U" "compactin X K" "x \<in> U" "U \<subseteq> K"
+    by (metis loc locally_compact_space_def openin_subset subsetD)
+  moreover have "openin X (U \<inter> W) \<and> x \<in> U \<inter> W"
+    using \<open>openin X W\<close> \<open>x \<in> W\<close> \<open>openin X U\<close> \<open>x \<in> U\<close> by blast
+  then have "\<exists>u' v. openin X u' \<and> closedin X v \<and> x \<in> u' \<and> u' \<subseteq> v \<and> v \<subseteq> U \<and> v \<subseteq> W"
+    using reg
+    by (metis le_infE neighbourhood_base_of neighbourhood_base_of_closedin)
+  then show "\<exists>U V. openin X U \<and> compactin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+    by (meson \<open>U \<subseteq> K\<close> \<open>compactin X K\<close> closed_compactin subset_trans)
+qed
+
+lemma Hausdorff_regular: "\<lbrakk>Hausdorff_space X; neighbourhood_base_of (compactin X) X\<rbrakk> \<Longrightarrow> regular_space X"
+  by (metis compactin_imp_closedin neighbourhood_base_of_closedin neighbourhood_base_of_mono)
+
+lemma locally_compact_Hausdorff_imp_regular_space: 
+  assumes loc: "locally_compact_space X" and "Hausdorff_space X"
+  shows "regular_space X"
+  unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of
+proof clarify
+  fix W x
+  assume "openin X W" and "x \<in> W"
+  then have "x \<in> topspace X"
+    using openin_subset by blast 
+  then obtain U K where "openin X U" "compactin X K" and UK: "x \<in> U" "U \<subseteq> K"
+    by (meson loc locally_compact_space_def)
+  with \<open>Hausdorff_space X\<close> have "regular_space (subtopology X K)"
+    using Hausdorff_space_subtopology compact_Hausdorff_imp_regular_space compact_space_subtopology by blast
+  then have "\<exists>U' V'. openin (subtopology X K) U' \<and> closedin (subtopology X K) V' \<and> x \<in> U' \<and> U' \<subseteq> V' \<and> V' \<subseteq> K \<inter> W"
+    unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of
+    by (meson IntI \<open>U \<subseteq> K\<close> \<open>openin X W\<close> \<open>x \<in> U\<close> \<open>x \<in> W\<close> openin_subtopology_Int2 subsetD)
+  then obtain V C where "openin X V" "closedin X C" and VC: "x \<in> K \<inter> V" "K \<inter> V \<subseteq> K \<inter> C" "K \<inter> C \<subseteq> K \<inter> W"
+    by (metis Int_commute closedin_subtopology openin_subtopology)
+  show "\<exists>U V. openin X U \<and> closedin X V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+  proof (intro conjI exI)
+    show "openin X (U \<inter> V)"
+      using \<open>openin X U\<close> \<open>openin X V\<close> by blast
+    show "closedin X (K \<inter> C)"
+      using \<open>closedin X C\<close> \<open>compactin X K\<close> compactin_imp_closedin \<open>Hausdorff_space X\<close> by blast
+  qed (use UK VC in auto)
+qed
+
+lemma locally_compact_space_neighbourhood_base:
+  "Hausdorff_space X \<or> regular_space X
+        \<Longrightarrow> locally_compact_space X \<longleftrightarrow> neighbourhood_base_of (compactin X) X"
+  by (metis locally_compact_imp_neighbourhood_base locally_compact_Hausdorff_imp_regular_space 
+            neighbourhood_base_imp_locally_compact_space)
+
+lemma locally_compact_Hausdorff_or_regular:
+   "locally_compact_space X \<and> (Hausdorff_space X \<or> regular_space X) \<longleftrightarrow> locally_compact_space X \<and> regular_space X"
+  using locally_compact_Hausdorff_imp_regular_space by blast
+
+lemma locally_compact_space_compact_closedin:
+  assumes  "Hausdorff_space X \<or> regular_space X"
+  shows "locally_compact_space X \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. \<exists>U K. openin X U \<and> compactin X K \<and> closedin X K \<and> x \<in> U \<and> U \<subseteq> K)"
+  using locally_compact_Hausdorff_or_regular unfolding locally_compact_space_def
+  by (metis assms closed_compactin inf.absorb_iff2 le_infE neighbourhood_base_of neighbourhood_base_of_closedin)
+
+lemma locally_compact_space_compact_closure_of:
+  assumes "Hausdorff_space X \<or> regular_space X"
+  shows "locally_compact_space X \<longleftrightarrow>
+         (\<forall>x \<in> topspace X. \<exists>U. openin X U \<and> compactin X (X closure_of U) \<and> x \<in> U)" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis assms closed_compactin closedin_closure_of closure_of_eq closure_of_mono locally_compact_space_compact_closedin)
+next
+  assume ?rhs then show ?lhs
+    by (meson closure_of_subset locally_compact_space_def openin_subset)
+qed
+
+lemma locally_compact_space_neighbourhood_base_closedin:
+  assumes "Hausdorff_space X \<or> regular_space X"
+  shows "locally_compact_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>C. compactin X C \<and> closedin X C) X" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then have "regular_space X"
+    using assms locally_compact_Hausdorff_imp_regular_space by blast
+  with L have "neighbourhood_base_of (compactin X) X"
+   by (simp add: locally_compact_imp_neighbourhood_base)
+  with \<open>regular_space X\<close> show ?rhs
+    by (smt (verit, ccfv_threshold) closed_compactin neighbourhood_base_of subset_trans neighbourhood_base_of_closedin)
+next
+  assume ?rhs then show ?lhs
+    using neighbourhood_base_imp_locally_compact_space neighbourhood_base_of_mono by blast
+qed
+
+lemma locally_compact_space_neighbourhood_base_closure_of:
+  assumes "Hausdorff_space X \<or> regular_space X"
+  shows "locally_compact_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>T. compactin X (X closure_of T)) X" 
+         (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then have "regular_space X"
+    using assms locally_compact_Hausdorff_imp_regular_space by blast
+  with L have "neighbourhood_base_of (\<lambda>A. compactin X A \<and> closedin X A) X"
+    using locally_compact_space_neighbourhood_base_closedin by blast
+  then show ?rhs
+    by (simp add: closure_of_closedin neighbourhood_base_of_mono)
+next
+  assume ?rhs then show ?lhs
+    unfolding locally_compact_space_def neighbourhood_base_of
+    by (meson closure_of_subset openin_topspace subset_trans)
+qed
+
+lemma locally_compact_space_neighbourhood_base_open_closure_of:
+  assumes "Hausdorff_space X \<or> regular_space X"
+  shows "locally_compact_space X \<longleftrightarrow> 
+             neighbourhood_base_of (\<lambda>U. openin X U \<and> compactin X (X closure_of U)) X"
+         (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then have "regular_space X"
+    using assms locally_compact_Hausdorff_imp_regular_space by blast
+  then have "neighbourhood_base_of (\<lambda>T. compactin X (X closure_of T)) X"
+    using L locally_compact_space_neighbourhood_base_closure_of by auto
+  with L show ?rhs
+    unfolding neighbourhood_base_of
+    by (meson closed_compactin closure_of_closure_of closure_of_eq closure_of_mono subset_trans)
+next
+  assume ?rhs then show ?lhs
+    unfolding locally_compact_space_def neighbourhood_base_of
+    by (meson closure_of_subset openin_topspace subset_trans)
+qed
+
+lemma locally_compact_space_compact_closed_compact:
+  assumes "Hausdorff_space X \<or> regular_space X"
+  shows "locally_compact_space X \<longleftrightarrow>
+         (\<forall>K. compactin X K
+              \<longrightarrow> (\<exists>U L. openin X U \<and> compactin X L \<and> closedin X L \<and> K \<subseteq> U \<and> U \<subseteq> L))"
+         (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then obtain U L where UL: "\<forall>x \<in> topspace X. openin X (U x) \<and> compactin X (L x) \<and> closedin X (L x) \<and> x \<in> U x \<and> U x \<subseteq> L x"
+    unfolding locally_compact_space_compact_closedin [OF assms]
+    by metis
+  show ?rhs
+  proof clarify
+    fix K
+    assume "compactin X K"
+    then have "K \<subseteq> topspace X"
+      by (simp add: compactin_subset_topspace)
+    then have *: "(\<forall>U\<in>U ` K. openin X U) \<and> K \<subseteq> \<Union> (U ` K)"
+      using UL by blast
+    with \<open>compactin X K\<close> obtain KF where KF: "finite KF" "KF \<subseteq> K" "K \<subseteq> \<Union>(U ` KF)"
+      by (metis compactinD finite_subset_image)
+    show "\<exists>U L. openin X U \<and> compactin X L \<and> closedin X L \<and> K \<subseteq> U \<and> U \<subseteq> L"
+    proof (intro conjI exI)
+      show "openin X (\<Union> (U ` KF))"
+        using "*" \<open>KF \<subseteq> K\<close> by fastforce
+      show "compactin X (\<Union> (L ` KF))"
+        by (smt (verit) UL \<open>K \<subseteq> topspace X\<close> KF compactin_Union finite_imageI imageE subset_iff)
+      show "closedin X (\<Union> (L ` KF))"
+        by (smt (verit) UL \<open>K \<subseteq> topspace X\<close> KF closedin_Union finite_imageI imageE subsetD)
+    qed (use UL \<open>K \<subseteq> topspace X\<close> KF in auto)
+  qed
+next
+  assume ?rhs then show ?lhs
+    by (metis compactin_sing insert_subset locally_compact_space_def)
+qed
+
+lemma locally_compact_regular_space_neighbourhood_base:
+   "locally_compact_space X \<and> regular_space X \<longleftrightarrow>
+        neighbourhood_base_of (\<lambda>C. compactin X C \<and> closedin X C) X"
+  using locally_compact_space_neighbourhood_base_closedin neighbourhood_base_of_closedin neighbourhood_base_of_mono by blast
+
+lemma locally_compact_kc_space:
+   "neighbourhood_base_of (compactin X) X \<and> kc_space X \<longleftrightarrow>
+        locally_compact_space X \<and> Hausdorff_space X"
+  using Hausdorff_imp_kc_space locally_compact_imp_kc_eq_Hausdorff_space locally_compact_space_neighbourhood_base by blast
+
+lemma locally_compact_kc_space_alt:
+   "neighbourhood_base_of (compactin X) X \<and> kc_space X \<longleftrightarrow>
+        locally_compact_space X \<and> Hausdorff_space X \<and> regular_space X"
+  using Hausdorff_regular locally_compact_kc_space by blast
+
+lemma locally_compact_kc_imp_regular_space:
+   "\<lbrakk>neighbourhood_base_of (compactin X) X; kc_space X\<rbrakk> \<Longrightarrow> regular_space X"
+  using Hausdorff_regular locally_compact_imp_kc_eq_Hausdorff_space by blast
+
+lemma kc_locally_compact_space:
+   "kc_space X
+    \<Longrightarrow> neighbourhood_base_of (compactin X) X \<longleftrightarrow> locally_compact_space X \<and> Hausdorff_space X \<and> regular_space X"
+  using Hausdorff_regular locally_compact_kc_space by blast
+
+lemma locally_compact_space_closed_subset:
+  assumes loc: "locally_compact_space X" and "closedin X S"
+  shows "locally_compact_space (subtopology X S)"
+proof (clarsimp simp: locally_compact_space_def)
+  fix x assume x: "x \<in> topspace X" "x \<in> S"
+  then obtain U K where UK: "openin X U \<and> compactin X K \<and> x \<in> U \<and> U \<subseteq> K"
+    by (meson loc locally_compact_space_def)
+  show "\<exists>U. openin (subtopology X S) U \<and> 
+            (\<exists>K. compactin (subtopology X S) K \<and> x \<in> U \<and> U \<subseteq> K)"
+  proof (intro conjI exI)
+    show "openin (subtopology X S) (S \<inter> U)"
+      by (simp add: UK openin_subtopology_Int2)
+    show "compactin (subtopology X S) (S \<inter> K)"
+      by (simp add: UK assms(2) closed_Int_compactin compactin_subtopology)
+  qed (use UK x in auto)
+qed
+
+lemma locally_compact_space_open_subset:
+  assumes reg: "regular_space X" and loc: "locally_compact_space X" and "openin X S"
+  shows "locally_compact_space (subtopology X S)"
+proof (clarsimp simp: locally_compact_space_def)
+  fix x assume x: "x \<in> topspace X" "x \<in> S"
+  then obtain U K where UK: "openin X U" "compactin X K" "x \<in> U" "U \<subseteq> K"
+    by (meson loc locally_compact_space_def)
+  have "openin X (U \<inter> S)"
+    by (simp add: UK \<open>openin X S\<close> openin_Int)
+  with UK reg x obtain V C 
+      where VC: "openin X V" "closedin X C" "x \<in> V" "V \<subseteq> C" "C \<subseteq> U" "C \<subseteq> S"
+    by (metis IntI le_inf_iff neighbourhood_base_of neighbourhood_base_of_closedin)
+  show "\<exists>U. openin (subtopology X S) U \<and> 
+            (\<exists>K. compactin (subtopology X S) K \<and> x \<in> U \<and> U \<subseteq> K)"
+  proof (intro conjI exI)
+    show "openin (subtopology X S) V"
+      using VC by (meson \<open>openin X S\<close> openin_open_subtopology order_trans)
+    show "compactin (subtopology X S) (C \<inter> K)"
+      using UK VC closed_Int_compactin compactin_subtopology by fastforce
+  qed (use UK VC x in auto)
+qed
+
+lemma locally_compact_space_discrete_topology:
+   "locally_compact_space (discrete_topology U)"
+  by (simp add: neighbourhood_base_imp_locally_compact_space neighbourhood_base_of_discrete_topology)
+
+lemma locally_compact_space_continuous_open_map_image:
+  "\<lbrakk>continuous_map X X' f; open_map X X' f;
+    f ` topspace X = topspace X'; locally_compact_space X\<rbrakk> \<Longrightarrow> locally_compact_space X'"
+unfolding locally_compact_space_def open_map_def
+  by (smt (verit, ccfv_SIG) image_compactin image_iff image_mono)
+
+lemma locally_compact_subspace_openin_closure_of:
+  assumes "Hausdorff_space X" and S: "S \<subseteq> topspace X" 
+    and loc: "locally_compact_space (subtopology X S)"
+  shows "openin (subtopology X (X closure_of S)) S"
+  unfolding openin_subopen [where S=S]
+proof clarify
+  fix a assume "a \<in> S"
+  then obtain T K where *: "openin X T" "compactin X K" "K \<subseteq> S" "a \<in> S" "a \<in> T" "S \<inter> T \<subseteq> K"
+    using loc unfolding locally_compact_space_def
+  by (metis IntE S compactin_subtopology inf_commute openin_subtopology topspace_subtopology_subset)
+  have "T \<inter> X closure_of S \<subseteq> X closure_of (T \<inter> S)"
+    by (simp add: "*"(1) openin_Int_closure_of_subset)
+  also have "... \<subseteq> S"
+    using * \<open>Hausdorff_space X\<close> by (metis closure_of_minimal compactin_imp_closedin order.trans inf_commute)
+  finally have "T \<inter> X closure_of S \<subseteq> T \<inter> S" by simp 
+  then have "openin (subtopology X (X closure_of S)) (T \<inter> S)"
+    unfolding openin_subtopology using \<open>openin X T\<close> S closure_of_subset by fastforce
+  with * show "\<exists>T. openin (subtopology X (X closure_of S)) T \<and> a \<in> T \<and> T \<subseteq> S"
+    by blast
+qed
+
+lemma locally_compact_subspace_closed_Int_openin:
+   "\<lbrakk>Hausdorff_space X \<and> S \<subseteq> topspace X \<and> locally_compact_space(subtopology X S)\<rbrakk>
+        \<Longrightarrow> \<exists>C U. closedin X C \<and> openin X U \<and> C \<inter> U = S"
+  by (metis closedin_closure_of inf_commute locally_compact_subspace_openin_closure_of openin_subtopology)
+
+lemma locally_compact_subspace_open_in_closure_of_eq:
+  assumes "Hausdorff_space X" and loc: "locally_compact_space X"
+  shows "openin (subtopology X (X closure_of S)) S \<longleftrightarrow> S \<subseteq> topspace X \<and> locally_compact_space(subtopology X S)" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then obtain "S \<subseteq> topspace X" "regular_space X"
+    using assms locally_compact_Hausdorff_imp_regular_space openin_subset by fastforce 
+  then have "locally_compact_space (subtopology (subtopology X (X closure_of S)) S)"
+    by (simp add: L loc locally_compact_space_closed_subset locally_compact_space_open_subset regular_space_subtopology)
+  then show ?rhs
+    by (metis L inf.orderE inf_commute le_inf_iff openin_subset subtopology_subtopology topspace_subtopology)
+next
+  assume ?rhs then show ?lhs
+    using  assms locally_compact_subspace_openin_closure_of by blast
+qed
+
+lemma locally_compact_subspace_closed_Int_openin_eq:
+  assumes "Hausdorff_space X" and loc: "locally_compact_space X"
+  shows "(\<exists>C U. closedin X C \<and> openin X U \<and> C \<inter> U = S) \<longleftrightarrow> S \<subseteq> topspace X \<and> locally_compact_space(subtopology X S)" (is "?lhs=?rhs")
+proof
+  assume L: ?lhs 
+  then obtain C U where "closedin X C" "openin X U" and Seq: "S = C \<inter> U"
+    by blast
+  then have "C \<subseteq> topspace X"
+    by (simp add: closedin_subset)
+  have "locally_compact_space (subtopology (subtopology X C) (topspace (subtopology X C) \<inter> U))"
+    proof (rule locally_compact_space_open_subset)
+  show "regular_space (subtopology X C)"
+    by (simp add: \<open>Hausdorff_space X\<close> loc locally_compact_Hausdorff_imp_regular_space regular_space_subtopology)
+  show "locally_compact_space (subtopology X C)"
+    by (simp add: \<open>closedin X C\<close> loc locally_compact_space_closed_subset)
+  show "openin (subtopology X C) (topspace (subtopology X C) \<inter> U)"
+    by (simp add: \<open>openin X U\<close> Int_left_commute inf_commute openin_Int openin_subtopology_Int2)
+qed
+    then show ?rhs
+      by (metis Seq \<open>C \<subseteq> topspace X\<close> inf.coboundedI1 subtopology_subtopology subtopology_topspace)
+next
+  assume ?rhs then show ?lhs
+  using assms locally_compact_subspace_closed_Int_openin by blast
+qed
+
+lemma dense_locally_compact_openin_Hausdorff_space:
+   "\<lbrakk>Hausdorff_space X; S \<subseteq> topspace X; X closure_of S = topspace X;
+     locally_compact_space (subtopology X S)\<rbrakk> \<Longrightarrow> openin X S"
+  by (metis locally_compact_subspace_openin_closure_of subtopology_topspace)
+
+lemma locally_compact_space_prod_topology:
+  "locally_compact_space (prod_topology X Y) \<longleftrightarrow>
+        topspace (prod_topology X Y) = {} \<or>
+        locally_compact_space X \<and> locally_compact_space Y" (is "?lhs=?rhs")
+proof (cases "topspace (prod_topology X Y) = {}")
+  case True
+  then show ?thesis
+    unfolding locally_compact_space_def by blast
+next
+  case False
+  then obtain w z where wz: "w \<in> topspace X" "z \<in> topspace Y"
+    by auto
+  show ?thesis 
+  proof
+    assume L: ?lhs then show ?rhs
+      by (metis wz empty_iff locally_compact_space_retraction_map_image retraction_map_fst retraction_map_snd)
+  next
+    assume R: ?rhs 
+    show ?lhs
+      unfolding locally_compact_space_def
+    proof clarsimp
+      fix x y
+      assume "x \<in> topspace X" and "y \<in> topspace Y"
+      obtain U C where "openin X U" "compactin X C" "x \<in> U" "U \<subseteq> C"
+        by (meson False R \<open>x \<in> topspace X\<close> locally_compact_space_def)
+      obtain V D where "openin Y V" "compactin Y D" "y \<in> V" "V \<subseteq> D"
+        by (meson False R \<open>y \<in> topspace Y\<close> locally_compact_space_def)
+      show "\<exists>U. openin (prod_topology X Y) U \<and> (\<exists>K. compactin (prod_topology X Y) K \<and> (x, y) \<in> U \<and> U \<subseteq> K)"
+      proof (intro exI conjI)
+        show "openin (prod_topology X Y) (U \<times> V)"
+          by (simp add: \<open>openin X U\<close> \<open>openin Y V\<close> openin_prod_Times_iff)
+        show "compactin (prod_topology X Y) (C \<times> D)"
+          by (simp add: \<open>compactin X C\<close> \<open>compactin Y D\<close> compactin_Times)
+        show "(x, y) \<in> U \<times> V"
+          by (simp add: \<open>x \<in> U\<close> \<open>y \<in> V\<close>)
+        show "U \<times> V \<subseteq> C \<times> D"
+          by (simp add: Sigma_mono \<open>U \<subseteq> C\<close> \<open>V \<subseteq> D\<close>)
+      qed
+    qed
+  qed
+qed
+
+lemma locally_compact_space_product_topology:
+   "locally_compact_space(product_topology X I) \<longleftrightarrow>
+        topspace(product_topology X I) = {} \<or>
+        finite {i \<in> I. \<not> compact_space(X i)} \<and> (\<forall>i \<in> I. locally_compact_space(X i))" (is "?lhs=?rhs")
+proof (cases "topspace (product_topology X I) = {}")
+  case True
+  then show ?thesis
+    by (simp add: locally_compact_space_def)
+next
+  case False
+  show ?thesis 
+  proof
+    assume L: ?lhs
+    obtain z where z: "z \<in> topspace (product_topology X I)"
+      using False by auto
+    with L z obtain U C where "openin (product_topology X I) U" "compactin (product_topology X I) C" "z \<in> U" "U \<subseteq> C"
+      by (meson locally_compact_space_def)
+    then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}" and "\<forall>i \<in> I. openin (X i) (V i)" 
+                    and "z \<in> PiE I V" "PiE I V \<subseteq> U"
+      by (auto simp: openin_product_topology_alt)
+    have "compact_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
+    proof -
+      have "compactin (X i) ((\<lambda>x. x i) ` C)"
+        using \<open>compactin (product_topology X I) C\<close> image_compactin
+        by (metis continuous_map_product_projection \<open>i \<in> I\<close>)
+      moreover have "V i \<subseteq> (\<lambda>x. x i) ` C"
+      proof -
+        have "V i \<subseteq> (\<lambda>x. x i) ` Pi\<^sub>E I V"
+          by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl \<open>i \<in> I\<close>)
+        also have "\<dots> \<subseteq> (\<lambda>x. x i) ` C"
+          using \<open>U \<subseteq> C\<close> \<open>Pi\<^sub>E I V \<subseteq> U\<close> by blast
+        finally show ?thesis .
+      qed
+      ultimately show ?thesis
+        by (metis closed_compactin closedin_topspace compact_space_def that(2))
+    qed
+    with finV have "finite {i \<in> I. \<not> compact_space (X i)}"
+      by (metis (mono_tags, lifting) mem_Collect_eq finite_subset subsetI)
+    moreover have "locally_compact_space (X i)" if "i \<in> I" for i
+      by (meson False L locally_compact_space_retraction_map_image retraction_map_product_projection that)
+    ultimately show ?rhs by metis
+  next
+    assume R: ?rhs 
+    show ?lhs
+      unfolding locally_compact_space_def
+    proof clarsimp
+      fix z
+      assume z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+      have "\<exists>U C. openin (X i) U \<and> compactin (X i) C \<and> z i \<in> U \<and> U \<subseteq> C \<and>
+                    (compact_space(X i) \<longrightarrow> U = topspace(X i) \<and> C = topspace(X i))" 
+        if "i \<in> I" for i
+        using that R z unfolding locally_compact_space_def compact_space_def
+        by (metis (no_types, lifting) False PiE_mem openin_topspace set_eq_subset)
+      then obtain U C where UC: "\<And>i. i \<in> I \<Longrightarrow> 
+             openin (X i) (U i) \<and> compactin (X i) (C i) \<and> z i \<in> U i \<and> U i \<subseteq> C i \<and>
+                    (compact_space(X i) \<longrightarrow> U i = topspace(X i) \<and> C i = topspace(X i))"
+        by metis
+      show "\<exists>U. openin (product_topology X I) U \<and> (\<exists>K. compactin (product_topology X I) K \<and> z \<in> U \<and> U \<subseteq> K)"
+      proof (intro exI conjI)
+        show "openin (product_topology X I) (Pi\<^sub>E I U)"
+        by (smt (verit) Collect_cong False R UC compactin_subspace openin_PiE_gen subset_antisym subtopology_topspace)
+        show "compactin (product_topology X I) (Pi\<^sub>E I C)"
+          by (simp add: UC compactin_PiE)
+      qed (use UC z in blast)+
+    qed
+  qed
+qed
+
+lemma locally_compact_space_sum_topology:
+   "locally_compact_space (sum_topology X I) \<longleftrightarrow> (\<forall>i \<in> I. locally_compact_space (X i))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (metis closed_map_component_injection embedding_map_imp_homeomorphic_space embedding_map_component_injection
+        embedding_imp_closed_map_eq homeomorphic_locally_compact_space locally_compact_space_closed_subset)
+next
+  assume R: ?rhs
+  show ?lhs
+    unfolding locally_compact_space_def
+  proof clarsimp
+    fix i y
+    assume "i \<in> I" and y: "y \<in> topspace (X i)"
+    then obtain U K where UK: "openin (X i) U" "compactin (X i) K" "y \<in> U" "U \<subseteq> K"
+      using R by (fastforce simp: locally_compact_space_def)
+    then show "\<exists>U. openin (sum_topology X I) U \<and> (\<exists>K. compactin (sum_topology X I) K \<and> (i, y) \<in> U \<and> U \<subseteq> K)"
+      by (metis \<open>i \<in> I\<close> continuous_map_component_injection image_compactin image_mono 
+          imageI open_map_component_injection open_map_def)
+  qed
+qed
+
+proposition quotient_map_prod_right:
+  assumes loc: "locally_compact_space Z" 
+    and reg: "Hausdorff_space Z \<or> regular_space Z" 
+    and f: "quotient_map X Y f"
+  shows "quotient_map (prod_topology Z X) (prod_topology Z Y) (\<lambda>(x,y). (x,f y))"
+proof -
+  define h where "h \<equiv> (\<lambda>(x::'a,y). (x,f y))"
+  have "continuous_map (prod_topology Z X) Y (f o snd)"
+    by (simp add: continuous_map_of_snd f quotient_imp_continuous_map)
+  then have cmh: "continuous_map (prod_topology Z X) (prod_topology Z Y) h"
+    by (simp add: h_def continuous_map_paired split_def continuous_map_fst o_def)
+  have fim: "f ` topspace X = topspace Y"
+    by (simp add: f quotient_imp_surjective_map)
+  moreover
+  have "openin (prod_topology Z X) {u \<in> topspace Z \<times> topspace X. h u \<in> W}
+   \<longleftrightarrow> openin (prod_topology Z Y) W"   (is "?lhs=?rhs")
+    if W: "W \<subseteq> topspace Z \<times> topspace Y" for W
+  proof
+    define S where "S \<equiv> {u \<in> topspace Z \<times> topspace X. h u \<in> W}"
+    assume ?lhs 
+    then have L: "openin (prod_topology Z X) S"
+      using S_def by blast
+    have "\<exists>T. openin (prod_topology Z Y) T \<and> (x0, z0) \<in> T \<and> T \<subseteq> W"
+      if \<section>: "(x0,z0) \<in> W" for x0 z0 
+    proof -
+      have x0: "x0 \<in> topspace Z"
+        using W that by blast
+      obtain y0 where y0: "y0 \<in> topspace X" "f y0 = z0"
+        by (metis W fim imageE insert_absorb insert_subset mem_Sigma_iff \<section>)
+      then have "(x0, y0) \<in> S"
+        by (simp add: S_def h_def that x0)
+      have "continuous_map Z (prod_topology Z X) (\<lambda>x. (x, y0))"
+        by (simp add: continuous_map_paired y0)
+      with openin_continuous_map_preimage [OF _ L] 
+      have ope_ZS: "openin Z {x \<in> topspace Z. (x,y0) \<in> S}"
+        by blast
+      obtain U U' where "openin Z U" "compactin Z U'" "closedin Z U'" 
+        "x0 \<in> U"  "U \<subseteq> U'" "U' \<subseteq> {x \<in> topspace Z. (x,y0) \<in> S}"
+        using loc ope_ZS x0 \<open>(x0, y0) \<in> S\<close>
+        by (force simp: locally_compact_space_neighbourhood_base_closedin [OF reg] 
+            neighbourhood_base_of)
+      then have D: "U' \<times> {y0} \<subseteq> S"
+        by (auto simp: )
+      define V where "V \<equiv> {z \<in> topspace Y. U' \<times> {y \<in> topspace X. f y = z} \<subseteq> S}"
+      have "z0 \<in> V"
+        using D y0 Int_Collect fim by (fastforce simp: h_def V_def S_def)
+      have "openin X {x \<in> topspace X. f x \<in> V} \<Longrightarrow> openin Y V"
+        using f unfolding V_def quotient_map_def subset_iff
+        by (smt (verit, del_insts) Collect_cong mem_Collect_eq)
+      moreover have "openin X {x \<in> topspace X. f x \<in> V}"
+      proof -
+        let ?Z = "subtopology Z U'"
+        have *: "{x \<in> topspace X. f x \<in> V} = topspace X - snd ` (U' \<times> topspace X - S)"
+          by (force simp: V_def S_def h_def simp flip: fim)
+        have "compact_space ?Z"
+          using \<open>compactin Z U'\<close> compactin_subspace by auto
+        moreover have "closedin (prod_topology ?Z X) (U' \<times> topspace X - S)"
+          by (simp add: L \<open>closedin Z U'\<close> closedin_closed_subtopology closedin_diff closedin_prod_Times_iff 
+              prod_topology_subtopology(1))
+        ultimately show ?thesis
+          using "*" closed_map_snd closed_map_def by fastforce
+      qed
+      ultimately have "openin Y V"
+        by metis
+      show ?thesis
+      proof (intro conjI exI)
+        show "openin (prod_topology Z Y) (U \<times> V)"
+          by (simp add: openin_prod_Times_iff \<open>openin Z U\<close> \<open>openin Y V\<close>)
+        show "(x0, z0) \<in> U \<times> V"
+          by (simp add: \<open>x0 \<in> U\<close> \<open>z0 \<in> V\<close>)
+        show "U \<times> V \<subseteq> W"
+          using \<open>U \<subseteq> U'\<close> by (force simp: V_def S_def h_def simp flip: fim)
+      qed
+    qed
+    with openin_subopen show ?rhs by force
+  next
+    assume ?rhs then show ?lhs
+      using openin_continuous_map_preimage cmh by fastforce
+  qed
+  ultimately show ?thesis
+    by (fastforce simp: image_iff quotient_map_def h_def)
+qed
+
+lemma quotient_map_prod_left:
+  assumes loc: "locally_compact_space Z" 
+    and reg: "Hausdorff_space Z \<or> regular_space Z" 
+    and f: "quotient_map X Y f"
+  shows "quotient_map (prod_topology X Z) (prod_topology Y Z) (\<lambda>(x,y). (f x,y))"
+proof -
+  have "(\<lambda>(x,y). (f x,y)) = prod.swap \<circ> (\<lambda>(x,y). (x,f y)) \<circ> prod.swap"
+    by force
+  then
+  show ?thesis
+    apply (rule ssubst)
+  proof (intro quotient_map_compose)
+    show "quotient_map (prod_topology X Z) (prod_topology Z X) prod.swap"
+      "quotient_map (prod_topology Z Y) (prod_topology Y Z) prod.swap"
+      using homeomorphic_map_def homeomorphic_map_swap quotient_map_eq by fastforce+
+    show "quotient_map (prod_topology Z X) (prod_topology Z Y) (\<lambda>(x, y). (x, f y))"
+      by (simp add: f loc quotient_map_prod_right reg)
+  qed
+qed
+
+lemma locally_compact_space_perfect_map_preimage:
+  assumes "locally_compact_space X'" and f: "perfect_map X X' f"
+  shows "locally_compact_space X"
+  unfolding locally_compact_space_def
+proof (intro strip)
+  fix x
+  assume x: "x \<in> topspace X"
+  then obtain U K where "openin X' U" "compactin X' K" "f x \<in> U" "U \<subseteq> K"
+    using assms unfolding locally_compact_space_def perfect_map_def
+    by (metis (no_types, lifting) continuous_map_closedin)
+  show "\<exists>U K. openin X U \<and> compactin X K \<and> x \<in> U \<and> U \<subseteq> K"
+  proof (intro exI conjI)
+    have "continuous_map X X' f"
+      using f perfect_map_def by blast
+    then show "openin X {x \<in> topspace X. f x \<in> U}"
+      by (simp add: \<open>openin X' U\<close> continuous_map)
+    show "compactin X {x \<in> topspace X. f x \<in> K}"
+      using \<open>compactin X' K\<close> f perfect_imp_proper_map proper_map_alt by blast
+  qed (use x \<open>f x \<in> U\<close> \<open>U \<subseteq> K\<close> in auto)
+qed
+
+end
+
diff -r 2b07535e0d27 -r c35f06b0931e src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Thu May 04 11:14:07 2023 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Sat May 06 11:10:23 2023 +0100
@@ -6,6 +6,7 @@
   (* Topology *)
   FSigma
   Sum_Topology
+  Abstract_Topological_Spaces
   Connected
   Abstract_Limits
   Isolated