Theory Abstract_Topological_Spaces

(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light] *)

section ‹Various Forms of Topological Spaces›

theory Abstract_Topological_Spaces
  imports Lindelof_Spaces Locally Abstract_Euclidean_Space Sum_Topology FSigma
begin


subsection‹Connected topological spaces›

lemma connected_space_eq_frontier_eq_empty:
   "connected_space X  (S. S  topspace X  X frontier_of S = {}  S = {}  S = topspace X)"
  by (meson clopenin_eq_frontier_of connected_space_clopen_in)

lemma connected_space_frontier_eq_empty:
   "connected_space X  S  topspace X
         (X frontier_of S = {}  S = {}  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 
        C  topspace X  (S T. separatedin X S T  C  S  T  C  S  C  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:
   "connectedin X C; closedin X T; openin X T  C  T  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_retraction_map_image:
   "retraction_map X X' r; connected_space X  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: "a. S = {a}"
  shows "S  X derived_set_of S"
unfolding derived_set_of_def
proof (intro subsetI CollectI conjI strip)
  show XS: "x  topspace X" if "x  S" for x
    using that S connectedin by fastforce 
  show "y. y  x  y  S  y  T"
    if "x  S" and "x  T  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  T  (topspace X - {x})"
      using XS that(2) by auto
    moreover have "(topspace X - {x})  S  {}"
      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:
  "Hausdorff_space X; connectedin X S; a. S = {a}  S  X derived_set_of S"
  by (simp add: Hausdorff_imp_t1_space connectedin_imp_perfect_gen)



subsection‹The notion of "separated between" (complement of "connected between)"›

definition separated_between 
  where "separated_between X S T 
        U V. openin X U  openin X V  U  V = topspace X  disjnt U V  S  U  T  V"

lemma separated_between_alt:
   "separated_between X S T 
        (U V. closedin X U  closedin X V  U  V = topspace X  disjnt U V  S  U  T  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 
        (U. closedin X U  openin X U  S  U  T  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:
   "separated_between X S T; S'  S; T'  T  separated_between X S' T'"
  by (meson order.trans separated_between)

lemma separated_between_refl:
   "separated_between X S S  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  separated_between X T S"
  by (metis disjnt_sym separated_between_alt sup_commute)

lemma separated_between_imp_subset:
   "separated_between X S T  S  topspace X  T  topspace X"
  by (metis le_supI1 le_supI2 separated_between_def)

lemma separated_between_empty: 
  "(separated_between X {} S  S  topspace X)  (separated_between X S {}  S  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  U)  separated_between X S T  separated_between X S U"
  by (auto simp: separated_between)

lemma separated_between_Un': 
  "separated_between X (S  T) U  separated_between X S U  separated_between X T U"
  by (simp add: separated_between_Un separated_between_sym)

lemma separated_between_imp_disjoint:
   "separated_between X S T  disjnt S T"
  by (meson disjnt_iff separated_between_def subsetD)

lemma separated_between_imp_separatedin:
   "separated_between X S T  separatedin X S T"
  by (meson separated_between_def separatedin_mono separatedin_open_sets)

lemma separated_between_full:
  assumes "S  T = topspace X"
  shows "separated_between X S T  disjnt S T  closedin X S  openin X S  closedin X T  openin X T"
proof -
  have "separated_between X S T  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  T = topspace X  (separated_between X S T  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 
         (S = {}  T  topspace X)  (x  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  topspace X"
    by (meson equals0I separated_between_imp_subset)
  show ?lhs
  proof -
    obtain U where U: "x  S. openin X (U x)"
      "x  S. V. openin X V  U x  V = topspace X  disjnt (U x) V  {x}  U x  T  V"
      using R unfolding separated_between_def by metis
    then have "S  (U ` S)"
      by blast
    then obtain K where "finite K" "K  S" and K: "S  (iK. 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 "x. x  K  closedin X (U x)"
        by (smt (verit) K  S Diff_cancel U(2) Un_Diff Un_Diff_Int disjnt_def openin_closedin_eq subsetD)
      then show "closedin X ( (U ` K))"
        by (metis (mono_tags, lifting) finite K closedin_Union finite_imageI image_iff)
      show "openin X ( (U ` K))"
        using U(1) K  S by blast
      show "S   (U ` K)"
        by (simp add: K)
      have "x i. x  T; i  K; x  U i  False"
        by (meson U(2) K  S disjnt_iff subsetD)
      then show "T  topspace X -  (U ` K)"
        using T  topspace X by auto
    qed
  qed
qed

lemma separated_between_pointwise_right:
   "compactin X T
         separated_between X S T  (T = {}  S  topspace X)  (y  T. separated_between X S {y})"
  by (meson separated_between_pointwise_left separated_between_sym)

lemma separated_between_closure_of:
  "S  topspace X  separated_between X (X closure_of S) T  separated_between X S T"
  by (meson closure_of_minimal_eq separated_between_alt)


lemma separated_between_closure_of':
 "T  topspace X  separated_between X S (X closure_of T)  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  S  topspace X  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  T  topspace X  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 
   T  topspace X  disjnt S T  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  U" "X closure_of T - X interior_of T  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  U - T" "T  topspace X - (U - T)"
        using R U(3) by (force simp: disjnt_iff)+
      have "T  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  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  S  topspace X  disjnt S T  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:
  "S  topspace X; disjnt S T
    (separated_between X (X frontier_of S) T  separated_between X S T)"
  using separated_between_frontier_of_eq by blast

lemma separated_between_frontier_of':
 "T  topspace X; disjnt S T
    (separated_between X S (X frontier_of T)  separated_between X S T)"
  using separated_between_frontier_of_eq' by auto

lemma connected_space_separated_between:
  "connected_space X  (S T. separated_between X S T  S = {}  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
         (separated_between X S T  S = {}  T  topspace X  S  topspace X  T = {})"
  by (metis connected_space_separated_between separated_between_empty)


subsection‹Connected components›

lemma connected_component_of_subtopology_eq:
   "connected_component_of (subtopology X U) a = connected_component_of X a 
    connected_component_of_set X a  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  connected_components_of X" "C  U"
  shows "C  connected_components_of (subtopology X U)"
proof -
  obtain a where a: "connected_component_of_set X a  U" and "a  topspace X"
             and Ceq: "C = connected_component_of_set X a"
    using assms by (force simp: connected_components_of_def)
  then have "a  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 a  U a  topspace X connected_component_in_connected_components_of)
qed

lemma open_in_finite_connected_components:
  assumes "finite(connected_components_of X)" "C  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  connected_components_of X" "C'  connected_components_of X"
    shows "(disjnt C C'  (C  C'))"
  using assms nonempty_connected_components_of pairwiseD pairwise_disjoint_connected_components_of by fastforce

lemma connected_components_of_overlap:
   "C  connected_components_of X; C'  connected_components_of X  C  C'  {}  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)  finite(connected_components_of X)"
  by (simp add: Union_connected_components_of finite_UnionD)

lemma connected_component_of_unique:
   "x  C; connectedin X C; C'. x  C'  connectedin X C'  C'  C
         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:
   "C  connected_components_of (subtopology X s); X closure_of C  s  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  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) = (λx. {x}) ` U"
  by (simp add: connected_component_of_discrete_topology connected_components_of_def)

lemma connected_component_of_continuous_image:
   "continuous_map X Y f; connected_component_of X x y
         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  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 " "x. x  topspace X  g (f x) = x" 
    "y. y  topspace Y  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 × connected_component_of_set Y y"
proof (cases "x  topspace X  y  topspace Y")
  case True
  show ?thesis
  proof (rule connected_component_of_unique)
    show "(x, y)  connected_component_of_set X x × 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 × connected_component_of_set Y y)"
      by (metis connectedin_Times connectedin_connected_component_of)
    show "C  connected_component_of_set X x × connected_component_of_set Y y"
      if "(x, y)  C  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 × D |C D. C  connected_components_of X  D  connected_components_of Y}" (is "?lhs=?rhs")
proof
  show "?lhs  ?rhs"
    apply (clarsimp simp: connected_components_of_def)
    by (metis (no_types) connected_component_of_pair imageI)
next
  show "?rhs  ?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  extensional I then PiE I (λi. connected_component_of_set (X i) (x i)) else {})"
    (is "?lhs = If _ ?R _")    
proof (cases "x  topspace(product_topology X I)")
  case True
  have "?lhs = (ΠE iI. connected_component_of_set (X i) (x i))"
    if xX: "i. iI  x i  topspace (X i)" and ext: "x  extensional I"
  proof (rule connected_component_of_unique)
    show "x  ?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  ?R"
      if "x  C  connectedin (product_topology X I) C" for C 
    proof -
      have "C  extensional I"
        using PiE_def connectedin_subset_topspace that by fastforce
      have "y. y  C  y  (Π iI. 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 C  extensional I by fastforce
    qed
  qed
  with True show ?thesis
    by (simp add: PiE_iff)
next
  case False
  then show ?thesis
    by (smt (verit, best) PiE_eq_empty_iff PiE_iff connected_component_of_eq_empty topspace_product_topology)
qed


lemma connected_components_of_product_topology:
   "connected_components_of (product_topology X I) =
    {PiE I B |B. i  I. B i  connected_components_of(X i)}"  (is "?lhs=?rhs")
proof
  show "?lhs  ?rhs"
    by (auto simp: connected_components_of_def connected_component_of_product_topology PiE_iff)
  show "?rhs  ?lhs"
  proof
    fix F
    assume "F  ?rhs"
    then obtain B where Feq: "F = PiE I B" and
      "iI. xtopspace (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: "i. i  I  f i  topspace (X i)  B i = connected_component_of_set (X i) (f i)"
      by metis
    then have "(λiI. f i)  ((ΠE iI. topspace (X i))  extensional I)"
      by simp
    with f show "F  ?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 ‹Monotone maps (in the general topological sense)›


definition monotone_map 
  where "monotone_map X Y f ==
        f ` (topspace X)  topspace Y 
        (y  topspace Y. connectedin X {x  topspace X. f x = y})"

lemma monotone_map:
  "monotone_map X Y f 
   f ` (topspace X)  topspace Y  (y. connectedin X {x  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  monotone_map X Y f  f ` (topspace X)  S"
  by (smt (verit, del_insts) le_inf_iff monotone_map topspace_subtopology)

lemma monotone_map_from_subtopology:
  assumes "monotone_map X Y f" 
    "x y. x  topspace X; y  topspace X; x  S; f x = f y  y  S"
  shows "monotone_map (subtopology X S) Y f"
proof -
  have "y. y  topspace Y  connectedin X {x  topspace X. x  S  f x = y}"
    by (smt (verit) Collect_cong assms connectedin_empty empty_def monotone_map_def)
  then show ?thesis
    using assms by (auto simp: monotone_map_def connectedin_subtopology)
qed

lemma monotone_map_restriction:
  "monotone_map X Y f  {x  topspace X. f x  v} = u
         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  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  topspace Y"
  then have "{x  topspace X. f x = y} = {}  (a  topspace X. {x  topspace X. f x = y} = {a})"
    using assms(2) unfolding inj_on_def by blast
  then show "connectedin X {x  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  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  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  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 "¬ connected_space X"
  then obtain U V where "openin X U" "openin X V" "U  V = {}"
    "U  {}" "V  {}" and topUV: "topspace X  U  V"
    by (auto simp: connected_space_def)
  then have UVsub: "U  topspace X" "V  topspace X"
    by (auto simp: openin_subset)
  have "¬ connected_space Y"
    unfolding connected_space_def not_not
  proof (intro exI conjI)
    show "topspace Y  f`U  f`V"
      by (metis f(2) image_Un quotient_imp_surjective_map subset_Un_eq topUV)
    show "f`U  {}"
      by (simp add: U  {})
    show "(f`V)  {}"
      by (simp add: V  {})
    have *: "y  f ` V" if "y  f ` U" for y
    proof -
      have §: "connectedin X {x  topspace X. f x = y}"
        using f(1) monotone_map by fastforce
      show ?thesis
        using connectedinD [OF § openin X U openin X V] UVsub topUV U  V = {} that
        by (force simp: disjoint_iff)
    qed
    then show "f`U  f`V = {}"
      by blast
    show "openin Y (f`U)"
      using f openin X U topUV * unfolding quotient_map_saturated_open by force
    show "openin Y (f`V)"
      using f openin X V 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  closedin Y C"
  shows "connectedin X {x  topspace X. f x  C}"
proof -
  have "connected_space (subtopology X {x  topspace X. f x  C})"
  proof -
    have "connected_space (subtopology Y C)"
      using connectedin Y C connectedin_def by blast
    moreover have "quotient_map (subtopology X {a  topspace X. f a  C}) (subtopology Y C) f"
      by (simp add: assms quotient_map_restriction)
    ultimately show ?thesis
      using monotone_map X Y f 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  (C. connectedin Y C  connectedin X {x  topspace X. f x  C})"
         (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding connectedin_def
  proof (intro strip conjI)
    fix C
    assume C: "C  topspace Y  connected_space (subtopology Y C)"
    show "connected_space (subtopology X {x  topspace X. f x  C})"
    proof (rule connected_space_monotone_quotient_map_preimage)
      show "monotone_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
        by (simp add: L monotone_map_restriction)
      show "quotient_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
      proof (rule continuous_open_imp_quotient_map)
        show "continuous_map (subtopology X {x  topspace X. f x  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 "y. connectedin Y {y}  connectedin X {x  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  (C. connectedin Y C  connectedin X {x  topspace X. f x  C})" 
         (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding connectedin_def
  proof (intro strip conjI)
    fix C
    assume C: "C  topspace Y  connected_space (subtopology Y C)"
    show "connected_space (subtopology X {x  topspace X. f x  C})"
    proof (rule connected_space_monotone_quotient_map_preimage)
      show "monotone_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
        by (simp add: L monotone_map_restriction)
      show "quotient_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
      proof (rule continuous_closed_imp_quotient_map)
        show "continuous_map (subtopology X {x  topspace X. f x  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 "y. connectedin Y {y}  connectedin X {x  topspace X. f x = y}"
    by (smt (verit) Collect_cong singletonD singletonI)
  then show ?lhs
    by (simp add: fim monotone_map_def)
qed

subsection‹Other countability properties›

definition second_countable
  where "second_countable X 
         . countable   (V  . openin X V) 
             (U x. openin X U  x  U  (V  . x  V  V  U))"

definition first_countable
  where "first_countable X 
        x  topspace X.
         . countable   (V  . openin X V) 
             (U. openin X U  x  U  (V  . x  V  V  U))"

definition separable_space
  where "separable_space X 
        C. countable C  C  topspace X  X closure_of C = topspace X"

lemma second_countable:
   "second_countable X 
        (. countable   openin X = arbitrary union_of (λx. x  ))"
  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  where : "countable " "V. V    openin X V"
    "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  show ?thesis
    unfolding second_countable_def
  proof (intro exI conjI)
    show "V((∩)S) ` . openin (subtopology X S) V"
      using openin_subtopology_Int2  by blast
    show "U x. openin (subtopology X S) U  x  U  (V((∩)S) ` . x  V  V  U)"
      using  unfolding openin_subtopology
      by (smt (verit, del_insts) IntI image_iff inf_commute inf_le1 subset_iff)
  qed (use  in auto)
qed


lemma second_countable_discrete_topology:
   "second_countable(discrete_topology U)  countable U" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  then
  obtain  where : "countable " "V. V    V  U"
    "W x. W  U  x  W  (V  . x  V  V  W)"
    by (auto simp: second_countable_def)
  then have "{x}  " if "x  U" for x
    by (metis empty_subsetI insertCI insert_subset subset_antisym that)
  then show ?rhs
    by (smt (verit) countable_subset image_subsetI countable  countable_image_inj_on [OF _ inj_singleton])
next
  assume ?rhs 
  then show ?lhs
    unfolding second_countable_def
    by (rule_tac x="(λ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: "U. openin X U  openin Y (f ` U)"
    using assms by (auto simp: open_map_def)
  obtain  where : "countable " "V. V    openin X V"
    and *: "U x. openin X U  x  U  (V  . x  V  V  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  y  V"
    then obtain x where "x  topspace X" and x: "f x = y"
      by (metis fim image_iff openin_subset subsetD)

    then obtain W where "W" "x  W" "W  {x  topspace X. f x  V}"
      using * [of "{x  topspace X. f x  V}" x] V assms openin_continuous_map_preimage 
      by force
    then show "W  (image f) ` . y  W  W  V"
      using x by auto
  qed (use  openXYf in auto)
qed

lemma homeomorphic_space_second_countability:
   "X homeomorphic_space Y  (second_countable X  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:
   "retraction_map X Y r; second_countable X  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  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  topspace (subtopology X S)"
  then obtain  where "countable " and : "V. V    openin X V"
    "U. openin X U  x  U  (V  . x  V  V  U)"
    using assms first_countable_def by force
  show ". countable   (V. openin (subtopology X S) V)  (U. openin (subtopology X S) U  x  U  (V. x  V  V  U))"
  proof (intro exI conjI strip)
    show "countable (((∩)S) ` )"
      using countable  by blast
    show "openin (subtopology X S) V" if "V  ((∩)S) ` " for V
      using  openin_subtopology_Int2 that by fastforce
    show "V((∩)S) ` . x  V  V  U"
      if "openin (subtopology X S) U  x  U" for U 
      using that (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  U"
  show ". countable   (V. V  U)  (Ua. Ua  U  x  Ua  (V. x  V  V  Ua))"
    using x  U 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  topspace Y"
  have openXYf: "U. openin X U  openin Y (f ` U)"
    using assms by (auto simp: open_map_def)
  then obtain x where x: "x  topspace X" "f x = y"
    by (metis y  topspace Y fim imageE)
  obtain  where : "countable " "V. V    openin X V"
    and *: "U. openin X U  x  U  (V  . x  V  V  U)"
    using assms x first_countable_def by force
  show ". countable  
              (V. openin Y V)  (U. openin Y U  y  U  (V. y  V  V  U))"
  proof (intro exI conjI strip)
    fix V assume "openin Y V  y  V"
    then have "W. x  W  W  {x  topspace X. f x  V}"
      using * [of "{x  topspace X. f x  V}"] assms openin_continuous_map_preimage x 
      by fastforce
    then show "V'  (image f) ` . y  V'  V'  V"
      using image_mono x by auto 
  qed (use  openXYf in force)+
qed

lemma homeomorphic_space_first_countability:
  "X homeomorphic_space Y  first_countable X  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:
   "retraction_map X Y r; first_countable X  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  topspace X" "X closure_of C = topspace X"
    by (meson assms separable_space_def)
  then have "x T. x  topspace X; x  T; openin (subtopology X S) T
            y. y  S  y  C  y  T"
    by (smt (verit) openin X S in_closure_of openin_open_subtopology subsetD)
  with C openin X S show ?thesis
    unfolding separable_space_def
    by (rule_tac x="S  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: "S. f ` (X closure_of S)  Y closure_of f ` S"
    by (simp add: assms continuous_map_image_closure_subset)
  obtain C where C: "countable C" "C  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:
  "quotient_map X Y q; separable_space X  separable_space Y"
  by (meson quotient_imp_continuous_map quotient_imp_surjective_map separable_space_continuous_map_image)

lemma separable_space_retraction_map_image:
  "retraction_map X Y r; separable_space X  separable_space Y"
  using retraction_imp_quotient_map separable_space_quotient_map_image by blast

lemma homeomorphic_separable_space:
  "X homeomorphic_space Y  (separable_space X  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)  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  where : "countable " "V. V    openin X V"
    and *: "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  obtain c where c: "V. V  ; V  {}  c V  V"
    by (metis all_not_in_conv)
  then have **: "x. x  topspace X  x  X closure_of c ` ( - {{}})"
    using * by (force simp: closure_of_def)
  show ?thesis
    unfolding separable_space_def
  proof (intro exI conjI)
    show "countable (c ` (-{{}}))"
      using (1) by blast
    show "(c ` (-{{}}))  topspace X"
      using (2) c openin_subset by fastforce
    show "X closure_of (c ` (-{{}})) = 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 𝒰
  assume "U  𝒰. openin X U" and UU: "𝒰 = topspace X"
  obtain  where : "countable " "V. V    openin X V"
    and *: "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  define ℬ' where "ℬ' = {B  . U. U  𝒰  B  U}"
  have ℬ': "countable ℬ'" "ℬ' = 𝒰"
    using  using "*" U𝒰. openin X U by (fastforce simp: ℬ'_def)+
  have "b. U. b  ℬ'  U  𝒰  b  U" 
    by (simp add: ℬ'_def)
  then obtain G where G: "b. b  ℬ'  G b  𝒰  b  G b" 
    by metis
  with ℬ' UU show "𝒱. countable 𝒱  𝒱  𝒰  𝒱 = topspace X"
    by (rule_tac x="G ` ℬ'" in exI) fastforce
qed

subsection ‹Neigbourhood bases EXTRAS›

text ‹Neigbourhood bases: useful for "local" properties of various kinds›

lemma openin_topology_neighbourhood_base_unique:
   "openin X = arbitrary union_of P 
        (u. P u  openin X u)  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
         (neighbourhood_base_at x P X 
             (w. b w  x  w  (u v. openin X u  P v  x  u  u  v  v  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 "S t. P S  openin X t  (t  {})  t  S  P t"
  shows "neighbourhood_base_of P X 
         (x  topspace X. u v. openin X u  P v  x  u  u  v  v  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)  x  u  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)  (x  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  
  (. countable   (V  . openin X V)  neighbourhood_base_of (λA. A) X)"
  by (metis (full_types) openin_topology_neighbourhood_base_unique second_countable)

lemma first_countable_neighbourhood_base_alt:
   "first_countable X 
    (x  topspace X. . countable   (V  . openin X V)  neighbourhood_base_at x (λV. V  ) 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 
        (. countable   neighbourhood_base_of (λV. V  ) X)" (is "?lhs=?rhs")
proof
  assume ?lhs 
  then show ?rhs
    using second_countable_neighbourhood_base_alt by blast
next
  assume ?rhs 
  then obtain  where "countable "
    and : "W x. openin X W  x  W  (U. openin X U  (V. V    x  U  U  V  V  W))"
    by (metis neighbourhood_base_of)
  then show ?lhs
    unfolding second_countable_neighbourhood_base_alt neighbourhood_base_of
    apply (rule_tac x="(λu. X interior_of u) ` " 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 
    (x  topspace X. . countable   neighbourhood_base_at x (λV. V  ) 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  topspace X"
    with R obtain  where "countable " and : "neighbourhood_base_at x (λV. V  ) X"
      by blast
    then
    show ". countable   Ball  (openin X)  neighbourhood_base_at x (λV. V  ) X"
      unfolding neighbourhood_base_at_def
      apply (rule_tac x="(λu. X interior_of u) ` " in exI)
      by (smt (verit, best) countable_image image_iff interior_of_eq interior_of_mono openin_interior_of)
  qed
qed


subsection‹$T_0$ spaces and the Kolmogorov quotient›

definition t0_space where
  "t0_space X 
     x  topspace X. y  topspace X. x  y  (U. openin X U  (x  U  y  U))"

lemma t0_space_expansive:
   "topspace Y = topspace X; U. openin X U  openin Y U  t0_space X  t0_space Y"
  by (metis t0_space_def)

lemma t1_imp_t0_space: "t1_space X  t0_space X"
  by (metis t0_space_def t1_space_def)

lemma t1_eq_symmetric_t0_space_alt:
   "t1_space X 
      t0_space X 
      (x  topspace X. y  topspace X. x  X closure_of {y}  y  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  t0_space X  (x y. x  X closure_of {y}  y  X closure_of {x})"
  by (auto simp: t1_eq_symmetric_t0_space_alt in_closure_of)

lemma Hausdorff_imp_t0_space:
   "Hausdorff_space X  t0_space X"
  by (simp add: Hausdorff_imp_t1_space t1_imp_t0_space)

lemma t0_space:
   "t0_space X 
    (x  topspace X. y  topspace X. x  y  (C. closedin X C  (x  C  y  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  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 
    (x  topspace X. y  topspace X. X closure_of {x} = X closure_of {y}  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  t0_space (subtopology X U)"
  by (simp add: t0_space_def openin_subtopology) (metis Int_iff)

lemma t0_space_retraction_map_image:
   "retraction_map X Y r; t0_space X  t0_space Y"
  using hereditary_imp_retractive_property homeomorphic_t0_space t0_space_subtopology by blast

lemma t0_space_prod_topologyI: "t0_space X; t0_space Y  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: sing_Times_sing insert_Times_insert)


lemma t0_space_prod_topology_iff:
   "t0_space (prod_topology X Y)  prod_topology X Y = trivial_topology  t0_space X  t0_space Y" (is "?lhs=?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (metis prod_topology_trivial_iff retraction_map_fst retraction_map_snd t0_space_retraction_map_image)
qed (metis t0_space_discrete_topology t0_space_prod_topologyI)

proposition t0_space_product_topology:
   "t0_space (product_topology X I)  product_topology X I = trivial_topology  (i  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 "product_topology X I = trivial_topology")
    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  topspace (product_topology X I)"
        and y: "y  topspace (product_topology X I)"
        and "x  y"
      then obtain i where "i  I" "x i  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  U  y i  U)"
        by (metis t0_space PiE_mem i  I x i  y i topspace_product_topology x y)
      with i  I x y show "U. closedin (product_topology X I) U  (x  U) = (y  U)"
        by (rule_tac x="PiE I (λj. if j = i then U else topspace(X j))" in exI)
          (simp add: closedin_product_topology PiE_iff)
    qed
  qed
qed


subsection ‹Kolmogorov quotients›

definition Kolmogorov_quotient 
  where "Kolmogorov_quotient X  λx. @y. U. openin X U  (y  U  x  U)"

lemma Kolmogorov_quotient_in_open:
   "openin X U  (Kolmogorov_quotient X x  U  x  U)"
  by (smt (verit, ccfv_SIG) Kolmogorov_quotient_def someI_ex)

lemma Kolmogorov_quotient_in_topspace:
   "Kolmogorov_quotient X x  topspace X  x  topspace X"
  by (simp add: Kolmogorov_quotient_in_open)

lemma Kolmogorov_quotient_in_closed:
  "closedin X C  (Kolmogorov_quotient X x  C  x  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  Kolmogorov_quotient X ` U = Kolmogorov_quotient X ` topspace X  U"
  using Kolmogorov_quotient_in_open openin_subset by fastforce


lemma open_map_Kolmogorov_quotient_gen:
   "open_map (subtopology X S) (subtopology X (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  U) = Kolmogorov_quotient X ` S  U"
    using Kolmogorov_quotient_in_open [of X U] by auto
  then show "V. openin X V  Kolmogorov_quotient X ` (S  U) = Kolmogorov_quotient X ` S  V"
    using openin X U 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  Kolmogorov_quotient X ` U = Kolmogorov_quotient X ` topspace X  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 
    (U. openin X U  (x  U  y  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 
    (U. closedin X U  (x  U  y  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  topspace X"
  shows "f (Kolmogorov_quotient X x) = f x"
  using assms unfolding continuous_map_def t0_space_def
  by (smt (verit, ccfv_threshold) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace PiE 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  x  topspace X  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  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  topspace X" "t0_space Y" and f: "continuous_map (subtopology X S) Y f"
  obtains g where "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
              "x. x  S  g(Kolmogorov_quotient X x) = f x"
proof -
  have "x y. x  S; y  S; Kolmogorov_quotient X x = Kolmogorov_quotient X y  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 Pi_iff)
  then obtain g where g: "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
    "g ` (topspace X  Kolmogorov_quotient X ` S) = f ` S"
    "x. x  S  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‹Closed diagonals and graphs›

lemma Hausdorff_space_closedin_diagonal:
  "Hausdorff_space X  closedin (prod_topology X X) ((λx. (x,x)) ` topspace X)"
proof -
  have §: "((λx. (x, x)) ` topspace X)  topspace X × topspace X"
    by auto
  show ?thesis
    apply (simp add: closedin_def openin_prod_topology_alt Hausdorff_space_def disjnt_iff §)
    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) (λx. (x,x))  Hausdorff_space X"
proof -
  have "section_map X (prod_topology X X) (λ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) (λ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 proper_map_diag_eq [simp]:
   "proper_map X (prod_topology X X) (λx. (x,x))  Hausdorff_space X"
  by (simp add: closed_map_diag_eq inj_on_convol_ident injective_imp_proper_eq_closed_map)
  
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  topspace X. f x = g x}"
proof -
  have §:"{x  topspace X. f x = g x} = {x  topspace X. (f x,g x)  ((λy.(y,y)) ` topspace Y)}"
    using f continuous_map_image_subset_topspace by fastforce
  show ?thesis
    unfolding §
  proof (intro closedin_continuous_map_preimage)
    show "continuous_map X (prod_topology Y Y) (λx. (f x, g x))"
      by (simp add: continuous_map_pairedI f g)
    show "closedin (prod_topology Y Y) ((λy. (y, y)) ` topspace Y)"
      using Hausdorff_space_closedin_diagonal assms by blast
  qed
qed

lemma forall_in_closure_of:
  assumes "x  X closure_of S" "x. x  S  P x"
    and "closedin X {x  topspace X. P x}"
  shows "P x"
  by (smt (verit, ccfv_threshold) Diff_iff assms closedin_def in_closure_of mem_Collect_eq)

lemma forall_in_closure_of_eq:
  assumes x: "x  X closure_of S"
    and Y: "Hausdorff_space Y" 
    and f: "continuous_map X Y f" and g: "continuous_map X Y g"
    and fg: "x. x  S  f x = g x"
  shows "f x = g x"
proof -
  have "closedin X {x  topspace X. f x = g x}"
    using Y closedin_continuous_maps_eq f g by blast
  then show ?thesis
    using forall_in_closure_of [OF x fg]
    by fastforce
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" "xS. r x = x"
    using assms by (meson retract_of_space_def)
  then have §: "S = {x  topspace X. r x = x}"
    using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff)
  show ?thesis
    unfolding § 
    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) ((λx. (x, f x)) ` (topspace X)))
         (λx. (x, f x)) fst    continuous_map X Y f" 
   (is "?lhs=?rhs")
proof
  assume ?lhs
  then 
  have h: "homeomorphic_map X (subtopology (prod_topology X Y) ((λx. (x, f x)) ` topspace X)) (λx. (x, f x))"
    by (auto simp: homeomorphic_maps_map)
  have "f = snd  (λ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, del_insts) continuous_map_eq continuous_map_subtopology_fst embedding_map_def 
        embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.sel(1))
qed


subsection ‹ KC spaces, those where all compact sets are closed.›

definition kc_space 
  where "kc_space X  S. compactin X S  closedin X S"

lemma kc_space_euclidean: "kc_space (euclidean :: 'a::metric_space topology)"
  by (simp add: compact_imp_closed kc_space_def)
  
lemma kc_space_expansive:
   "kc_space X; topspace Y = topspace X; U. openin X U  openin Y U
       kc_space Y"
  by (meson compactin_contractive kc_space_def topology_finer_closedin)

lemma compactin_imp_closedin_gen:
   "kc_space X; compactin X S  closedin X S"
  using kc_space_def by blast

lemma Hausdorff_imp_kc_space: "Hausdorff_space X  kc_space X"
  by (simp add: compactin_imp_closedin kc_space_def)

lemma kc_imp_t1_space: "kc_space X  t1_space X"
  by (simp add: finite_imp_compactin kc_space_def t1_space_closedin_finite)

lemma kc_space_subtopology:
   "kc_space X  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  topspace X. f x  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" "x. x  topspace Y  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  topspace Y. s x  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  kc_space X  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 
         (Y. topspace Y = topspace X  (S. openin X S  openin Y S)  compact_space Y  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  topology (arbitrary union_of (finite intersection_of (λA. A = topspace X - S  openin X A)
                           relative_to (topspace X)))"
    have "topspace Y = topspace X"
      by (auto simp: Y_def)
    have "openin X T  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_inc)
    have "compact_space Y"
    proof (rule Alexander_subbase_alt)
      show "ℱ'. finite ℱ'  ℱ'  𝒞  topspace X   ℱ'" 
        if 𝒞: "𝒞  insert (topspace X - S) (Collect (openin X))" and sub: "topspace X  𝒞" for 𝒞
      proof -
        consider "𝒞  Collect (openin X)" | 𝒱 where "𝒞 = insert (topspace X - S) 𝒱" "𝒱  Collect (openin X)"
          using 𝒞 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  𝒱"
            using S sub compactin_subset_topspace by blast
          with 2 obtain  where "finite     𝒱  S  "
            using S unfolding compactin_def by (metis Ball_Collect)
          with 2 show ?thesis
            by (rule_tac x="insert (topspace X - S) " in exI) blast
        qed
      qed
    qed (auto simp: Y_def)
    have "Y = X"
      using R S. openin X S  openin Y S compact_space Y topspace Y = topspace X 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_inc)
    ultimately show "closedin X S"
      unfolding closedin_def using S compactin_subset_topspace by blast
  qed
qed

lemma continuous_imp_closed_map_gen:
   "compact_space X; kc_space Y; continuous_map X Y f  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  (K. compactin X K  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  topspace X"
      by (simp add: compactin_subset_topspace)
    moreover have "X closure_of K  K"
    proof
      fix x
      assume x: "x  X closure_of K"
      have "kc_space (subtopology X K)"
        by (simp add: R compactin X K)
      have "compactin X (insert x K)"
        by (metis K x compactin_Un compactin_sing in_closure_of insert_is_Un)
      then show "x  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)  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) (λ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)  (K. compactin X K  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  fst ` L  snd ` L"
    have "L  K × 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: compactin X K 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 L  K × K 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) 
        kc_space X 
        (K. compactin X K  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  topspace X × topspace Y"
    using compactin_subset_topspace topspace_prod_topology by blast
  moreover have "T. openin (prod_topology X Y) T  (a,b)  T  T  (topspace X × topspace Y) - K"
    if ab: "(a,b)  (topspace X × topspace Y) - K" for a b
  proof - 
    have "compactin Y {b}"
      using that by force
    moreover 
    have "compactin Y {y  topspace Y. (a,y)  K}"
    proof -
      have "compactin (prod_topology X Y) (K  {a} × 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  {a} × topspace Y)  homeomorphic_space 
                     subtopology Y {y  topspace Y. (a, y)  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  topspace Y. (a,y)  K}"
      using ab by force
    ultimately obtain V U where VU: "openin Y V" "openin Y U" "{b}  V" "{y  topspace Y. (a,y)  K}  U" "disjnt V U"
      using Hausdorff_space_compact_separation [OF Y] by blast
    define V' where "V'  topspace Y - U"
    have W: "closedin Y V'" "{y  topspace Y. (a,y)  K}  topspace Y - V'" "disjnt V (topspace Y - V')"
      using VU by (auto simp: V'_def disjnt_iff)
    with VU obtain "V  topspace Y" "V'  topspace Y"
      by (meson closedin_subset openin_closedin_eq)
    then obtain "b  V" "disjnt {y  topspace Y. (a,y)  K} V'" "V  V'"
      using VU unfolding disjnt_iff V'_def by force
    define C where "C  image fst (K  {z  topspace(prod_topology X Y). snd z  V'})"
    have "closedin (prod_topology X Y) {z  topspace (prod_topology X Y). snd z  V'}"
        using closedin_continuous_map_preimage closedin Y V' 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
    proof (intro exI conjI)
      show "openin (prod_topology X Y) ((topspace X - C) × V)"
        by (simp add: VU closedin X C openin_diff openin_prod_Times_iff)
      have "a  C"
        using VU by (auto simp: C_def V'_def)
      then show "(a, b)  (topspace X - C) × V"
        using a  C b  V that by blast
      show "(topspace X - C) × V  topspace X × topspace Y - K"
        using V  V' V  topspace Y 
        apply (simp add: C_def )
        by (smt (verit, ccfv_threshold) DiffE DiffI IntI SigmaE SigmaI image_eqI mem_Collect_eq prod.sel(1) snd_conv subset_iff)
    qed
  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:
   "Hausdorff_space X; kc_space Y  kc_space (prod_topology X Y)"
  using kc_space_prod_topology_left homeomorphic_kc_space homeomorphic_space_prod_topology_swap by blast

subsection ‹Technical results about proper maps, perfect maps, etc›

lemma compact_imp_proper_map_gen:
  assumes Y: "S. S  topspace Y; K. compactin Y K  compactin Y (S  K)
                closedin Y S"
    and fim: "f ` (topspace X)  topspace Y"
    and f: "continuous_map X Y f  kc_space X"
    and YX: "K. compactin Y K  compactin X {x  topspace X. f x  K}"
  shows "proper_map X Y f"
  unfolding proper_map_alt closed_map_def
proof (intro conjI strip)
  fix C
  assume C: "closedin X C"
  show "closedin Y (f ` C)"
  proof (intro Y)
    show "f ` C  topspace Y"
      using C closedin_subset fim by blast
    fix K
    assume K: "compactin Y K"
    define A where "A  {x  topspace X. f x  K}"
    have eq: "f ` C  K = f ` ({x  topspace X. f x  K}  C)"
      using C closedin_subset by auto
    show "compactin Y (f ` C  K)"
      unfolding eq
    proof (rule image_compactin)
      show "compactin (subtopology X A) ({x  topspace X. f x  K}  C)"
      proof (rule closedin_compact_space)
        show "compact_space (subtopology X A)"
          by (simp add: A_def K YX compact_space_subtopology)
        show "closedin (subtopology X A) ({x  topspace X. f x  K}  C)"
          using A_def C closedin_subtopology by blast
      qed
      have "continuous_map (subtopology X A) (subtopology Y K) f" if "kc_space X"
        unfolding continuous_map_closedin
      proof (intro conjI strip)
        show "f  topspace (subtopology X A)  topspace (subtopology Y K)"
          using A_def K compactin_subset_topspace by fastforce
      next
        fix C
        assume C: "closedin (subtopology Y K) C"
        show "closedin (subtopology X A) {x  topspace (subtopology X A). f x  C}"
        proof (rule compactin_imp_closedin_gen)
          show "kc_space (subtopology X A)"
            by (simp add: kc_space_subtopology that)
          have [simp]: "{x  topspace X. f x  K  f x  C} = {x  topspace X. f x  C}"
            using C closedin_imp_subset by auto
          have "compactin (subtopology Y K) C"
            by (simp add: C K closedin_compact_space compact_space_subtopology)
          then have "compactin X {x  topspace X. x  A  f x  C}"
            by (auto simp: A_def compactin_subtopology dest: YX)
          then show "compactin (subtopology X A) {x  topspace (subtopology X A). f x  C}"
            by (auto simp add: compactin_subtopology)
        qed
      qed
      with f show "continuous_map (subtopology X A) Y f"
        using continuous_map_from_subtopology continuous_map_in_subtopology by blast
    qed
  qed
qed (simp add: YX)

lemma tube_lemma_left:
  assumes W: "openin (prod_topology X Y) W" and C: "compactin X C" 
    and y: "y  topspace Y" and subW: "C × {y}  W"
  shows "U V. openin X U  openin Y V  C  U  y  V  U × V  W"
proof (cases "C = {}")
  case True
  with y show ?thesis by auto
next
  case False
  have "U V. openin X U  openin Y V  x  U  y  V  U × V  W" 
    if "x  C" for x
    using W openin_prod_topology_alt subW subsetD that by fastforce
  then obtain U V where UV: "x. x  C  openin X (U x)  openin Y (V x)  x  U x  y  V x  U x × V x  W" 
    by metis
  then obtain D where D: "finite D" "D  C" "C   (U ` D)"
    using compactinD [OF C, of "U`C"]
    by (smt (verit) UN_I finite_subset_image imageE subsetI)
  show ?thesis
  proof (intro exI conjI)
    show "openin X ( (U ` D))" "openin Y ( (V ` D))"
      using D False UV by blast+
    show "y   (V ` D)" "C   (U ` D)" "(U ` D) × (V ` D)  W"
      using D UV by force+
  qed
qed

lemma Wallace_theorem_prod_topology:
  assumes "compactin X K" "compactin Y L" 
    and W: "openin (prod_topology X Y) W" and subW: "K × L  W"
  obtains U V where "openin X U" "openin Y V" "K  U" "L  V" "U × V  W"
proof -
  have "y. y  L  U V. openin X U  openin Y V  K  U  y  V  U × V  W"
  proof (intro tube_lemma_left assms)
    fix y assume "y  L"
    show "y  topspace Y"
      using assms y  L compactin_subset_topspace by blast 
    show "K × {y}  W"
      using y  L subW by force
  qed
  then obtain U V where UV: 
         "y. y  L  openin X (U y)  openin Y (V y)  K  U y  y  V y  U y × V y  W"
    by metis
  then obtain M where "finite M" "M  L" and M: "L   (V ` M)"
    using compactin Y L unfolding compactin_def
    by (smt (verit) UN_iff finite_subset_image imageE subset_iff)
  show thesis
  proof (cases "M={}")
    case True
    with M have "L={}"
      by blast
    then show ?thesis
      using compactin X K compactin_subset_topspace that by fastforce
  next
    case False
    show ?thesis
    proof
      show "openin X ((U`M))"
        using False UV M  L finite M by blast
      show "openin Y ((V`M))"
        using UV M  L by blast
      show "K  (U`M)"
        by (meson INF_greatest UV M  L subsetD)
      show "L  (V`M)"
        by (simp add: M)
      show "(U`M) × (V`M)  W"
        using UV M  L by fastforce
    qed   
  qed
qed

lemma proper_map_prod:
   "proper_map (prod_topology X Y) (prod_topology X' Y') (λ(x,y). (f x, g y)) 
    (prod_topology X Y) = trivial_topology  proper_map X X' f  proper_map Y Y' g"
   (is "?lhs  _  ?rhs")
proof (cases "(prod_topology X Y) = trivial_topology")
  case True then show ?thesis by auto
next
  case False
  then have ne: "topspace X  {}" "topspace Y  {}"
    by auto
  define h where "h  λ(x,y). (f x, g y)"
  have "proper_map X X' f" "proper_map Y Y' g" if ?lhs
  proof -
    have cm: "closed_map X X' f" "closed_map Y Y' g"
      using that False closed_map_prod proper_imp_closed_map by blast+
    show "proper_map X X' f"
    proof (clarsimp simp add: proper_map_def cm)
      fix y
      assume y: "y  topspace X'"
      obtain z where z: "z  topspace Y"
        using ne by blast
      then have eq: "{x  topspace X. f x = y} =
                     fst ` {u  topspace X × topspace Y. h u = (y,g z)}"
        by (force simp: h_def)
      show "compactin X {x  topspace X. f x = y}"
        unfolding eq
      proof (intro image_compactin)
        have "g z  topspace Y'"
          by (meson closed_map_def closedin_subset closedin_topspace cm image_subset_iff z)
        with y show "compactin (prod_topology X Y) {u  topspace X × topspace Y. (h u) = (y, g z)}"
          using that by (simp add: h_def proper_map_def)
        show "continuous_map (prod_topology X Y) X fst"
          by (simp add: continuous_map_fst)
      qed
    qed
    show "proper_map Y Y' g"
    proof (clarsimp simp add: proper_map_def cm)
      fix y
      assume y: "y  topspace Y'"
      obtain z where z: "z  topspace X"
        using ne by blast
      then have eq: "{x  topspace Y. g x = y} =
                     snd ` {u  topspace X × topspace Y. h u = (f z,y)}"
        by (force simp: h_def)
      show "compactin Y {x  topspace Y. g x = y}"
        unfolding eq
      proof (intro image_compactin)
        have "f z  topspace X'"
          by (meson closed_map_def closedin_subset closedin_topspace cm image_subset_iff z)
        with y show "compactin (prod_topology X Y) {u  topspace X × topspace Y. (h u) = (f z, y)}"
          using that by (simp add: proper_map_def h_def)
        show "continuous_map (prod_topology X Y) Y snd"
          by (simp add: continuous_map_snd)
      qed
    qed
  qed
  moreover
  { assume R: ?rhs
    then have fgim: "f  topspace X  topspace X'" "g  topspace Y  topspace Y'" 
          and cm: "closed_map X X' f" "closed_map Y Y' g"
      by (auto simp: proper_map_def closed_map_imp_subset_topspace)
    have "closed_map (prod_topology X Y) (prod_topology X' Y') h"
      unfolding closed_map_fibre_neighbourhood imp_conjL
    proof (intro conjI strip)
      show "h  topspace (prod_topology X Y)  topspace (prod_topology X' Y')"
        unfolding h_def using fgim by auto
      fix W w
      assume W: "openin (prod_topology X Y) W"
        and w: "w  topspace (prod_topology X' Y')"
        and subW: "{x  topspace (prod_topology X Y). h x = w}  W"
      then obtain x' y' where weq: "w = (x',y')" "x'  topspace X'" "y'  topspace Y'"
        by auto
      have eq: "{u  topspace X × topspace Y. h u = (x',y')} = {x  topspace X. f x = x'} × {y  topspace Y. g y = y'}"
        by (auto simp: h_def)
      obtain U V where "openin X U" "openin Y V" "U × V  W"
        and U: "{x  topspace X. f x = x'}  U" 
        and V: "{x  topspace Y. g x = y'}  V" 
      proof (rule Wallace_theorem_prod_topology)
        show "compactin X {x  topspace X. f x = x'}" "compactin Y {x  topspace Y. g x = y'}"
          using R weq unfolding proper_map_def closed_map_fibre_neighbourhood by fastforce+
        show "{x  topspace X. f x = x'} × {x  topspace Y. g x = y'}  W"
          using weq subW by (auto simp: h_def)
      qed (use W in auto)
      obtain U' where "openin X' U'" "x'  U'" and U': "{x  topspace X. f x  U'}  U"
        using cm U openin X U weq unfolding closed_map_fibre_neighbourhood by meson
      obtain V' where "openin Y' V'" "y'  V'" and V': "{x  topspace Y. g x  V'}  V"
        using cm V openin Y V weq unfolding closed_map_fibre_neighbourhood by meson
      show "V. openin (prod_topology X' Y') V  w  V  {x  topspace (prod_topology X Y). h x  V}  W"
      proof (intro conjI exI)
        show "openin (prod_topology X' Y') (U' × V')"
          by (simp add: openin X' U' openin Y' V' openin_prod_Times_iff)
        show "w  U' × V'"
          using x'  U' y'  V' weq by blast
        show "{x  topspace (prod_topology X Y). h x  U' × V'}  W"
          using U × V  W U' V' h_def by auto
      qed
    qed
    moreover
    have "compactin (prod_topology X Y) {u  topspace X × topspace Y. h u = (w, z)}"
      if "w  topspace X'" and "z  topspace Y'" for w z
    proof -
      have eq: "{u  topspace X × topspace Y. h u = (w,z)} =
                {u  topspace X. f u = w} × {y. y  topspace Y  g y = z}"
        by (auto simp: h_def)
      show ?thesis
        using R that by (simp add: eq compactin_Times proper_map_def)
    qed
    ultimately have ?lhs
      by (auto simp: h_def proper_map_def) 
  }
  ultimately show ?thesis using False by metis
qed

lemma proper_map_paired:
  assumes "Hausdorff_space X  proper_map X Y f  proper_map X Z g 
        Hausdorff_space Y  continuous_map X Y f  proper_map X Z g 
        Hausdorff_space Z  proper_map X Y f  continuous_map X Z g"
  shows "proper_map X (prod_topology Y Z) (λx. (f x,g x))"
  using assms
proof (elim disjE conjE)
  assume §: "Hausdorff_space X" "proper_map X Y f" "proper_map X Z g"
  have eq: "(λx. (f x, g x)) = (λ(x, y). (f x, g y))  (λx. (x, x))"
    by auto
  show "proper_map X (prod_topology Y Z) (λx. (f x, g x))"
    unfolding eq
  proof (rule proper_map_compose)
    show "proper_map X (prod_topology X X) (λx. (x,x))"
      by (simp add: §)
    show "proper_map (prod_topology X X) (prod_topology Y Z) (λ(x,y). (f x, g y))"
      by (simp add: § proper_map_prod)
  qed
next
  assume §: "Hausdorff_space Y" "continuous_map X Y f" "proper_map X Z g"
  have eq: "(λx. (f x, g x)) = (λ(x,y). (x,g y))  (λx. (f x,x))"
    by auto
  show "proper_map X (prod_topology Y Z) (λx. (f x, g x))"
    unfolding eq
  proof (rule proper_map_compose)
    show "proper_map X (prod_topology Y X) (λx. (f x,x))"
      by (simp add: § proper_map_paired_continuous_map_left)
    show "proper_map (prod_topology Y X) (prod_topology Y Z) (λ(x,y). (x,g y))"
      by (simp add: § proper_map_prod proper_map_id [unfolded id_def])
  qed
next
  assume §: "Hausdorff_space Z" "proper_map X Y f" "continuous_map X Z g"
  have eq: "(λx. (f x, g x)) = (λ(x,y). (f x,y))  (λx. (x,g x))"
    by auto
  show "proper_map X (prod_topology Y Z) (λx. (f x, g x))"
    unfolding eq
  proof (rule proper_map_compose)
    show "proper_map X (prod_topology X Z) (λx. (x, g x))"
      using § proper_map_paired_continuous_map_right by auto
    show "proper_map (prod_topology X Z) (prod_topology Y Z) (λ(x,y). (f x,y))"
      by (simp add: § proper_map_prod proper_map_id [unfolded id_def])
  qed
qed

lemma proper_map_pairwise:
  assumes
    "Hausdorff_space X  proper_map X Y (fst  f)  proper_map X Z (snd  f) 
     Hausdorff_space Y  continuous_map X Y (fst  f)  proper_map X Z (snd  f) 
     Hausdorff_space Z  proper_map X Y (fst  f)  continuous_map X Z (snd  f)"
  shows "proper_map X (prod_topology Y Z) f"
  using proper_map_paired [OF assms] by (simp add: o_def)

lemma proper_map_from_composition_right:
  assumes "Hausdorff_space Y" "proper_map X Z (g  f)" and contf: "continuous_map X Y f"
    and contg: "continuous_map Y Z g"
  shows "proper_map X Y f"
proof -
  define YZ where "YZ  subtopology (prod_topology Y Z) ((λx. (x, g x)) ` topspace Y)"
  have "proper_map X Y (fst  (λx. (f x, (g  f) x)))"
  proof (rule proper_map_compose)
    have [simp]: "x  topspace X  f x  topspace Y" for x
      using contf continuous_map_preimage_topspace by auto
    show "proper_map X YZ (λx. (f x, (g  f) x))"
      unfolding YZ_def
      using assms
      by (force intro!: proper_map_into_subtopology proper_map_paired simp: o_def image_iff)+
    show "proper_map YZ Y fst"
      using contg 
      by (simp flip: homeomorphic_maps_graph add: YZ_def homeomorphic_maps_map homeomorphic_imp_proper_map)
  qed
  moreover have "fst  (λx. (f x, (g  f) x)) = f"
    by auto
  ultimately show ?thesis
    by auto
qed

lemma perfect_map_from_composition_right:
   "Hausdorff_space Y; perfect_map X Z (g  f);
     continuous_map X Y f; continuous_map Y Z g; f ` topspace X = topspace Y
     perfect_map X Y f"
  by (meson perfect_map_def proper_map_from_composition_right)

lemma perfect_map_from_composition_right_inj:
   "perfect_map X Z (g  f); f ` topspace X = topspace Y;
     continuous_map X Y f; continuous_map Y Z g; inj_on g (topspace Y)
     perfect_map X Y f"
  by (meson continuous_map_openin_preimage_eq perfect_map_def proper_map_from_composition_right_inj)


subsection ‹Regular spaces›

text ‹Regular spaces are *not* a priori assumed to be Hausdorff or $T_1$›

definition regular_space 
  where "regular_space X 
        C a. closedin X C  a  topspace X - C
                 (U V. openin X U  openin X V  a  U  C  V  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: "(x  topspace X. g(f x) = x)  (y  topspace Y. f(g y) = y)"
    using assms X homeomorphic_maps_map homeomorphic_space_def by fastforce
  show ?thesis
    unfolding regular_space_def
  proof clarify
    fix C a
    assume Y: "closedin Y C" "a  topspace Y" and "a  C"
    then obtain "closedin X (g ` C)" "g a  topspace X" "g a  g ` C"
      using closedin Y C 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  S" "g`C  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  f`S  C  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 "U V. openin Y U  openin Y V  a  U  C  V  disjnt U V"
      by metis
  qed
qed

lemma homeomorphic_regular_space:
   "X homeomorphic_space Y
         (regular_space X  regular_space Y)"
  by (meson homeomorphic_regular_space_aux homeomorphic_space_sym)

lemma regular_space:
   "regular_space X 
        (C a. closedin X C  a  topspace X - C
               (U. openin X U  a  U  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  a  topspace X - C"
  show "(V. openin X U  openin X V  a  U  C  V  disjnt U V)  
     (openin X U  a  U  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  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  regular_space X" (is "?lhs=?rhs")
proof -
  have "?lhs  (W x. openin X W  x  W 
                  (U. openin X U  (V. closedin X V  x  U  U  V  V  W)))"
    by (simp add: neighbourhood_base_of)
  also have "  (W x. closedin X W  x  topspace X - W 
                     (U. openin X U  (V. closedin X V  x  U  U  V  V  topspace X - W)))"
    by (smt (verit) Diff_Diff_Int closedin_def inf.absorb_iff2 openin_closedin_eq)
  also have "  ?rhs"
  proof -
    have §: "(V. closedin X V  x  U  U  V  V  topspace X - W) 
          (V. openin X V  x  U  W  V  disjnt U V)" (is "?lhs=?rhs")
      if "openin X U"  "closedin X W" "x  topspace X" "x  W" for W U x
    proof
      assume ?lhs with closedin X W show ?rhs
        unfolding closedin_def by (smt (verit) Diff_mono disjnt_Diff1 double_diff subset_eq)
    next
      assume ?rhs with openin X U 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 § DiffE)
  qed
  finally show ?thesis .
qed

lemma regular_space_discrete_topology [simp]:
   "regular_space (discrete_topology S)"
  using neighbourhood_base_of_closedin neighbourhood_base_of_discrete_topology by fastforce

lemma regular_space_subtopology:
 "regular_space X  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:
   "retraction_map X Y r; regular_space X  regular_space Y"
  using hereditary_imp_retractive_property homeomorphic_regular_space regular_space_subtopology by blast

lemma regular_t0_imp_Hausdorff_space:
   "regular_space X; t0_space X  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  (t0_space X  Hausdorff_space X)"
  using Hausdorff_imp_t0_space regular_t0_imp_Hausdorff_space by blast

lemma regular_t1_imp_Hausdorff_space:
   "regular_space X; t1_space X  Hausdorff_space X"
  by (simp add: regular_t0_imp_Hausdorff_space t1_imp_t0_space)

lemma regular_t1_eq_Hausdorff_space:
   "regular_space X  t1_space X  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  topspace X" and "a  S"
  then show "U V. openin X U  openin X V  a  U  S  V  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 neighbourhood_base_of_closed_Hausdorff_space:
   "regular_space X  Hausdorff_space X 
    neighbourhood_base_of (λC. closedin X C  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  kc_space X  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 "U V. openin X U  openin X V  S  U  T  V  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 "U V. x  S  openin X U  openin X V  x  U  T  V  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: "x. x  S  openin X (U x)  openin X (V x)  x  (U x)  T  (V x)  disjnt (U x) (V x)" 
    by metis
  then obtain  where "finite " "  U ` S" "S   "
    using S unfolding compactin_def by (smt (verit) UN_iff image_iff subsetI)
  then obtain K where "finite K" "K  S" and K: "S  (U ` K)"
    by (metis finite_subset_image)
  show ?thesis 
  proof (intro exI conjI)
    show "openin X ((U ` K))"
      using K  S UV by blast
    show "openin X ((V ` K))"
      using False K UV K  S finite K by blast
    show "S  (U ` K)"
      by (simp add: K)
    show "T  (V ` K)"
      using UV K  S by blast
    show "disjnt ((U ` K)) ((V ` K))"
      by (smt (verit) Inter_iff UN_E UV K  S disjnt_iff image_eqI subset_iff)
  qed
qed

lemma regular_space_compact_closed_sets:
   "regular_space X 
        (S T. compactin X S  closedin X T  disjnt S T
            (U V. openin X U  openin X V  S  U  T  V  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  topspace X" and "x  S"
    then obtain U V where "openin X U  openin X V  {x}  U  S  V  disjnt U V"
      by (metis R compactin_sing disjnt_empty1 disjnt_insert1)
    then show "U. openin X U  x  U  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) 
        X = trivial_topology  Y = trivial_topology  regular_space X  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 "X = trivial_topology  Y = trivial_topology")
    case True then show ?thesis by auto
  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)  W"
      then obtain U V where U: "openin X U" "x  U" and V: "openin Y V" "y  V" 
        and "U × V  W"
        by (metis openin_prod_topology_alt)
      obtain D1 C1 where 1: "openin X D1" "closedin X C1" "x  D1" "D1  C1" "C1  U"
        by (metis regular_space X U neighbourhood_base_of neighbourhood_base_of_closedin)
      obtain D2 C2 where 2: "openin Y D2" "closedin Y C2" "y  D2" "D2  C2" "C2  V"
        by (metis regular_space Y V neighbourhood_base_of neighbourhood_base_of_closedin)
      show "U V. openin (prod_topology X Y) U  closedin (prod_topology X Y) V 
                  (x,y)  U  U  V  V  W"
      proof (intro conjI exI)
        show "openin (prod_topology X Y) (D1 × D2)"
          by (simp add: 1 2 openin_prod_Times_iff)
        show "closedin (prod_topology X Y) (C1 × C2)"
          by (simp add: 1 2 closedin_prod_Times_iff)
      qed (use 1 2 U × V  W in auto)
    qed
  qed
qed

lemma regular_space_product_topology:
   "regular_space (product_topology X I) 
    (product_topology X I) = trivial_topology  (i  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 "product_topology X I = trivial_topology")
    case True
    then show ?thesis
      by auto
  next
    case False
    then obtain x where x: "x  topspace (product_topology X I)"
      by (meson ex_in_conv null_topspace_iff_trivial)
    define  where "  {PiE I U |U. finite {i  I. U i  topspace (X i)}
                         (iI. openin (X i) (U i))}"
    have oo: "openin (product_topology X I) = arbitrary union_of (λW. W  )"
      by (simp add: ℱ_def openin_product_topology product_topology_base_alt)
    have "U V. openin (product_topology X I) U  closedin (product_topology X I) V  x  U  U  V  V  PiE I W"
      if fin: "finite {i  I. W i  topspace (X i)}" 
        and opeW: "k. k  I  openin (X k) (W k)" and x: "x  PiE I W" for W x
    proof -
      have "i. i  I  U V. openin (X i) U  closedin (X i) V  x i  U  U  V  V  W i"
        by (metis False PiE_iff R neighbourhood_base_of neighbourhood_base_of_closedin opeW x)
      then obtain U C where UC: 
        "i. i  I  openin (X i) (U i)  closedin (X i) (C i)  x i  U i  U i  C i  C i  W i"
        by metis
      define PI where "PI  λV. PiE I (λi. if W i = topspace(X i) then topspace(X i) else V i)"
      show ?thesis
      proof (intro conjI exI)
        have "iI. W i  topspace (X i)  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  PI U"
          using UC x by (fastforce simp: PI_def)
        show "PI U  PI C"
          by (smt (verit) UC Orderings.order_eq_iff PiE_mono PI_def)
        show "PI C  PiE 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: ℱ_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: "y. y  topspace X  closedin Z {x  topspace Z. f x = y}"
    and contg: "continuous_map Z Y g"
  shows "closed_map Z (prod_topology X Y) (λx. (f x, g x))"
  unfolding closed_map_def
proof (intro strip)
  fix C assume "closedin Z C"
  then have "C  topspace Z"
    by (simp add: closedin_subset)
  have "f  topspace Z  topspace X" "g  topspace Z  topspace Y"
    by (simp_all add: assms closed_map_imp_subset_topspace)
  show "closedin (prod_topology X Y) ((λx. (f x, g x)) ` C)"
    unfolding closedin_def topspace_prod_topology
  proof (intro conjI)
    have "closedin Y (g ` C)"
      using closedin Z C assms(3) closed_map_def by blast
    with assms show "(λx. (f x, g x)) ` C  topspace X × topspace Y"
      by (smt (verit) SigmaI closedin Z C closed_map_def closedin_subset image_subset_iff)
    have *: "T. openin (prod_topology X Y) T  (y1,y2)  T  T  topspace X × topspace Y - (λx. (f x, g x)) ` C"
      if "(y1,y2)  (λx. (f x, g x)) ` C" and y1: "y1  topspace X" and y2: "y2  topspace Y"
      for y1 y2
    proof -
      define A where "A  topspace Z - (C  {x  topspace Z. f x = y1})"
      have A: "openin Z A" "{x  topspace Z. g x = y2}  A"
        using that closedin Z C clo that(2) by (auto simp: A_def)
      obtain V0 where "openin Y V0  y2  V0" and UA: "{x  topspace Z. g x  V0}  A"
        using g A y2 unfolding closed_map_fibre_neighbourhood by blast
      then obtain V V' where VV: "openin Y V  closedin Y V'  y2  V  V  V'" and "V'  V0"
        by (metis (no_types, lifting) regular_space Y neighbourhood_base_of neighbourhood_base_of_closedin)
      with UA have subA: "{x  topspace Z. g x  V'}  A"
        by blast
      show ?thesis
      proof -
        define B where "B  topspace Z - (C  {x  topspace Z. g x  V'})"
        have "openin Z B"
          using VV closedin Z C contg by (fastforce simp: B_def continuous_map_closedin)
        have "{x  topspace Z. f x = y1}  B"
          using A_def subA by (auto simp: A_def B_def)
        then obtain U where "openin X U" "y1  U" and subB: "{x  topspace Z. f x  U}  B"
          using openin Z B y1 f unfolding closed_map_fibre_neighbourhood by meson
        show ?thesis
        proof (intro conjI exI)
          show "openin (prod_topology X Y) (U × V)"
            by (metis VV openin X U openin_prod_Times_iff)
          show "(y1, y2)  U × V"
            by (simp add: VV y1  U)
          show "U × V  topspace X × topspace Y - (λx. (f x, g x)) ` C"
            using VV C  topspace Z openin X U 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 × topspace Y - (λ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  continuous_map Z X f  (z  topspace Y. closedin Z {x  topspace Z. g x = z})
          regular_space Y  continuous_map Z Y g  (y  topspace X. closedin Z {x  topspace Z. f x = y}))"
         (is "?RSX  ?RSY")
       shows "closed_map Z (prod_topology X Y) (λx. (f x, g x))"
  using D
proof
  assume RSX: ?RSX
  have eq: "(λx. (f x, g x)) = (λ(x,y). (y,x))  (λx. (g x, f x))"
    by auto
  show ?thesis
    unfolding eq
  proof (rule closed_map_compose)
    show "closed_map Z (prod_topology Y X) (λ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) (λ(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  regular_space Y  regular_space X  t1_space Y"
  shows "closed_map Z (prod_topology X Y) (λx. (f x, g x))"
proof (rule closed_map_paired_gen)
  show "regular_space X  continuous_map Z X f  (ztopspace Y. closedin Z {x  topspace Z. g x = z})  regular_space Y  continuous_map Z Y g  (ytopspace X. closedin Z {x  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  f)" "continuous_map Z X (fst  f)"
    "closed_map Z Y (snd  f)" "continuous_map Z Y (snd  f)"
    "t1_space X  regular_space Y  regular_space X  t1_space Y"
  shows "closed_map Z (prod_topology X Y) f"
proof -
  have "closed_map Z (prod_topology X Y) (λa. ((fst  f) a, (snd  f) a))"
    using assms closed_map_paired by blast
  then show ?thesis
    by auto
qed

lemma continuous_imp_proper_map:
   "compact_space X; kc_space Y; continuous_map X Y f  proper_map X Y f"
  by (simp add: continuous_closed_imp_proper_map continuous_imp_closed_map_gen kc_imp_t1_space)


lemma tube_lemma_right:
  assumes W: "openin (prod_topology X Y) W" and C: "compactin Y C" 
    and x: "x  topspace X" and subW: "{x} × C  W"
  shows "U V. openin X U  openin Y V  x  U  C  V  U × V  W"
proof (cases "C = {}")
  case True
  with x show ?thesis by auto
next
  case False
  have "U V. openin X U  openin Y V  x  U  y  V  U × V  W" 
    if "y  C" for y
    using W openin_prod_topology_alt subW subsetD that by fastforce
  then obtain U V where UV: "y. y  C  openin X (U y)  openin Y (V y)  x  U y  y  V y  U y × V y  W" 
    by metis
  then obtain D where D: "finite D" "D  C" "C   (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 ( (U ` D))" "openin Y ( (V ` D))"
      using D False UV by blast+
    show "x   (U ` D)" "C   (V ` D)" " (U ` D) ×  (V ` D)  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  topspace X × topspace Y. fst x  U} = U × topspace Y"
    if "U  topspace X" for U
    using that by force
  have **: "U y. openin (prod_topology X Y) U; y  topspace X;
            {x  topspace X × topspace Y. fst x = y}  U
            V. openin X V  y  V  V × topspace Y  U"
    using tube_lemma_right[of X Y _ "topspace Y"] assms by (fastforce simp: compact_space_def)
  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:
   "closed_map X Y f; regular_space X;
     y. y  topspace Y  closedin X {x  topspace X. f x = y}
     closed_map X (prod_topology X Y) (λ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"
    "y. y  topspace Y  closedin X {x  topspace X. f x = y}"
  shows "closed_map X (prod_topology Y X) (λx. (f x, x))"
proof -
  have eq: "(λx. (f x, x)) = (λ(x,y). (y,x))  (λx. (x, f x))"
    by auto
  show ?thesis
    unfolding eq
  proof (rule closed_map_compose)
    show "closed_map X (prod_topology X Y) (λ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) (λ(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"
          "y. y  topspace Y  closedin X {x  topspace X. f x = y}"
  shows "closedin (prod_topology X Y) ((λ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"
    "y. y  topspace Y  closedin X {x  topspace X. f x = y}"
  shows "proper_map X (prod_topology X Y) (λ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"
    "y. y  topspace Y  closedin X {x  topspace X. f x = y}"
  shows "proper_map X (prod_topology Y X) (λ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  topspace Y" and "y  C"
  have "closed_map X Y f" "(y  topspace Y. compactin X {x  topspace X. f x = y})"
    using pmapf proper_map_def by force+
  moreover have "closedin X {z  topspace X. f z  C}"
    using closedin Y C contf continuous_map_closedin by fastforce
  moreover have "disjnt {z  topspace X. f z = y} {z  topspace X. f z  C}"
    using y  C disjnt_iff by blast
  ultimately
  obtain U V where UV: "openin X U" "openin X V" "{z  topspace X. f z = y}  U" "{z  topspace X. f z  C}  V"
                  and dUV: "disjnt U V"
    using y  topspace Y regular_space X unfolding regular_space_compact_closed_sets
    by meson

  have *: "U T. openin X U  T  topspace Y  {x  topspace X. f x  T}  U 
         (V. openin Y V  T  V  {x  topspace X. f x  V}  U)"
   using closed_map X Y f unfolding closed_map_preimage_neighbourhood by blast
  obtain V1 where V1: "openin Y V1  y  V1" and sub1: "{x  topspace X. f x  V1}  U"
    using * [of U "{y}"] UV y  topspace Y by auto
  moreover
  obtain V2 where "openin Y V2  C  V2" and sub2: "{x  topspace X. f x  V2}  V"
    by (smt (verit, ccfv_SIG) * UV closedin Y C closedin_subset mem_Collect_eq subset_iff)
  moreover have "disjnt V1 V2"
  proof -
    have "x. x. x  U  x  V; x  V1; x  V2  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 "U V. openin Y U  openin Y V  y  U  C  V  disjnt U V"
    by meson
qed

lemma regular_space_perfect_map_image:
   "regular_space X; perfect_map X Y f  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  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: "(y  topspace Y. compactin X {x  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  topspace X" and "x  C"
    obtain U1 U2 where "openin X U1" "openin X U2" "{x}  U1" and "disjnt U1 U2"
      and subV: "C  {z  topspace X. f z = f x}  U2"
    proof (rule Hausdorff_space_compact_separation [of X "{x}" "C  {z  topspace X. f z = f x}", OF Hausdorff_space X])
      show "compactin X {x}"
        by (simp add: x  topspace X)
      show "compactin X (C  {z  topspace X. f z = f x})"
        using closedin X C fim x  topspace X closed_Int_compactin preYf by fastforce
      show "disjnt {x} (C  {z  topspace X. f z = f x})"
        using x  C by force
    qed
    have "closedin Y (f ` (C - U2))"
      using closed_map X Y f closedin X C openin X U2 closed_map_def by blast
    moreover
    have "f x  topspace Y - f ` (C - U2)"
      using closedin X C continuous_map X Y f x  topspace X closedin_subset continuous_map_def subV 
      by (fastforce simp: Pi_iff)
    ultimately
    obtain V1 V2 where VV: "openin Y V1" "openin Y V2" "f x  V1" 
                and subV2: "f ` (C - U2)  V2" and "disjnt V1 V2"
      by (meson R regular_space_def)
    show "U U'. openin X U  openin X U'  x  U  C  U'  disjnt U U'"
    proof (intro exI conjI)
      show "openin X (U1  {x  topspace X. f x  V1})"
        using VV(1) continuous_map X Y f openin X U1 continuous_map by fastforce
      show "openin X (U2  {x  topspace X. f x  V2})"
        using VV(2) continuous_map X Y f openin X U2 continuous_map by fastforce
      show "x  U1  {x  topspace X. f x  V1}"
        using VV(3) x  topspace X {x}  U1 by auto
      show "C  U2  {x  topspace X. f x  V2}"
        using closedin X C closedin_subset subV2 by auto
      show "disjnt (U1  {x  topspace X. f x  V1}) (U2  {x  topspace X. f x  V2})"
        using disjnt U1 U2 disjnt V1 V2 by (auto simp: disjnt_iff)
    qed
  qed
qed


subsection‹Locally compact spaces›

definition locally_compact_space 
  where "locally_compact_space X 
    x  topspace X. U K. openin X U  compactin X K  x  U  U  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 "V K. openin Y V  compactin Y K  f x  V  V  K"
    if "x  topspace X" "openin X U" "compactin X K" "x  U" "U  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  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" "xT. 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  topspace X" "x  T"
    obtain U K where UK: "openin X U  compactin X K  x  U  U  K"
      by (meson X x  topspace X locally_compact_space_def)
    then have "compactin (subtopology X T) (r ` K)  T  U  r ` K"
      by (smt (verit) IntD1 image_compactin image_iff inf_le2 r subset_iff)
    then show "U. openin X U  (K. compactin (subtopology X T) K  x  U  T  U  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  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  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  W"
  then obtain U K where "openin X U" "compactin X K" "x  U" "U  K"
    by (metis loc locally_compact_space_def openin_subset subsetD)
  moreover have "openin X (U  W)  x  U  W"
    using openin X W x  W openin X U x  U by blast
  then have "u' v. openin X u'  closedin X v  x  u'  u'  v  v  U  v  W"
    using reg
    by (metis le_infE neighbourhood_base_of neighbourhood_base_of_closedin)
  then show "U V. openin X U  compactin X V  x  U  U  V  V  W"
    by (meson U  K compactin X K closed_compactin subset_trans)
qed

lemma Hausdorff_regular: "Hausdorff_space X; neighbourhood_base_of (compactin X) X  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  W"
  then have "x  topspace X"
    using openin_subset by blast 
  then obtain U K where "openin X U" "compactin X K" and UK: "x  U" "U  K"
    by (meson loc locally_compact_space_def)
  with Hausdorff_space X have "regular_space (subtopology X K)"
    using Hausdorff_space_subtopology compact_Hausdorff_imp_regular_space compact_space_subtopology by blast
  then have "U' V'. openin (subtopology X K) U'  closedin (subtopology X K) V'  x  U'  U'  V'  V'  K  W"
    unfolding neighbourhood_base_of_closedin [symmetric] neighbourhood_base_of
    by (meson IntI U  K openin X W x  U x  W openin_subtopology_Int2 subsetD)
  then obtain V C where "openin X V" "closedin X C" and VC: "x  K  V" "K  V  K  C" "K  C  K  W"
    by (metis Int_commute closedin_subtopology openin_subtopology)
  show "U V. openin X U  closedin X V  x  U  U  V  V  W"
  proof (intro conjI exI)
    show "openin X (U  V)"
      using openin X U openin X V by blast
    show "closedin X (K  C)"
      using closedin X C compactin X K compactin_imp_closedin Hausdorff_space X by blast
  qed (use UK VC in auto)
qed

lemma locally_compact_space_neighbourhood_base:
  "Hausdorff_space X  regular_space X
         locally_compact_space X  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  (Hausdorff_space X  regular_space X)  locally_compact_space X  regular_space X"
  using locally_compact_Hausdorff_imp_regular_space by blast

lemma locally_compact_space_compact_closedin:
  assumes  "Hausdorff_space X  regular_space X"
  shows "locally_compact_space X 
         (x  topspace X. U K. openin X U  compactin X K  closedin X K  x  U  U  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  regular_space X"
  shows "locally_compact_space X 
         (x  topspace X. U. openin X U  compactin X (X closure_of U)  x  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  regular_space X"
  shows "locally_compact_space X  neighbourhood_base_of (λC. compactin X C  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 regular_space X 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  regular_space X"
  shows "locally_compact_space X  neighbourhood_base_of (λ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 (λA. compactin X A  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  regular_space X"
  shows "locally_compact_space X  
             neighbourhood_base_of (λU. openin X U  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 (λ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  regular_space X"
  shows "locally_compact_space X 
         (K. compactin X K
               (U L. openin X U  compactin X L  closedin X L  K  U  U  L))"
         (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  then obtain U L where UL: "x  topspace X. openin X (U x)  compactin X (L x)  closedin X (L x)  x  U x  U x  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  topspace X"
      by (simp add: compactin_subset_topspace)
    then have *: "(UU ` K. openin X U)  K   (U ` K)"
      using UL by blast
    with compactin X K obtain KF where KF: "finite KF" "KF  K" "K  (U ` KF)"
      by (metis compactinD finite_subset_image)
    show "U L. openin X U  compactin X L  closedin X L  K  U  U  L"
    proof (intro conjI exI)
      show "openin X ( (U ` KF))"
        using "*" KF  K by fastforce
      show "compactin X ( (L ` KF))"
        by (smt (verit) UL K  topspace X KF compactin_Union finite_imageI imageE subset_iff)
      show "closedin X ( (L ` KF))"
        by (smt (verit) UL K  topspace X KF closedin_Union finite_imageI imageE subsetD)
    qed (use UL K  topspace X 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  regular_space X 
        neighbourhood_base_of (λC. compactin X C  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  kc_space X 
        locally_compact_space X  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  kc_space X 
        locally_compact_space X  Hausdorff_space X  regular_space X"
  using Hausdorff_regular locally_compact_kc_space by blast

lemma locally_compact_kc_imp_regular_space:
   "neighbourhood_base_of (compactin X) X; kc_space X  regular_space X"
  using Hausdorff_regular locally_compact_imp_kc_eq_Hausdorff_space by blast

lemma kc_locally_compact_space:
   "kc_space X
     neighbourhood_base_of (compactin X) X  locally_compact_space X  Hausdorff_space X  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  topspace X" "x  S"
  then obtain U K where UK: "openin X U  compactin X K  x  U  U  K"
    by (meson loc locally_compact_space_def)
  show "U. openin (subtopology X S) U  
            (K. compactin (subtopology X S) K  x  U  U  K)"
  proof (intro conjI exI)
    show "openin (subtopology X S) (S  U)"
      by (simp add: UK openin_subtopology_Int2)
    show "compactin (subtopology X S) (S  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 X: "Hausdorff_space X  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  topspace X" "x  S"
  then obtain U K where UK: "openin X U" "compactin X K" "x  U" "U  K"
    by (meson loc locally_compact_space_def)
  moreover have reg: "regular_space X"
    using X loc locally_compact_Hausdorff_imp_regular_space by blast
  moreover have "openin X (U  S)"
    by (simp add: UK openin X S openin_Int)
  ultimately obtain V C 
      where VC: "openin X V" "closedin X C" "x  V" "V  C" "C  U" "C  S"
    by (metis x  S IntI le_inf_iff neighbourhood_base_of neighbourhood_base_of_closedin)
  show "U. openin (subtopology X S) U  
            (K. compactin (subtopology X S) K  x  U  U  K)"
  proof (intro conjI exI)
    show "openin (subtopology X S) V"
      using VC by (meson openin X S openin_open_subtopology order_trans)
    show "compactin (subtopology X S) (C  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:
  "continuous_map X X' f; open_map X X' f;
    f ` topspace X = topspace X'; locally_compact_space X  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  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  S"
  then obtain T K where *: "openin X T" "compactin X K" "K  S" "a  S" "a  T" "S  T  K"
    using loc unfolding locally_compact_space_def
  by (metis IntE S compactin_subtopology inf_commute openin_subtopology topspace_subtopology_subset)
  have "T  X closure_of S  X closure_of (T  S)"
    by (simp add: "*"(1) openin_Int_closure_of_subset)
  also have "...  S"
    using * Hausdorff_space X by (metis closure_of_minimal compactin_imp_closedin order.trans inf_commute)
  finally have "T  X closure_of S  T  S" by simp 
  then have "openin (subtopology X (X closure_of S)) (T  S)"
    unfolding openin_subtopology using openin X T S closure_of_subset by fastforce
  with * show "T. openin (subtopology X (X closure_of S)) T  a  T  T  S"
    by blast
qed

lemma locally_compact_subspace_closed_Int_openin:
   "Hausdorff_space X  S  topspace X  locally_compact_space(subtopology X S)
         C U. closedin X C  openin X U  C  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  S  topspace X  locally_compact_space(subtopology X S)" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  then obtain "S  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 "(C U. closedin X C  openin X U  C  U = S)  S  topspace X  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  U"
    by blast
  then have "C  topspace X"
    by (simp add: closedin_subset)
  have "locally_compact_space (subtopology (subtopology X C) (topspace (subtopology X C)  U))"
  proof (rule locally_compact_space_open_subset)
    show "locally_compact_space (subtopology X C)"
      by (simp add: closedin X C loc locally_compact_space_closed_subset)
    show "openin (subtopology X C) (topspace (subtopology X C)  U)"
      by (simp add: openin X U Int_left_commute inf_commute openin_Int openin_subtopology_Int2)
  qed (simp add: Hausdorff_space_subtopology Hausdorff_space X)
  then show ?rhs
    by (metis Seq C  topspace X 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:
   "Hausdorff_space X; S  topspace X; X closure_of S = topspace X;
     locally_compact_space (subtopology X S)  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) 
        (prod_topology X Y) = trivial_topology 
        locally_compact_space X  locally_compact_space Y" (is "?lhs=?rhs")
proof (cases "(prod_topology X Y) = trivial_topology")
  case True
  then show ?thesis
    using locally_compact_space_discrete_topology by force
next
  case False
  then obtain w z where wz: "w  topspace X" "z  topspace Y"
    by fastforce
  show ?thesis 
  proof
    assume L: ?lhs then show ?rhs
      by (metis locally_compact_space_retraction_map_image prod_topology_trivial_iff retraction_map_fst retraction_map_snd)
  next
    assume R: ?rhs 
    show ?lhs
      unfolding locally_compact_space_def
    proof clarsimp
      fix x y
      assume "x  topspace X" and "y  topspace Y"
      obtain U C where "openin X U" "compactin X C" "x  U" "U  C"
        by (meson False R x  topspace X locally_compact_space_def)
      obtain V D where "openin Y V" "compactin Y D" "y  V" "V  D"
        by (meson False R y  topspace Y locally_compact_space_def)
      show "U. openin (prod_topology X Y) U  (K. compactin (prod_topology X Y) K  (x, y)  U  U  K)"
      proof (intro exI conjI)
        show "openin (prod_topology X Y) (U × V)"
          by (simp add: openin X U openin Y V openin_prod_Times_iff)
        show "compactin (prod_topology X Y) (C × D)"
          by (simp add: compactin X C compactin Y D compactin_Times)
        show "(x, y)  U × V"
          by (simp add: x  U y  V)
        show "U × V  C × D"
          by (simp add: Sigma_mono U  C V  D)
      qed
    qed
  qed
qed

lemma locally_compact_space_product_topology:
   "locally_compact_space(product_topology X I) 
        product_topology X I = trivial_topology 
        finite {i  I. ¬ compact_space(X i)}  (i  I. locally_compact_space(X i))" (is "?lhs=?rhs")
proof (cases "(product_topology X I) = trivial_topology")
  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  topspace (product_topology X I)"
      using False
      by (meson ex_in_conv null_topspace_iff_trivial)
    with L z obtain U C where "openin (product_topology X I) U" "compactin (product_topology X I) C" "z  U" "U  C"
      by (meson locally_compact_space_def)
    then obtain V where finV: "finite {i  I. V i  topspace (X i)}" and "i  I. openin (X i) (V i)" 
                    and "z  PiE I V" "PiE I V  U"
      by (auto simp: openin_product_topology_alt)
    have "compact_space (X i)" if "i  I" "V i = topspace (X i)" for i
    proof -
      have "compactin (X i) ((λx. x i) ` C)"
        using compactin (product_topology X I) C image_compactin
        by (metis continuous_map_product_projection i  I)
      moreover have "V i  (λx. x i) ` C"
      proof -
        have "V i  (λx. x i) ` PiE I V"
          by (metis z  PiE I V empty_iff image_projection_PiE order_refl i  I)
        also have "  (λx. x i) ` C"
          using U  C PiE I V  U 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  I. ¬ compact_space (X i)}"
      by (metis (mono_tags, lifting) mem_Collect_eq finite_subset subsetI)
    moreover have "locally_compact_space (X i)" if "i  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  (ΠE iI. topspace (X i))"
      have "U C. openin (X i) U  compactin (X i) C  z i  U  U  C 
                    (compact_space(X i)  U = topspace(X i)  C = topspace(X i))" 
        if "i  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: "i. i  I  
             openin (X i) (U i)  compactin (X i) (C i)  z i  U i  U i  C i 
                    (compact_space(X i)  U i = topspace(X i)  C i = topspace(X i))"
        by metis
      show "U. openin (product_topology X I) U  (K. compactin (product_topology X I) K  z  U  U  K)"
      proof (intro exI conjI)
        show "openin (product_topology X I) (PiE 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) (PiE 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)  (i  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  I" and y: "y  topspace (X i)"
    then obtain U K where UK: "openin (X i) U" "compactin (X i) K" "y  U" "U  K"
      using R by (fastforce simp: locally_compact_space_def)
    then show "U. openin (sum_topology X I) U  (K. compactin (sum_topology X I) K  (i, y)  U  U  K)"
      by (metis i  I continuous_map_component_injection image_compactin image_mono 
          imageI open_map_component_injection open_map_def)
  qed
qed

lemma locally_compact_space_euclidean:
  "locally_compact_space (euclidean::'a::heine_borel topology)" 
  unfolding locally_compact_space_def
proof (intro strip)
  fix x::'a
  assume "x  topspace euclidean"
  have "ball x 1  cball x 1"
    by auto
  then show "U K. openin euclidean U  compactin euclidean K  x  U  U  K"
    by (metis Elementary_Metric_Spaces.open_ball centre_in_ball compact_cball compactin_euclidean_iff open_openin zero_less_one)
qed

lemma locally_compact_Euclidean_space:
  "locally_compact_space(Euclidean_space n)"
  using homeomorphic_locally_compact_space [OF homeomorphic_Euclidean_space_product_topology] 
  using locally_compact_space_product_topology locally_compact_space_euclidean by fastforce

proposition quotient_map_prod_right:
  assumes loc: "locally_compact_space Z" 
    and reg: "Hausdorff_space Z  regular_space Z" 
    and f: "quotient_map X Y f"
  shows "quotient_map (prod_topology Z X) (prod_topology Z Y) (λ(x,y). (x,f y))"
proof -
  define h where "h  (λ(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  topspace Z × topspace X. h u  W}
    openin (prod_topology Z Y) W"   (is "?lhs=?rhs")
    if W: "W  topspace Z × topspace Y" for W
  proof
    define S where "S  {u  topspace Z × topspace X. h u  W}"
    assume ?lhs 
    then have L: "openin (prod_topology Z X) S"
      using S_def by blast
    have "T. openin (prod_topology Z Y) T  (x0, z0)  T  T  W"
      if §: "(x0,z0)  W" for x0 z0 
    proof -
      have x0: "x0  topspace Z"
        using W that by blast
      obtain y0 where y0: "y0  topspace X" "f y0 = z0"
        by (metis W fim imageE insert_absorb insert_subset mem_Sigma_iff §)
      then have "(x0, y0)  S"
        by (simp add: S_def h_def that x0)
      have "continuous_map Z (prod_topology Z X) (λx. (x, y0))"
        by (simp add: continuous_map_paired y0)
      with openin_continuous_map_preimage [OF _ L] 
      have ope_ZS: "openin Z {x  topspace Z. (x,y0)  S}"
        by blast
      obtain U U' where "openin Z U" "compactin Z U'" "closedin Z U'" 
        "x0  U"  "U  U'" "U'  {x  topspace Z. (x,y0)  S}"
        using loc ope_ZS x0 (x0, y0)  S
        by (force simp: locally_compact_space_neighbourhood_base_closedin [OF reg] 
            neighbourhood_base_of)
      then have D: "U' × {y0}  S"
        by (auto simp: )
      define V where "V  {z  topspace Y. U' × {y  topspace X. f y = z}  S}"
      have "z0  V"
        using D y0 Int_Collect fim by (fastforce simp: h_def V_def S_def)
      have "openin X {x  topspace X. f x  V}  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  topspace X. f x  V}"
      proof -
        let ?Z = "subtopology Z U'"
        have *: "{x  topspace X. f x  V} = topspace X - snd ` (U' × topspace X - S)"
          by (force simp: V_def S_def h_def simp flip: fim)
        have "compact_space ?Z"
          using compactin Z U' compactin_subspace by auto
        moreover have "closedin (prod_topology ?Z X) (U' × topspace X - S)"
          by (simp add: L closedin Z U' 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 × V)"
          by (simp add: openin_prod_Times_iff openin Z U openin Y V)
        show "(x0, z0)  U × V"
          by (simp add: x0  U z0  V)
        show "U × V  W"
          using U  U' 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  regular_space Z" 
    and f: "quotient_map X Y f"
  shows "quotient_map (prod_topology X Z) (prod_topology Y Z) (λ(x,y). (f x,y))"
proof -
  have "(λ(x,y). (f x,y)) = prod.swap  (λ(x,y). (x,f y))  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) (λ(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  topspace X"
  then obtain U K where "openin X' U" "compactin X' K" "f x  U" "U  K"
    using assms unfolding locally_compact_space_def perfect_map_def
    by (metis (no_types, lifting) continuous_map_closedin Pi_iff)
  show "U K. openin X U  compactin X K  x  U  U  K"
  proof (intro exI conjI)
    have "continuous_map X X' f"
      using f perfect_map_def by blast
    then show "openin X {x  topspace X. f x  U}"
      by (simp add: openin X' U continuous_map)
    show "compactin X {x  topspace X. f x  K}"
      using compactin X' K f perfect_imp_proper_map proper_map_alt by blast
  qed (use x f x  U U  K in auto)
qed


subsection‹Special characterizations of classes of functions into and out of R›

lemma monotone_map_into_euclideanreal_alt:
  assumes "continuous_map X euclideanreal f" 
  shows "(k. is_interval k  connectedin X {x  topspace X. f x  k}) 
         connected_space X  monotone_map X euclideanreal f"  (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
  proof
    show "connected_space X"
      using L connected_space_subconnected by blast
    have "connectedin X {x  topspace X. f x  {y}}" for y
      by (metis L is_interval_1 nle_le singletonD)
    then show "monotone_map X euclideanreal f"
      by (simp add: monotone_map)
  qed
next
  assume R: ?rhs 
  then
  have *: False 
      if "a < b" "closedin X U" "closedin X V" "U  {}" "V  {}" "disjnt U V"
         and UV: "{x  topspace X. f x  {a..b}} = U  V" 
         and dis: "disjnt U {x  topspace X. f x = b}" "disjnt V {x  topspace X. f x = a}" 
       for a b U V
  proof -
    define E1 where "E1  U  {x  topspace X. f x  {c. c  a}}"
    define E2 where "E2  V  {x  topspace X. f x  {c. b  c}}"
    have "closedin X {x  topspace X. f x  a}" "closedin X {x  topspace X. b  f x}"
      using assms continuous_map_upper_lower_semicontinuous_le by blast+
    then have "closedin X E1" "closedin X E2"
      unfolding E1_def E2_def using that by auto
    moreover
    have "E1  E2 = {}"
      unfolding E1_def E2_def using a<b disjnt U V dis UV
      by (simp add: disjnt_def set_eq_iff) (smt (verit))
    have "topspace X  E1  E2"
      unfolding E1_def E2_def using UV by fastforce
    have "E1 = {}  E2 = {}"
      using R connected_space_closedin
      using E1  E2 = {} closedin X E1 closedin X E2 topspace X  E1  E2 by blast
    then show False
      using E1_def E2_def U  {} V  {} by fastforce
  qed
  show ?lhs
  proof (intro strip)
    fix K :: "real set"
    assume "is_interval K"
    have False
      if "a  K" "b  K" and clo: "closedin X U" "closedin X V" 
         and UV: "{x. x  topspace X  f x  K}  U  V"
                 "U  V  {x. x  topspace X  f x  K} = {}" 
         and nondis: "¬ disjnt U {x. x  topspace X  f x = a}"
                     "¬ disjnt V {x. x  topspace X  f x = b}" 
     for a b U V
    proof -
      have "y. connectedin X {x. x  topspace X  f x = y}"
        using R monotone_map by fastforce
      then have **: False if "p  U  q  V  f p = f q  f q  K" for p q
        unfolding connectedin_closedin
        using a  K b  K UV clo that 
        by (smt (verit, ccfv_threshold) closedin_subset disjoint_iff mem_Collect_eq subset_iff)
      consider "a < b" | "a = b" | "b < a"
        by linarith
      then show ?thesis
      proof cases
        case 1
        define W where "W  {x  topspace X. f x  {a..b}}"
        have "closedin X W"
          unfolding W_def
          by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin continuous_map_closedin)
        show ?thesis
        proof (rule * [OF 1 , of "U  W" "V  W"])
          show "closedin X (U  W)" "closedin X (V  W)"
            using closedin X W clo by auto
          show "U  W  {}" "V  W  {}"
            using nondis 1 by (auto simp: disjnt_iff W_def)
          show "disjnt (U  W) (V  W)"
            using is_interval K unfolding is_interval_1 disjnt_iff W_def
            by (metis (mono_tags, lifting) a  K b  K ** Int_Collect atLeastAtMost_iff)
          have "x. x  topspace X; a  f x; f x  b  x  U  x  V"
            using a  K b  K is_interval K UV unfolding is_interval_1 disjnt_iff
            by blast
          then show "{x  topspace X. f x  {a..b}} = U  W  V  W"
            by (auto simp: W_def)
          show "disjnt (U  W) {x  topspace X. f x = b}" "disjnt (V  W) {x  topspace X. f x = a}"
            using ** a  K b  K nondis by (force simp: disjnt_iff)+
        qed
      next
        case 2
        then show ?thesis
          using ** nondis b  K by (force simp add: disjnt_iff)
      next
        case 3
        define W where "W  {x  topspace X. f x  {b..a}}"
        have "closedin X W"
          unfolding W_def
          by (metis (no_types) assms closed_real_atLeastAtMost closed_closedin continuous_map_closedin)
        show ?thesis
        proof (rule * [OF 3, of "V  W" "U  W"])
          show "closedin X (U  W)" "closedin X (V  W)"
            using closedin X W clo by auto
          show "U  W  {}" "V  W  {}"
            using nondis 3 by (auto simp: disjnt_iff W_def)
          show "disjnt (V  W) (U  W)"
            using is_interval K unfolding is_interval_1 disjnt_iff W_def
            by (metis (mono_tags, lifting) a  K b  K ** Int_Collect atLeastAtMost_iff)
          have "x. x  topspace X; b  f x; f x  a  x  U  x  V"
            using a  K b  K is_interval K UV unfolding is_interval_1 disjnt_iff
            by blast
          then show "{x  topspace X. f x  {b..a}} = V  W  U  W"
            by (auto simp: W_def)
          show "disjnt (V  W) {x  topspace X. f x = a}" "disjnt (U  W) {x  topspace X. f x = b}"
            using ** a  K b  K nondis by (force simp: disjnt_iff)+
        qed      
      qed
    qed
    then show "connectedin X {x  topspace X. f x  K}"
      unfolding connectedin_closedin disjnt_iff by blast
  qed
qed

lemma monotone_map_into_euclideanreal:
   "connected_space X; continuous_map X euclideanreal f
     monotone_map X euclideanreal f 
        (k. is_interval k  connectedin X {x  topspace X. f x  k})"
  by (simp add: monotone_map_into_euclideanreal_alt)

lemma monotone_map_euclideanreal_alt:
   "(I::real set. is_interval I  is_interval {x::real. x  S  f x  I}) 
    is_interval S  (mono_on S f  antimono_on S f)" (is "?lhs=?rhs")
proof
  assume L [rule_format]: ?lhs 
  show ?rhs
  proof
    show "is_interval S"
      using L is_interval_1 by auto
    have False if "a  S" "b  S" "c  S" "a<b" "b<c" and d: "f a < f b  f c < f b  f a > f b  f c > f b" for a b c
      using d
    proof
      assume "f a < f b  f c < f b"
      then show False
        using L [of "{y.  y < f b}"] unfolding is_interval_1
        by (smt (verit, best) mem_Collect_eq that)
    next
      assume "f b < f a  f b < f c"
      then show False
        using L [of "{y.  y > f b}"] unfolding is_interval_1
        by (smt (verit, best) mem_Collect_eq that)
    qed
    then show "mono_on S f  monotone_on S (≤) (≥) f"
      unfolding monotone_on_def by (smt (verit))
  qed
next
  assume ?rhs then show ?lhs
    unfolding is_interval_1 monotone_on_def by simp meson
qed


lemma monotone_map_euclideanreal:
  fixes S :: "real set"
  shows
   "is_interval S; continuous_on S f  
    monotone_map (top_of_set S) euclideanreal f  (mono_on S f  monotone_on S (≤) (≥) f)"
  using monotone_map_euclideanreal_alt 
  by (simp add: monotone_map_into_euclideanreal connectedin_subtopology is_interval_connected_1)

lemma injective_eq_monotone_map:
  fixes f :: "real  real"
  assumes "is_interval S" "continuous_on S f"
  shows "inj_on f S  strict_mono_on S f  strict_antimono_on S f"
  by (metis assms injective_imp_monotone_map monotone_map_euclideanreal strict_antimono_iff_antimono 
        strict_mono_iff_mono top_greatest topspace_euclidean topspace_euclidean_subtopology)


subsection‹Normal spaces›

definition normal_space 
  where "normal_space X 
        S T. closedin X S  closedin X T  disjnt S T 
               (U V. openin X U  openin X V  S  U  T  V  disjnt U V)"

lemma normal_space_retraction_map_image:
  assumes r: "retraction_map X Y r" and X: "normal_space X"
  shows "normal_space Y"
  unfolding normal_space_def
proof clarify
  fix S T
  assume "closedin Y S" and "closedin Y T" and "disjnt S T"
  obtain r' where r': "retraction_maps X Y r r'"
    using r retraction_map_def by blast
  have "closedin X {x  topspace X. r x  S}" "closedin X {x  topspace X. r x  T}"
    using closedin_continuous_map_preimage closedin Y S closedin Y T r'
    by (auto simp: retraction_maps_def)
  moreover
  have "disjnt {x  topspace X. r x  S} {x  topspace X. r x  T}"
    using disjnt S T by (auto simp: disjnt_def)
  ultimately
  obtain U V where UV: "openin X U  openin X V  {x  topspace X. r x  S}  U  {x  topspace X. r x  T}  V" "disjnt U V"
    by (meson X normal_space_def)
  show "U V. openin Y U  openin Y V  S  U  T  V  disjnt U V"
  proof (intro exI conjI)
    show "openin Y {x  topspace Y. r' x  U}" "openin Y {x  topspace Y. r' x  V}"
      using openin_continuous_map_preimage UV r'
      by (auto simp: retraction_maps_def)
    show "S  {x  topspace Y. r' x  U}" "T  {x  topspace Y. r' x  V}"
      using openin_continuous_map_preimage UV r' closedin Y S closedin Y T 
      by (auto simp add: closedin_def continuous_map_closedin retraction_maps_def subset_iff Pi_iff)
    show "disjnt {x  topspace Y. r' x  U} {x  topspace Y. r' x  V}"
      using disjnt U V by (auto simp: disjnt_def)
  qed
qed

lemma homeomorphic_normal_space:
   "X homeomorphic_space Y  normal_space X  normal_space Y"
  unfolding homeomorphic_space_def
  by (meson homeomorphic_imp_retraction_maps homeomorphic_maps_sym normal_space_retraction_map_image retraction_map_def)

lemma normal_space:
  "normal_space X 
    (S T. closedin X S  closedin X T  disjnt S T
           (U. openin X U  S  U  disjnt T (X closure_of U)))"
proof -
  have "(V. openin X U  openin X V  S  U  T  V  disjnt U V)  openin X U  S  U  disjnt T (X closure_of U)"
    (is "?lhs=?rhs")
    if "closedin X S" "closedin X T" "disjnt S T" for S T U
  proof
    show "?lhs  ?rhs"
      by (smt (verit, best) disjnt_iff in_closure_of subsetD)
    assume R: ?rhs
    then have "(U  S)  (topspace X - X closure_of U) = {}"
      by (metis Diff_eq_empty_iff Int_Diff Int_Un_eq(4) closure_of_subset inf.orderE openin_subset)
    moreover have "T  topspace X - X closure_of U"
      by (meson DiffI R closedin_subset disjnt_iff subsetD subsetI that(2))
    ultimately show ?lhs
      by (metis R closedin_closure_of closedin_def disjnt_def sup.orderE)
  qed
  then show ?thesis
    unfolding normal_space_def by meson
qed

lemma normal_space_alt:
   "normal_space X 
    (S U. closedin X S  openin X U  S  U  (V. openin X V  S  V  X closure_of V  U))"
proof -
  have "V. openin X V  S  V  X closure_of V  U"
    if "T. closedin X T  disjnt S T  (U. openin X U  S  U  disjnt T (X closure_of U))"
       "closedin X S" "openin X U" "S  U"
    for S U
    using that 
    by (smt (verit) Diff_eq_empty_iff Int_Diff closure_of_subset_topspace disjnt_def inf.orderE inf_commute openin_closedin_eq)
  moreover have "U. openin X U  S  U  disjnt T (X closure_of U)"
    if "U. openin X U  S  U  (V. openin X V  S  V  X closure_of V  U)"
      and "closedin X S" "closedin X T" "disjnt S T"
    for S T
    using that   
    by (smt (verit) Diff_Diff_Int Diff_eq_empty_iff Int_Diff closedin_def disjnt_def inf.absorb_iff2 inf.orderE)
  ultimately show ?thesis
    by (fastforce simp: normal_space)
qed

lemma normal_space_closures:
   "normal_space X 
    (S T. S  topspace X  T  topspace X 
              disjnt (X closure_of S) (X closure_of T)
               (U V. openin X U  openin X V  S  U  T  V  disjnt U V))" 
   (is "?lhs=?rhs")
proof
  show "?lhs  ?rhs"
    by (meson closedin_closure_of closure_of_subset normal_space_def order.trans)
  show "?rhs  ?lhs"
    by (metis closedin_subset closure_of_eq normal_space_def)
qed

lemma normal_space_disjoint_closures:
   "normal_space X 
    (S T. closedin X S  closedin X T  disjnt S T
           (U V. openin X U  openin X V  S  U  T  V 
                    disjnt (X closure_of U) (X closure_of V)))"
   (is "?lhs=?rhs")
proof
  show "?lhs  ?rhs"
    by (metis closedin_closure_of normal_space)
  show "?rhs  ?lhs"
    by (smt (verit) closure_of_subset disjnt_iff normal_space openin_subset subset_eq)
qed

lemma normal_space_dual:
   "normal_space X 
    (U V. openin X U  openin X V  U  V = topspace X
           (S T. closedin X S  closedin X T  S  U  T  V  S  T = topspace X))"
   (is "_ = ?rhs")
proof -
  have "normal_space X 
        (U V. closedin X U  closedin X V  disjnt U V 
              (S T. ¬ (openin X S  openin X T 
                         ¬ (U  S  V  T  disjnt S T))))"
    unfolding normal_space_def by meson
  also have "...  (U V. openin X U  openin X V  disjnt (topspace X - U) (topspace X - V) 
              (S T. ¬ (openin X S  openin X T 
                         ¬ (topspace X - U  S  topspace X - V  T  disjnt S T))))"
    by (auto simp: all_closedin)
  also have "...  ?rhs"
  proof -
    have *: "disjnt (topspace X - U) (topspace X - V)  U  V = topspace X"
      if "U  topspace X" "V  topspace X" for U V
      using that by (auto simp: disjnt_iff)
    show ?thesis
      using ex_closedin *
      apply (simp add: ex_closedin * [OF openin_subset openin_subset] cong: conj_cong)
      apply (intro all_cong1 ex_cong1 imp_cong refl)
      by (smt (verit, best) "*" Diff_Diff_Int Diff_subset Diff_subset_conv inf.orderE inf_commute openin_subset sup_commute)
  qed
  finally show ?thesis .
qed


lemma normal_t1_imp_Hausdorff_space:
  assumes "normal_space X" "t1_space X"
  shows "Hausdorff_space X"
  unfolding Hausdorff_space_def
proof clarify
  fix x y
  assume xy: "x  topspace X" "y  topspace X" "x  y"
  then have "disjnt {x} {y}"
    by (auto simp: disjnt_iff)
  then show "U V. openin X U  openin X V  x  U  y  V  disjnt U V"
    using assms xy closedin_t1_singleton normal_space_def
    by (metis singletonI subsetD)
qed

lemma normal_t1_eq_Hausdorff_space:
   "normal_space X  t1_space X  Hausdorff_space X"
  using normal_t1_imp_Hausdorff_space t1_or_Hausdorff_space by blast

lemma normal_t1_imp_regular_space:
   "normal_space X; t1_space X  regular_space X"
  by (metis compactin_imp_closedin normal_space_def normal_t1_eq_Hausdorff_space regular_space_compact_closed_sets)

lemma compact_Hausdorff_or_regular_imp_normal_space:
   "compact_space X; Hausdorff_space X  regular_space X
         normal_space X"
  by (metis Hausdorff_space_compact_sets closedin_compact_space normal_space_def regular_space_compact_closed_sets)

lemma normal_space_discrete_topology:
   "normal_space(discrete_topology U)"
  by (metis discrete_topology_closure_of inf_le2 normal_space_alt)

lemma normal_space_fsigmas:
  "normal_space X 
    (S T. fsigma_in X S  fsigma_in X T  separatedin X S T
            (U B. openin X U  openin X B  S  U  T  B  disjnt U B))" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
  proof clarify
    fix S T
    assume "fsigma_in X S" 
    then obtain C where C: "n. closedin X (C n)" "n. C n  C (Suc n)" " (range C) = S"
      by (meson fsigma_in_ascending)
    assume "fsigma_in X T" 
    then obtain D where D: "n. closedin X (D n)" "n. D n  D (Suc n)" " (range D) = T"
      by (meson fsigma_in_ascending)
    assume "separatedin X S T"
    have "n. disjnt (D n) (X closure_of S)"
      by (metis D(3) separatedin X S T disjnt_Union1 disjnt_def rangeI separatedin_def)
    then have "n. V V'. openin X V  openin X V'  D n  V  X closure_of S  V'  disjnt V V'"
      by (metis D(1) L closedin_closure_of normal_space_def)
    then obtain V V' where V: "n. openin X (V n)" and "n. openin X (V' n)" "n. disjnt (V n) (V' n)"
          and DV:  "n. D n  V n" 
          and subV': "n. X closure_of S  V' n"
      by metis
    then have VV: "V' n  X closure_of V n = {}" for n
      using openin_Int_closure_of_eq_empty [of X "V' n" "V n"] by (simp add: Int_commute disjnt_def)
    have "n. disjnt (C n) (X closure_of T)"
      by (metis C(3) separatedin X S T disjnt_Union1 disjnt_def rangeI separatedin_def)
    then have "n. U U'. openin X U  openin X U'  C n  U  X closure_of T  U'  disjnt U U'"
      by (metis C(1) L closedin_closure_of normal_space_def)
    then obtain U U' where U: "n. openin X (U n)" and "n. openin X (U' n)" "n. disjnt (U n) (U' n)"
          and CU:  "n. C n  U n" 
          and subU': "n. X closure_of T  U' n"
      by metis
    then have UU: "U' n  X closure_of U n = {}" for n
      using openin_Int_closure_of_eq_empty [of X "U' n" "U n"] by (simp add: Int_commute disjnt_def)
    show "U B. openin X U  openin X B  S  U  T  B  disjnt U B"
    proof (intro conjI exI)
      have "S n. closedin X (mn. X closure_of V m)"
        by (force intro: closedin_Union)
      then show "openin X (n. U n - (mn. X closure_of V m))"
        using U by blast
      have "S n. closedin X (mn. X closure_of U m)"
        by (force intro: closedin_Union)
      then show "openin X (n. V n - (mn. X closure_of U m))"
        using V by blast
      have "S  topspace X"
        by (simp add: fsigma_in X S fsigma_in_subset)
      then show "S  (n. U n - (mn. X closure_of V m))"
        apply (clarsimp simp: Ball_def)
        by (metis VV C(3) CU IntI UN_E closure_of_subset empty_iff subV' subsetD)
      have "T  topspace X"
        by (simp add: fsigma_in X T fsigma_in_subset)
      then show "T  (n. V n - (mn. X closure_of U m))"
        apply (clarsimp simp: Ball_def)
        by (metis UU D(3) DV IntI UN_E closure_of_subset empty_iff subU' subsetD)
      have "x m n. x  U n; x  V m; km. x  X closure_of U k  kn. x  X closure_of V k"
        by (meson U V closure_of_subset nat_le_linear openin_subset subsetD)
      then show "disjnt (n. U n - (mn. X closure_of V m)) (n. V n - (mn. X closure_of U m))"
        by (force simp: disjnt_iff)
    qed
  qed
next
  show "?rhs  ?lhs"
    by (simp add: closed_imp_fsigma_in normal_space_def separatedin_closed_sets)
qed

lemma normal_space_fsigma_subtopology:
  assumes "normal_space X" "fsigma_in X S"
  shows "normal_space (subtopology X S)"
  unfolding normal_space_fsigmas
proof clarify
  fix T U
  assume "fsigma_in (subtopology X S) T"
      and "fsigma_in (subtopology X S) U"
      and TU: "separatedin (subtopology X S) T U"
  then obtain A B where "openin X A  openin X B  T  A  U  B  disjnt A B"
    by (metis assms fsigma_in_fsigma_subtopology normal_space_fsigmas separatedin_subtopology)
  then
  show "A B. openin (subtopology X S) A  openin (subtopology X S) B  T  A 
   U  B  disjnt A B"
    using TU
    by (force simp add: separatedin_subtopology openin_subtopology_alt disjnt_iff)
qed

lemma normal_space_closed_subtopology:
  assumes "normal_space X" "closedin X S"
  shows "normal_space (subtopology X S)"
  by (simp add: assms closed_imp_fsigma_in normal_space_fsigma_subtopology)

lemma normal_space_continuous_closed_map_image:
  assumes "normal_space X" and contf: "continuous_map X Y f" 
    and clof: "closed_map X Y f"  and fim: "f ` topspace X = topspace Y"
shows "normal_space Y"
  unfolding normal_space_def
proof clarify
  fix S T
  assume "closedin Y S" and "closedin Y T" and "disjnt S T"
  have "closedin X {x  topspace X. f x  S}" "closedin X {x  topspace X. f x  T}"
    using closedin Y S closedin Y T closedin_continuous_map_preimage contf by auto
  moreover
  have "disjnt {x  topspace X. f x  S} {x  topspace X. f x  T}"
    using disjnt S T by (auto simp: disjnt_iff)
  ultimately
  obtain U V where "closedin X U" "closedin X V" 
    and subXU: "{x  topspace X. f x  S}  topspace X - U" 
    and subXV: "{x  topspace X. f x  T}  topspace X - V" 
    and dis: "disjnt (topspace X - U) (topspace X -V)"
    using normal_space X by (force simp add: normal_space_def ex_openin)
  have "closedin Y (f ` U)" "closedin Y (f ` V)"
    using closedin X U closedin X V clof closed_map_def by blast+
  moreover have "S  topspace Y - f ` U"
    using closedin Y S closedin X U subXU by (force dest: closedin_subset)
  moreover have "T  topspace Y - f ` V"
    using closedin Y T closedin X V subXV by (force dest: closedin_subset)
  moreover have "disjnt (topspace Y - f ` U) (topspace Y - f ` V)"
    using fim dis by (force simp add: disjnt_iff)
  ultimately show "U V. openin Y U  openin Y V  S  U  T  V  disjnt U V"
    by (force simp add: ex_openin)
qed


subsection ‹Hereditary topological properties›

definition hereditarily 
  where "hereditarily P X 
        S. S  topspace X  P(subtopology X S)"

lemma hereditarily:
   "hereditarily P X  (S. P(subtopology X S))"
  by (metis Int_lower1 hereditarily_def subtopology_restrict)

lemma hereditarily_mono:
   "hereditarily P X; x. P x  Q x  hereditarily Q X"
  by (simp add: hereditarily)

lemma hereditarily_inc:
   "hereditarily P X  P X"
  by (metis hereditarily subtopology_topspace)

lemma hereditarily_subtopology:
   "hereditarily P X  hereditarily P (subtopology X S)"
  by (simp add: hereditarily subtopology_subtopology)

lemma hereditarily_normal_space_continuous_closed_map_image:
  assumes X: "hereditarily normal_space X" and contf: "continuous_map X Y f" 
    and clof: "closed_map X Y f"  and fim: "f ` (topspace X) = topspace Y" 
  shows "hereditarily normal_space Y"
  unfolding hereditarily_def
proof (intro strip)
  fix T
  assume "T  topspace Y"
  then have nx: "normal_space (subtopology X {x  topspace X. f x  T})"
    by (meson X hereditarily)
  moreover have "continuous_map (subtopology X {x  topspace X. f x  T}) (subtopology Y T) f"
    by (simp add: contf continuous_map_from_subtopology continuous_map_in_subtopology image_subset_iff)
  moreover have "closed_map (subtopology X {x  topspace X. f x  T}) (subtopology Y T) f"
    by (simp add: clof closed_map_restriction)
  ultimately show "normal_space (subtopology Y T)"
    using fim normal_space_continuous_closed_map_image by fastforce
qed

lemma homeomorphic_hereditarily_normal_space:
   "X homeomorphic_space Y
       (hereditarily normal_space X  hereditarily normal_space Y)"
  by (meson hereditarily_normal_space_continuous_closed_map_image homeomorphic_eq_everything_map 
      homeomorphic_space homeomorphic_space_sym)

lemma hereditarily_normal_space_retraction_map_image:
   "retraction_map X Y r; hereditarily normal_space X  hereditarily normal_space Y"
  by (smt (verit) hereditarily_subtopology hereditary_imp_retractive_property homeomorphic_hereditarily_normal_space)

subsection‹Limits in a topological space›

lemma limitin_const_iff:
  assumes "t1_space X" "¬ trivial_limit F"
  shows "limitin X (λk. a) l F  l  topspace X  a = l"  (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    using assms unfolding limitin_def t1_space_def by (metis eventually_const openin_topspace)
next
  assume ?rhs then show ?lhs
    using assms by (auto simp: limitin_def t1_space_def)
qed

lemma compactin_sequence_with_limit:
  assumes lim: "limitin X σ l sequentially" and "S  range σ" and SX: "S  topspace X"
  shows "compactin X (insert l S)"
unfolding compactin_def
proof (intro conjI strip)
  show "insert l S  topspace X"
    by (meson SX insert_subset lim limitin_topspace)
  fix 𝒰
  assume §: "Ball 𝒰 (openin X)  insert l S   𝒰"
  have "V. finite V  V  𝒰  (t  V. l  t)  S   V"
    if *: "x  S. T  𝒰. x  T" and "T  𝒰" "l  T" for T
  proof -
    obtain V where V: "x. x  S  V x  𝒰  x  V x"
      using * by metis
    obtain N where N: "n. N  n  σ n  T"
      by (meson "§" T  𝒰 l  T lim limitin_sequentially)
    show ?thesis
    proof (intro conjI exI)
      have "x  T"
        if "x  S" and "A. (x  S. (nN. x  σ n)  A  V x)  x  A" for x 
        by (metis (no_types) N V that assms(2) imageE nle_le subsetD)
      then show "S   (insert T (V ` (S  σ ` {0..N})))"
        by force
    qed (use V that in auto)
  qed
  then show ". finite     𝒰  insert l S   "
    by (smt (verit, best) Union_iff § insert_subset subsetD)
qed

lemma limitin_Hausdorff_unique:
  assumes "limitin X f l1 F" "limitin X f l2 F" "¬ trivial_limit F" "Hausdorff_space X"
  shows "l1 = l2"
proof (rule ccontr)
  assume "l1  l2"
  with assms obtain U V where "openin X U" "openin X V" "l1  U" "l2  V" "disjnt U V"
    by (metis Hausdorff_space_def limitin_topspace)
  then have "eventually (λx. f x  U) F" "eventually (λx. f x  V) F"
    using assms by (fastforce simp: limitin_def)+
  then have "x. f x  U  f x  V"
    using assms eventually_elim2 filter_eq_iff by fastforce
  with assms disjnt U V show False
    by (meson disjnt_iff)
qed

lemma limitin_kc_unique:
  assumes "kc_space X" and lim1: "limitin X f l1 sequentially" and lim2: "limitin X f l2 sequentially"
  shows "l1 = l2"
proof (rule ccontr)
  assume "l1  l2"
  define A where "A  insert l1 (range f - {l2})"
  have "l1  topspace X"
    using lim1 limitin_def by fastforce
  moreover have "compactin X (insert l1 (topspace X  (range f - {l2})))"
    by (meson Diff_subset compactin_sequence_with_limit inf_le1 inf_le2 lim1 subset_trans)
  ultimately have "compactin X (topspace X  A)"
    by (simp add: A_def)
  then have OXA: "openin X (topspace X - A)"
    by (metis Diff_Diff_Int Diff_subset kc_space X kc_space_def openin_closedin_eq)
  have "l2  topspace X - A"
    using l1  l2 A_def lim2 limitin_topspace by fastforce
  then have "F x in sequentially. f x = l2"
    using limitinD [OF lim2 OXA] by (auto simp: A_def eventually_conj_iff)
  then show False
    using limitin_transform_eventually [OF _ lim1] 
          limitin_const_iff [OF kc_imp_t1_space trivial_limit_sequentially]
    using l1  l2 kc_space X by fastforce
qed

lemma limitin_closedin:
  assumes lim: "limitin X f l F" 
    and "closedin X S" and ev: "eventually (λx. f x  S) F" "¬ trivial_limit F"
  shows "l  S"
proof (rule ccontr)
  assume "l  S"
  have "F x in F. f x  topspace X - S"
    by (metis Diff_iff l  S closedin X S closedin_def lim limitin_def)
  with ev eventually_elim2 trivial_limit_def show False
    by force
qed

subsection‹Quasi-components›

definition quasi_component_of :: "'a topology  'a  'a  bool"
  where
  "quasi_component_of X x y 
        x  topspace X  y  topspace X 
        (T. closedin X T  openin X T  (x  T  y  T))"

abbreviation "quasi_component_of_set S x  Collect (quasi_component_of S x)"

definition quasi_components_of :: "'a topology  ('a set) set"
  where
  "quasi_components_of X = quasi_component_of_set X ` topspace X"

lemma quasi_component_in_topspace:
   "quasi_component_of X x y  x  topspace X  y  topspace X"
  by (simp add: quasi_component_of_def)

lemma quasi_component_of_refl [simp]:
   "quasi_component_of X x x  x  topspace X"
  by (simp add: quasi_component_of_def)

lemma quasi_component_of_sym:
   "quasi_component_of X x y  quasi_component_of X y x"
  by (meson quasi_component_of_def)

lemma quasi_component_of_trans:
   "quasi_component_of X x y; quasi_component_of X y z  quasi_component_of X x z"
  by (simp add: quasi_component_of_def)

lemma quasi_component_of_subset_topspace:
   "quasi_component_of_set X x  topspace X"
  using quasi_component_of_def by fastforce

lemma quasi_component_of_eq_empty:
   "quasi_component_of_set X x = {}  (x  topspace X)"
  using quasi_component_of_def by fastforce

lemma quasi_component_of:
   "quasi_component_of X x y 
    x  topspace X  y  topspace X  (T. x  T  closedin X T  openin X T  y  T)"
  unfolding quasi_component_of_def by (metis Diff_iff closedin_def openin_closedin_eq) 

lemma quasi_component_of_alt:
  "quasi_component_of X x y 
      x  topspace X  y  topspace X 
      ¬ (U V. openin X U  openin X V  U  V = topspace X  disjnt U V  x  U  y  V)" 
  (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    unfolding quasi_component_of_def
    by (metis disjnt_iff separatedin_full separatedin_open_sets)
  show "?rhs  ?lhs"
    unfolding quasi_component_of_def
    by (metis Diff_disjoint Diff_iff Un_Diff_cancel closedin_def disjnt_def inf_commute sup.orderE sup_commute)
qed

lemma quasi_components_lepoll_topspace: "quasi_components_of X  topspace X"
  by (simp add: image_lepoll quasi_components_of_def)

lemma quasi_component_of_separated:
   "quasi_component_of X x y 
     x  topspace X  y  topspace X 
     ¬ (U V. separatedin X U V  U  V = topspace X  x  U  y  V)"
  by (meson quasi_component_of_alt separatedin_full separatedin_open_sets)

lemma quasi_component_of_subtopology:
  "quasi_component_of (subtopology X s) x y  quasi_component_of X x y"
  unfolding quasi_component_of_def
  by (simp add: closedin_subtopology) (metis Int_iff inf_commute openin_subtopology_Int2)

lemma quasi_component_of_mono:
   "quasi_component_of (subtopology X S) x y  S  T
         quasi_component_of (subtopology X T) x y"
  by (metis inf.absorb_iff2 quasi_component_of_subtopology subtopology_subtopology)

lemma quasi_component_of_equiv:
   "quasi_component_of X x y 
    x  topspace X  y  topspace X  quasi_component_of X x = quasi_component_of X y"
  using quasi_component_of_def by fastforce

lemma quasi_component_of_disjoint [simp]:
   "disjnt (quasi_component_of_set X x) (quasi_component_of_set X y)  ¬ (quasi_component_of X x y)"
  by (metis disjnt_iff quasi_component_of_equiv mem_Collect_eq)

lemma quasi_component_of_eq:
   "quasi_component_of X x = quasi_component_of X y 
    (x  topspace X  y  topspace X) 
   x  topspace X  y  topspace X  quasi_component_of X x y"
  by (metis Collect_empty_eq_bot quasi_component_of_eq_empty quasi_component_of_equiv)

lemma topspace_imp_quasi_components_of:
  assumes "x  topspace X"
  obtains C where "C  quasi_components_of X" "x  C"
  by (metis assms imageI mem_Collect_eq quasi_component_of_refl quasi_components_of_def)

lemma Union_quasi_components_of: " (quasi_components_of X) = topspace X"
  by (auto simp: quasi_components_of_def quasi_component_of_def)

lemma pairwise_disjoint_quasi_components_of:
   "pairwise disjnt (quasi_components_of X)"
  by (auto simp: quasi_components_of_def quasi_component_of_def disjoint_def)

lemma complement_quasi_components_of_Union:
  assumes "C  quasi_components_of X"
  shows "topspace X - C =  (quasi_components_of X - {C})"  (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    using Union_quasi_components_of by fastforce
  show "?rhs  ?lhs"
    using assms
    using quasi_component_of_equiv by (fastforce simp add: quasi_components_of_def image_iff subset_iff)
qed

lemma nonempty_quasi_components_of:
   "C  quasi_components_of X  C  {}"
  by (metis imageE quasi_component_of_eq_empty quasi_components_of_def)

lemma quasi_components_of_subset:
   "C  quasi_components_of X  C  topspace X"
  using Union_quasi_components_of by force

lemma quasi_component_in_quasi_components_of:
   "quasi_component_of_set X a  quasi_components_of X  a  topspace X"
  by (metis (no_types, lifting) image_iff quasi_component_of_eq_empty quasi_components_of_def)

lemma quasi_components_of_eq_empty [simp]:
   "quasi_components_of X = {}  X = trivial_topology"
  by (simp add: quasi_components_of_def)

lemma quasi_components_of_empty_space [simp]:
   "quasi_components_of trivial_topology = {}"
  by simp

lemma quasi_component_of_set:
   "quasi_component_of_set X x =
        (if x  topspace X
        then  {t. closedin X t  openin X t  x  t}
        else {})"
  by (auto simp: quasi_component_of)

lemma closedin_quasi_component_of: "closedin X (quasi_component_of_set X x)"
  by (auto simp: quasi_component_of_set)

lemma closedin_quasi_components_of:
   "C  quasi_components_of X  closedin X C"
  by (auto simp: quasi_components_of_def closedin_quasi_component_of)

lemma openin_finite_quasi_components:
  "finite(quasi_components_of X); C  quasi_components_of X  openin X C"
  apply (simp add:openin_closedin_eq quasi_components_of_subset complement_quasi_components_of_Union)
  by (meson DiffD1 closedin_Union closedin_quasi_components_of finite_Diff)

lemma quasi_component_of_eq_overlap:
   "quasi_component_of X x = quasi_component_of X y 
      (x  topspace X  y  topspace X) 
      ¬ (quasi_component_of_set X x  quasi_component_of_set X y = {})"
  using quasi_component_of_equiv by fastforce

lemma quasi_component_of_nonoverlap:
   "quasi_component_of_set X x  quasi_component_of_set X y = {} 
     (x  topspace X)  (y  topspace X) 
     ¬ (quasi_component_of X x = quasi_component_of X y)"
  by (metis inf.idem quasi_component_of_eq_empty quasi_component_of_eq_overlap)

lemma quasi_component_of_overlap:
   "¬ (quasi_component_of_set X x  quasi_component_of_set X y = {}) 
    x  topspace X  y  topspace X  quasi_component_of X x = quasi_component_of X y"
  by (meson quasi_component_of_nonoverlap)

lemma quasi_components_of_disjoint:
   "C  quasi_components_of X; D  quasi_components_of X  disjnt C D  C  D"
  by (metis disjnt_self_iff_empty nonempty_quasi_components_of pairwiseD pairwise_disjoint_quasi_components_of)

lemma quasi_components_of_overlap:
   "C  quasi_components_of X; D  quasi_components_of X  ¬ (C  D = {})  C = D"
  by (metis disjnt_def quasi_components_of_disjoint)

lemma pairwise_separated_quasi_components_of:
   "pairwise (separatedin X) (quasi_components_of X)"
  by (metis closedin_quasi_components_of pairwise_def pairwise_disjoint_quasi_components_of separatedin_closed_sets)

lemma finite_quasi_components_of_finite:
   "finite(topspace X)  finite(quasi_components_of X)"
  by (simp add: Union_quasi_components_of finite_UnionD)

lemma connected_imp_quasi_component_of:
  assumes "connected_component_of X x y"
  shows "quasi_component_of X x y"
proof -
  have "x  topspace X" "y  topspace X"
    by (meson assms connected_component_of_equiv)+
  with assms show ?thesis
    apply (clarsimp simp add: quasi_component_of connected_component_of_def)
    by (meson connectedin_clopen_cases disjnt_iff subsetD)
qed

lemma connected_component_subset_quasi_component_of:
   "connected_component_of_set X x  quasi_component_of_set X x"
  using connected_imp_quasi_component_of by force

lemma quasi_component_as_connected_component_Union:
   "quasi_component_of_set X x =
     (connected_component_of_set X ` quasi_component_of_set X x)" 
    (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    using connected_component_of_refl quasi_component_of by fastforce
  show "?rhs  ?lhs"
    apply (rule SUP_least)
    by (simp add: connected_component_subset_quasi_component_of quasi_component_of_equiv)
qed

lemma quasi_components_as_connected_components_Union:
  assumes "C  quasi_components_of X"
  obtains 𝒯 where "𝒯  connected_components_of X" "𝒯 = C"
proof -
  obtain x where "x  topspace X" and Ceq: "C = quasi_component_of_set X x"
    by (metis assms imageE quasi_components_of_def)
  define 𝒯 where "𝒯  connected_component_of_set X ` quasi_component_of_set X x"
  show thesis
  proof
    show "𝒯  connected_components_of X"
      by (simp add: 𝒯_def connected_components_of_def image_mono quasi_component_of_subset_topspace)
    show "𝒯 = C"
      by (metis 𝒯_def Ceq quasi_component_as_connected_component_Union)
  qed
qed

lemma path_imp_quasi_component_of:
   "path_component_of X x y  quasi_component_of X x y"
  by (simp add: connected_imp_quasi_component_of path_imp_connected_component_of)

lemma path_component_subset_quasi_component_of:
   "path_component_of_set X x  quasi_component_of_set X x"
  by (simp add: Collect_mono path_imp_quasi_component_of)

lemma connected_space_iff_quasi_component:
   "connected_space X  (x  topspace X. y  topspace X. quasi_component_of X x y)"
  unfolding connected_space_clopen_in closedin_def quasi_component_of
  by blast

lemma connected_space_imp_quasi_component_of:
   " connected_space X; a  topspace X; b  topspace X  quasi_component_of X a b"
  by (simp add: connected_space_iff_quasi_component)

lemma connected_space_quasi_component_set:
   "connected_space X  (x  topspace X. quasi_component_of_set X x = topspace X)"
  by (metis Ball_Collect connected_space_iff_quasi_component quasi_component_of_subset_topspace subset_antisym)

lemma connected_space_iff_quasi_components_eq:
  "connected_space X 
    (C  quasi_components_of X. D  quasi_components_of X. C = D)"
  apply (simp add: quasi_components_of_def)
  by (metis connected_space_iff_quasi_component mem_Collect_eq quasi_component_of_equiv)

lemma quasi_components_of_subset_sing:
   "quasi_components_of X  {S}  connected_space X  (X = trivial_topology  topspace X = S)"
proof (cases "quasi_components_of X = {}")
  case True
  then show ?thesis
    by (simp add: subset_singleton_iff)
next
  case False
  then show ?thesis
    apply (simp add: connected_space_iff_quasi_components_eq subset_iff Ball_def)
    by (metis False Union_quasi_components_of ccpo_Sup_singleton insert_iff is_singletonE is_singletonI')
qed

lemma connected_space_iff_quasi_components_subset_sing:
   "connected_space X  (a. quasi_components_of X  {a})"
  by (simp add: quasi_components_of_subset_sing)

lemma quasi_components_of_eq_singleton:
   "quasi_components_of X = {S} 
        connected_space X  ¬ (X = trivial_topology)  S = topspace X"
  by (metis empty_not_insert quasi_components_of_eq_empty quasi_components_of_subset_sing subset_singleton_iff)

lemma quasi_components_of_connected_space:
   "connected_space X
         quasi_components_of X = (if X = trivial_topology then {} else {topspace X})"
  by (simp add: quasi_components_of_eq_singleton)

lemma separated_between_singletons:
   "separated_between X {x} {y} 
    x  topspace X  y  topspace X  ¬ (quasi_component_of X x y)"
proof (cases "x  topspace X  y  topspace X")
  case True
  then show ?thesis
    by (auto simp add: separated_between_def quasi_component_of_alt)
qed (use separated_between_imp_subset in blast)

lemma quasi_component_nonseparated:
   "quasi_component_of X x y  x  topspace X  y  topspace X  ¬ (separated_between X {x} {y})"
  by (metis quasi_component_of_equiv separated_between_singletons)

lemma separated_between_quasi_component_pointwise_left:
  assumes "C  quasi_components_of X"
  shows "separated_between X C S  (x  C. separated_between X {x} S)"  (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    using assms quasi_components_of_disjoint separated_between_mono by fastforce
next
  assume ?rhs
  then obtain y where "separated_between X {y} S" and "y  C"
    by metis
  with assms show ?lhs
    by (force simp add: separated_between quasi_components_of_def quasi_component_of_def)
qed

lemma separated_between_quasi_component_pointwise_right:
   "C  quasi_components_of X  separated_between X S C  (x  C. separated_between X S {x})"
  by (simp add: separated_between_quasi_component_pointwise_left separated_between_sym)

lemma separated_between_quasi_component_point:
  assumes "C  quasi_components_of X"
  shows "separated_between X C {x}  x  topspace X - C" (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    by (meson DiffI disjnt_insert2 insert_subset separated_between_imp_disjoint separated_between_imp_subset)
next
  assume ?rhs
  with assms show ?lhs
    unfolding quasi_components_of_def image_iff Diff_iff separated_between_quasi_component_pointwise_left [OF assms]
    by (metis mem_Collect_eq quasi_component_of_refl separated_between_singletons)
qed

lemma separated_between_point_quasi_component:
   "C  quasi_components_of X  separated_between X {x} C  x  topspace X - C"
  by (simp add: separated_between_quasi_component_point separated_between_sym)

lemma separated_between_quasi_component_compact:
   "C  quasi_components_of X; compactin X K  (separated_between X C K  disjnt C K)"
  unfolding disjnt_iff
  using compactin_subset_topspace quasi_components_of_subset separated_between_pointwise_right separated_between_quasi_component_point by fastforce

lemma separated_between_compact_quasi_component:
   "compactin X K; C  quasi_components_of X  separated_between X K C  disjnt K C"
  using disjnt_sym separated_between_quasi_component_compact separated_between_sym by blast

lemma separated_between_quasi_components:
  assumes C: "C  quasi_components_of X" and D: "D  quasi_components_of X"
  shows "separated_between X C D  disjnt C D"   (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    by (simp add: separated_between_imp_disjoint)
next
  assume ?rhs
  obtain x y where x: "C = quasi_component_of_set X x" and "x  C"
               and y: "D = quasi_component_of_set X y" and "y  D"
    using assms by (auto simp: quasi_components_of_def)
  then have "separated_between X {x} {y}"
    using disjnt C D separated_between_singletons by fastforce
  with x  C y  D show ?lhs
    by (auto simp: assms separated_between_quasi_component_pointwise_left separated_between_quasi_component_pointwise_right)
qed

lemma quasi_eq_connected_component_of_eq:
   "quasi_component_of X x = connected_component_of X x 
    connectedin X (quasi_component_of_set X x)"  (is "?lhs = ?rhs")
proof (cases "x  topspace X")
  case True
  show ?thesis
  proof
    show "?lhs  ?rhs"
      by (simp add: connectedin_connected_component_of)
  next
    assume ?rhs
    then have "y. quasi_component_of X x y = connected_component_of X x y"
      by (metis connected_component_of_def connected_imp_quasi_component_of mem_Collect_eq quasi_component_of_equiv)
    then show ?lhs
      by force
  qed
next
  case False
  then show ?thesis
    by (metis Collect_empty_eq_bot connected_component_of_eq_empty connectedin_empty quasi_component_of_eq_empty)
qed

lemma connected_quasi_component_of:
  assumes "C  quasi_components_of X"
  shows "C  connected_components_of X  connectedin X C"  (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
    using assms
    by (simp add: connectedin_connected_components_of)
next
  assume ?rhs
  with assms show ?lhs
    unfolding quasi_components_of_def connected_components_of_def image_iff
    by (metis quasi_eq_connected_component_of_eq)
qed

lemma quasi_component_of_clopen_cases:
   "C  quasi_components_of X; closedin X T; openin X T  C  T  disjnt C T"
  by (smt (verit) disjnt_iff image_iff mem_Collect_eq quasi_component_of_def quasi_components_of_def subset_iff)

lemma quasi_components_of_set:
  assumes "C  quasi_components_of X"
  shows " {T. closedin X T  openin X T  C  T} = C"  (is "?lhs = ?rhs")
proof
  have "x  C" if "x   {T. closedin X T  openin X T  C  T}" for x
  proof (rule ccontr)
    assume "x  C"
    have "x  topspace X"
      using assms quasi_components_of_subset that by force
    then have "separated_between X C {x}"
      by (simp add: x  C assms separated_between_quasi_component_point)
    with that show False
      by (auto simp: separated_between)
  qed
  then show "?lhs  ?rhs"
    by auto
qed blast

lemma open_quasi_eq_connected_components_of:
  assumes "openin X C"
  shows "C  quasi_components_of X  C  connected_components_of X"  (is "?lhs = ?rhs")
proof (cases "closedin X C")
  case True
  show ?thesis
  proof
    assume L: ?lhs
    have "T = {}  T = topspace X  C"
      if "openin (subtopology X C) T" "closedin (subtopology X C) T" for T
    proof -
      have "C  T  disjnt C T"
        by (meson L True assms closedin_trans_full openin_trans_full quasi_component_of_clopen_cases that)
      with that show ?thesis
        by (metis Int_absorb2 True closedin_imp_subset closure_of_subset_eq disjnt_def inf_absorb2)
    qed
    with L assms show "?rhs"
      by (simp add: connected_quasi_component_of connected_space_clopen_in connectedin_def openin_subset)
  next
    assume ?rhs
    then obtain x where "x  topspace X" and x: "C = connected_component_of_set X x"
      by (metis connected_components_of_def imageE)
    have "C = quasi_component_of_set X x"
      using True assms connected_component_of_refl connected_imp_quasi_component_of quasi_component_of_def x by fastforce
    then show ?lhs
      using x  topspace X quasi_components_of_def by fastforce
  qed
next
  case False
  then show ?thesis
    using closedin_connected_components_of closedin_quasi_components_of by blast
qed

lemma quasi_component_of_continuous_image:
  assumes f:  "continuous_map X Y f" and qc: "quasi_component_of X x y"
  shows "quasi_component_of Y (f x) (f y)"
  unfolding quasi_component_of_def
proof (intro strip conjI)
  show "f x  topspace Y" "f y  topspace Y"
    using assms by (simp_all add: continuous_map_def quasi_component_of_def Pi_iff)
  fix T
  assume "closedin Y T  openin Y T"
  with assms show "(f x  T) = (f y  T)"
    by (smt (verit) continuous_map_closedin continuous_map_def mem_Collect_eq quasi_component_of_def)
qed

lemma quasi_component_of_discrete_topology:
   "quasi_component_of_set (discrete_topology U) x = (if x  U then {x} else {})"
proof -
  have "quasi_component_of_set (discrete_topology U) y = {y}" if "y  U" for y
    using that
    apply (simp add: set_eq_iff quasi_component_of_def)
    by (metis Set.set_insert insertE subset_insertI)
  then show ?thesis
    by (simp add: quasi_component_of)
qed

lemma quasi_components_of_discrete_topology:
   "quasi_components_of (discrete_topology U) = (λx. {x}) ` U"
  by (auto simp add: quasi_components_of_def quasi_component_of_discrete_topology)

lemma homeomorphic_map_quasi_component_of:
  assumes hmf: "homeomorphic_map X Y f" and "x  topspace X"
  shows "quasi_component_of_set Y (f x) = f ` (quasi_component_of_set X x)"
proof -
  obtain g where hmg: "homeomorphic_map Y X g"
    and contf: "continuous_map X Y f" and contg: "continuous_map Y X g"
    and fg: "(x  topspace X. g(f x) = x)  (y  topspace Y. f(g y) = y)"
    by (smt (verit, best) hmf homeomorphic_map_maps homeomorphic_maps_def)
  show ?thesis
  proof
    show "quasi_component_of_set Y (f x)  f ` quasi_component_of_set X x"
      using quasi_component_of_continuous_image [OF contg]
         x  topspace X fg image_iff quasi_component_of_subset_topspace by fastforce
    show "f ` quasi_component_of_set X x  quasi_component_of_set Y (f x)"
      using quasi_component_of_continuous_image [OF contf] by blast
  qed
qed


lemma homeomorphic_map_quasi_components_of:
  assumes "homeomorphic_map X Y f"
  shows "quasi_components_of Y = image (image f) (quasi_components_of X)"
  using assms
proof -
  have "xtopspace X. quasi_component_of_set Y y = f ` quasi_component_of_set X x"
    if "y  topspace Y" for y 
    by (metis that assms homeomorphic_imp_surjective_map homeomorphic_map_quasi_component_of image_iff)
  moreover have "xtopspace Y. f ` quasi_component_of_set X u = quasi_component_of_set Y x"
    if  "u  topspace X" for u
    by (metis that assms homeomorphic_imp_surjective_map homeomorphic_map_quasi_component_of imageI)
  ultimately show ?thesis
    by (auto simp: quasi_components_of_def image_iff)
qed

lemma openin_quasi_component_of_locally_connected_space:
  assumes "locally_connected_space X"
  shows "openin X (quasi_component_of_set X x)"
proof -
  have *: "openin X (connected_component_of_set X x)"
    by (simp add: assms openin_connected_component_of_locally_connected_space)
  moreover have "connected_component_of_set X x = quasi_component_of_set X x"
    using * closedin_connected_component_of connected_component_of_refl connected_imp_quasi_component_of
            quasi_component_of_def by fastforce
  ultimately show ?thesis
    by simp
qed

lemma openin_quasi_components_of_locally_connected_space:
   "locally_connected_space X  c  quasi_components_of X
         openin X c"
  by (smt (verit, best) image_iff openin_quasi_component_of_locally_connected_space quasi_components_of_def)

lemma quasi_eq_connected_components_of_alt:
  "quasi_components_of X = connected_components_of X  (C  quasi_components_of X. connectedin X C)"
  (is "?lhs = ?rhs")
proof
  assume R: ?rhs
  moreover have "connected_components_of X  quasi_components_of X"
    using R unfolding quasi_components_of_def connected_components_of_def
    by (force simp flip: quasi_eq_connected_component_of_eq)
  ultimately show ?lhs
    using connected_quasi_component_of by blast
qed (use connected_quasi_component_of in blast)
  
lemma connected_subset_quasi_components_of_pointwise:
   "connected_components_of X  quasi_components_of X 
    (x  topspace X. quasi_component_of X x = connected_component_of X x)"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  have "connectedin X (quasi_component_of_set X x)" if "x  topspace X" for x
  proof -
    have "ytopspace X. connected_component_of_set X x = quasi_component_of_set X y"
      using L that by (force simp: quasi_components_of_def connected_components_of_def image_subset_iff)
    then show ?thesis
      by (metis connected_component_of_equiv connectedin_connected_component_of mem_Collect_eq quasi_component_of_eq)
  qed
  then show ?rhs
    by (simp add: quasi_eq_connected_component_of_eq)
qed (simp add: connected_components_of_def quasi_components_of_def)

lemma quasi_subset_connected_components_of_pointwise:
   "quasi_components_of X  connected_components_of X 
    (x  topspace X. quasi_component_of X x = connected_component_of X x)"
  by (simp add: connected_quasi_component_of image_subset_iff quasi_components_of_def quasi_eq_connected_component_of_eq)

lemma quasi_eq_connected_components_of_pointwise:
   "quasi_components_of X = connected_components_of X 
    (x  topspace X. quasi_component_of X x = connected_component_of X x)"
  using connected_subset_quasi_components_of_pointwise quasi_subset_connected_components_of_pointwise by fastforce

lemma quasi_eq_connected_components_of_pointwise_alt:
   "quasi_components_of X = connected_components_of X 
    (x. quasi_component_of X x = connected_component_of X x)"
  unfolding quasi_eq_connected_components_of_pointwise
  by (metis connectedin_empty quasi_component_of_eq_empty quasi_eq_connected_component_of_eq)

lemma quasi_eq_connected_components_of_inclusion:
   "quasi_components_of X = connected_components_of X 
        connected_components_of X  quasi_components_of X 
        quasi_components_of X  connected_components_of X"
  by (simp add: connected_subset_quasi_components_of_pointwise dual_order.eq_iff quasi_subset_connected_components_of_pointwise)


lemma quasi_eq_connected_components_of:
  "finite(connected_components_of X) 
      finite(quasi_components_of X) 
      locally_connected_space X 
      compact_space X  (Hausdorff_space X  regular_space X  normal_space X)
       quasi_components_of X = connected_components_of X"
proof (elim disjE)
  show "quasi_components_of X = connected_components_of X"
    if "finite (connected_components_of X)"
    unfolding quasi_eq_connected_components_of_inclusion
    using that open_in_finite_connected_components open_quasi_eq_connected_components_of by blast
  show "quasi_components_of X = connected_components_of X"
    if "finite (quasi_components_of X)"
    unfolding quasi_eq_connected_components_of_inclusion
    using that open_quasi_eq_connected_components_of openin_finite_quasi_components by blast 
  show "quasi_components_of X = connected_components_of X"
    if "locally_connected_space X"
    unfolding quasi_eq_connected_components_of_inclusion
    using that open_quasi_eq_connected_components_of openin_quasi_components_of_locally_connected_space by auto 
  show "quasi_components_of X = connected_components_of X"
    if "compact_space X  (Hausdorff_space X  regular_space X  normal_space X)"
  proof -
    show ?thesis
      unfolding quasi_eq_connected_components_of_alt
    proof (intro strip)
      fix C
      assume C: "C  quasi_components_of X"
      then have cloC: "closedin X C"
        by (simp add: closedin_quasi_components_of)
      have "normal_space X"
        using that compact_Hausdorff_or_regular_imp_normal_space by blast
      show "connectedin X C"
      proof (clarsimp simp add: connectedin_def connected_space_closedin_eq closedin_closed_subtopology cloC closedin_subset [OF cloC])
        fix S T
        assume "S  C" and "closedin X S" and "S  T = {}" and SUT: "S  T = topspace X  C"
          and T: "T  C" "T  {}" and "closedin X T" 
        with normal_space X obtain U V where UV: "openin X U" "openin X V" "S  U" "T  V" "disjnt U V"
          by (meson disjnt_def normal_space_def)
        moreover have "compactin X (topspace X - (U  V))"
          using UV that by (intro closedin_compact_space closedin_diff openin_Un) auto
        ultimately have "separated_between X C (topspace X - (U  V))  disjnt C (topspace X - (U  V))"
          by (simp add: C  quasi_components_of X separated_between_quasi_component_compact)
        moreover have "disjnt C (topspace X - (U  V))"
          using UV SUT disjnt_def by fastforce
        ultimately have "separated_between X C (topspace X - (U  V))"
          by simp
        then obtain A B where "openin X A" "openin X B" "A  B = topspace X" "disjnt A B" "C  A" 
                        and subB: "topspace X - (U  V)  B"
          by (meson separated_between_def)
        have "B  U = topspace X - (A  V)"
        proof
          show "B  U  topspace X - A  V"
            using openin X U disjnt U V disjnt A B openin X B disjnt_iff openin_closedin_eq by fastforce
          show "topspace X - A  V  B  U"
            using A  B = topspace X subB by fastforce
        qed
        then have "closedin X (B  U)"
          using openin X V openin X A by auto
        then have "C  B  U  disjnt C (B  U)"
          using quasi_component_of_clopen_cases [OF C] openin X U openin X B by blast
        with UV show "S = {}"
          by (metis UnE C  A S  C T disjnt A B all_not_in_conv disjnt_Un2 disjnt_iff subset_eq)
      qed
    qed
  qed
qed


lemma quasi_eq_connected_component_of:
   "finite(connected_components_of X) 
      finite(quasi_components_of X) 
      locally_connected_space X 
      compact_space X  (Hausdorff_space X  regular_space X  normal_space X)
       quasi_component_of X x = connected_component_of X x"
  by (metis quasi_eq_connected_components_of quasi_eq_connected_components_of_pointwise_alt)


subsection‹Additional quasicomponent and continuum properties like Boundary Bumping›

lemma cut_wire_fence_theorem_gen:
  assumes "compact_space X" and X: "Hausdorff_space X  regular_space X  normal_space X"
    and S: "compactin X S" and T: "closedin X T"
    and dis: "C. connectedin X C  disjnt C S  disjnt C T"
  shows "separated_between X S T"
  proof -
  have "x  topspace X" if "x  S" and "T = {}" for x
    using that S compactin_subset_topspace by auto
  moreover have "separated_between X {x} {y}" if "x  S" and "y  T" for x y
  proof (cases "x  topspace X  y  topspace X")
    case True
    then have "¬ connected_component_of X x y"
      by (meson dis connected_component_of_def disjnt_iff that)
    with True X compact_space X show ?thesis
      by (metis quasi_component_nonseparated quasi_eq_connected_component_of)
  next
    case False
    then show ?thesis
      using S T compactin_subset_topspace closedin_subset that by blast
  qed
  ultimately show ?thesis
    using assms
    by (simp add: separated_between_pointwise_left separated_between_pointwise_right 
              closedin_compact_space closedin_subset)
qed

lemma cut_wire_fence_theorem:
   "compact_space X; Hausdorff_space X; closedin X S; closedin X T;
     C. connectedin X C  disjnt C S  disjnt C T
         separated_between X S T"
  by (simp add: closedin_compact_space cut_wire_fence_theorem_gen)

lemma separated_between_from_closed_subtopology:
  assumes XC: "separated_between (subtopology X C) S (X frontier_of C)" 
    and ST: "separated_between (subtopology X C) S T"
  shows "separated_between X S T"
proof -
  obtain U where clo: "closedin (subtopology X C) U" and ope: "openin (subtopology X C) U" 
             and "S  U" and sub: "X frontier_of C  T  topspace (subtopology X C) - U"
    by (meson assms separated_between separated_between_Un)
  then have "X frontier_of C  T  topspace X  C - U"
    by auto
  have "closedin X (topspace X  C)"
    by (metis XC frontier_of_restrict frontier_of_subset_eq inf_le1 separated_between_imp_subset topspace_subtopology)
  then have "closedin X U"
    by (metis clo closedin_closed_subtopology subtopology_restrict)
  moreover have "openin (subtopology X C) U  openin X U  U  C"
    using disjnt_iff sub by (force intro!: openin_subset_topspace_eq)
  with ope have "openin X U"
    by blast
  moreover have "T  topspace X - U"
    using ope openin_closedin_eq sub by auto
  ultimately show ?thesis
    using S  U separated_between by blast
qed

lemma separated_between_from_closed_subtopology_frontier:
   "separated_between (subtopology X T) S (X frontier_of T)
         separated_between X S (X frontier_of T)"
  using separated_between_from_closed_subtopology by blast

lemma separated_between_from_frontier_of_closed_subtopology:
  assumes "separated_between (subtopology X T) S (X frontier_of T)"
  shows "separated_between X S (topspace X - T)"
proof -
  have "disjnt S (topspace X - T)"
    using assms disjnt_iff separated_between_imp_subset by fastforce
  then show ?thesis
    by (metis Diff_subset assms frontier_of_complement separated_between_from_closed_subtopology separated_between_frontier_of_eq')
qed

lemma separated_between_compact_connected_component:
  assumes "locally_compact_space X" "Hausdorff_space X" 
    and C: "C  connected_components_of X" 
    and "compactin X C" "closedin X T" "disjnt C T"
  shows "separated_between X C T"
proof -
  have Csub: "C  topspace X"
    by (simp add: assms(4) compactin_subset_topspace)
  have "Hausdorff_space (subtopology X (topspace X - T))"
    using Hausdorff_space_subtopology assms(2) by blast
  moreover have "compactin (subtopology X (topspace X - T)) C"
    using assms Csub by (metis Diff_Int_distrib Diff_empty compact_imp_compactin_subtopology disjnt_def le_iff_inf)
  moreover have "locally_compact_space (subtopology X (topspace X - T))"
    by (meson assms closedin_def locally_compact_Hausdorff_imp_regular_space locally_compact_space_open_subset)
  ultimately
  obtain N L where "openin X N" "compactin X L" "closedin X L" "C  N" "N  L" 
    and Lsub: "L  topspace X - T"
    using Hausdorff_space X closedin X T
    apply (simp add: locally_compact_space_compact_closed_compact compactin_subtopology)
    by (meson closedin_def compactin_imp_closedin  openin_trans_full)
  then have disC: "disjnt C (topspace X - L)"
    by (meson DiffD2 disjnt_iff subset_iff)
  have "separated_between (subtopology X L) C (X frontier_of L)"
  proof (rule cut_wire_fence_theorem)
    show "compact_space (subtopology X L)"
      by (simp add: compactin X L compact_space_subtopology)
    show "Hausdorff_space (subtopology X L)"
      by (simp add: Hausdorff_space_subtopology Hausdorff_space X)
    show "closedin (subtopology X L) C"
      by (meson C  N N  L Hausdorff_space X compactin X C closedin_subset_topspace compactin_imp_closedin subset_trans)
    show "closedin (subtopology X L) (X frontier_of L)"
      by (simp add: closedin X L closedin_frontier_of closedin_subset_topspace frontier_of_subset_closedin)
    show "disjnt D C  disjnt D (X frontier_of L)"
      if "connectedin (subtopology X L) D" for D 
    proof (rule ccontr)
      assume "¬ (disjnt D C  disjnt D (X frontier_of L))"
      moreover have "connectedin X D"
        using connectedin_subtopology that by blast
      ultimately show False
        using that connected_components_of_maximal [of C X D] C
        apply (simp add: disjnt_iff)
        by (metis Diff_eq_empty_iff C  N N  L openin X N disjoint_iff frontier_of_openin_straddle_Int(2) subsetD)
    qed
  qed
  then have "separated_between X (X frontier_of C) (topspace X - L)"
    using separated_between_from_frontier_of_closed_subtopology separated_between_frontier_of_eq by blast
  with closedin X T  
    separated_between_frontier_of [OF Csub disC] 
  show ?thesis
    unfolding separated_between by (smt (verit) Diff_iff Lsub closedin_subset subset_iff)
qed

lemma wilder_locally_compact_component_thm:
  assumes "locally_compact_space X" "Hausdorff_space X" 
    and "C  connected_components_of X" "compactin X C" "openin X W" "C  W"
  obtains U V where "openin X U" "openin X V" "disjnt U V" "U  V = topspace X" "C  U" "U  W"
proof -
  have "closedin X (topspace X - W)"
    using openin X W by blast
  moreover have "disjnt C (topspace X - W)"
    using C  W disjnt_def by fastforce
  ultimately have "separated_between X C (topspace X - W)"
    using separated_between_compact_connected_component assms by blast
  then show thesis
    by (smt (verit, del_insts) DiffI disjnt_iff openin_subset separated_between_def subset_iff that)
qed

lemma compact_quasi_eq_connected_components_of:
  assumes "locally_compact_space X" "Hausdorff_space X" "compactin X C"
  shows "C  quasi_components_of X  C  connected_components_of X"
proof -
  have "compactin X (connected_component_of_set X x)" 
    if "x  topspace X" "compactin X (quasi_component_of_set X x)" for x
  proof (rule closed_compactin)
    show "compactin X (quasi_component_of_set X x)"
      by (simp add: that)
    show "connected_component_of_set X x  quasi_component_of_set X x"
      by (simp add: connected_component_subset_quasi_component_of)
    show "closedin X (connected_component_of_set X x)"
      by (simp add: closedin_connected_component_of)
  qed
  moreover have "connected_component_of X x = quasi_component_of X x"
    if §: "x  topspace X" "compactin X (connected_component_of_set X x)" for x
  proof -
    have "y. connected_component_of X x y  quasi_component_of X x y"
      by (simp add: connected_imp_quasi_component_of)
    moreover have False if non: "¬ connected_component_of X x y" and quasi: "quasi_component_of X x y" for y
    proof -
      have "y  topspace X"
        by (meson quasi_component_of_equiv that)
      then have "closedin X {y}"
        by (simp add: Hausdorff_space X compactin_imp_closedin)
      moreover have "disjnt (connected_component_of_set X x) {y}"
        by (simp add: non)
      moreover have "¬ separated_between X (connected_component_of_set X x) {y}"
        using § quasi separated_between_pointwise_left 
        by (fastforce simp: quasi_component_nonseparated connected_component_of_refl)
      ultimately show False
        using assms by (metis § connected_component_in_connected_components_of separated_between_compact_connected_component)
    qed
    ultimately show ?thesis
      by blast
  qed
  ultimately show ?thesis
    using compactin X C unfolding connected_components_of_def image_iff quasi_components_of_def by metis
qed


lemma boundary_bumping_theorem_closed_gen:
  assumes "connected_space X" "locally_compact_space X" "Hausdorff_space X" "closedin X S" 
    "S  topspace X" and C: "compactin X C" "C  connected_components_of (subtopology X S)"
  shows "C  X frontier_of S  {}"
proof 
  assume §: "C  X frontier_of S = {}"
  consider "C  {}" "X frontier_of S  topspace X" | "C  topspace X" "S = {}"
    using C by (metis frontier_of_subset_topspace nonempty_connected_components_of)
  then show False
  proof cases
    case 1
    have "separated_between (subtopology X S) C (X frontier_of S)"
    proof (rule separated_between_compact_connected_component)
      show "compactin (subtopology X S) C"
        using C compact_imp_compactin_subtopology connected_components_of_subset by fastforce
      show "closedin (subtopology X S) (X frontier_of S)"
        by (simp add: closedin X S closedin_frontier_of closedin_subset_topspace frontier_of_subset_closedin)
      show "disjnt C (X frontier_of S)"
        using § by (simp add: disjnt_def)
    qed (use assms Hausdorff_space_subtopology locally_compact_space_closed_subset in auto)
    then have "separated_between X C (X frontier_of S)"
      using separated_between_from_closed_subtopology by auto
    then have "X frontier_of S = {}"
      using C  {} connected_space X connected_space_separated_between by blast
    moreover have "C  S"
      using C connected_components_of_subset by fastforce
    ultimately show False
      using 1 assms by (metis closedin_subset connected_space_eq_frontier_eq_empty subset_empty)
  next
    case 2
    then show False
      using C connected_components_of_eq_empty by fastforce
  qed
qed

lemma boundary_bumping_theorem_closed:
  assumes "connected_space X" "compact_space X" "Hausdorff_space X" "closedin X S" 
          "S  topspace X" "C  connected_components_of(subtopology X S)"
  shows "C  X frontier_of S  {}"
  by (meson assms boundary_bumping_theorem_closed_gen closedin_compact_space closedin_connected_components_of
            closedin_trans_full compact_imp_locally_compact_space)


lemma intermediate_continuum_exists:
  assumes "connected_space X" "locally_compact_space X" "Hausdorff_space X" 
    and C: "compactin X C" "connectedin X C" "C  {}" "C  topspace X"
    and U: "openin X U" "C  U"
  obtains D where "compactin X D" "connectedin X D" "C  D" "D  U"
proof -
  have "C  topspace X"
    by (simp add: C compactin_subset_topspace)
  with C obtain a where a: "a  topspace X" "a  C"
    by blast
  moreover have "compactin (subtopology X (U - {a})) C"
    by (simp add: C U a compact_imp_compactin_subtopology subset_Diff_insert)
  moreover have "Hausdorff_space (subtopology X (U - {a}))"
    using Hausdorff_space_subtopology assms(3) by blast
  moreover
  have "locally_compact_space (subtopology X (U - {a}))"
    by (rule locally_compact_space_open_subset)
       (auto simp: locally_compact_Hausdorff_imp_regular_space open_in_Hausdorff_delete assms)
  ultimately obtain V K where V: "openin X V" "a  V" "V  U" and K: "compactin X K" "a  K" "K  U" 
    and cloK: "closedin (subtopology X (U - {a})) K" and "C  V" "V  K"
    using locally_compact_space_compact_closed_compact [of "subtopology X (U - {a})"] assms
    by (smt (verit, del_insts) Diff_empty compactin_subtopology open_in_Hausdorff_delete openin_open_subtopology subset_Diff_insert)
  then obtain D where D: "D  connected_components_of (subtopology X K)" and "C  D"
    using C
    by (metis compactin_subset_topspace connected_component_in_connected_components_of        
              connected_component_of_maximal connectedin_subtopology subset_empty subset_eq topspace_subtopology_subset)
  show thesis
  proof
    have cloD: "closedin (subtopology X K) D"
      by (simp add: D closedin_connected_components_of)
    then have XKD: "compactin (subtopology X K) D"
      by (simp add: K closedin_compact_space compact_space_subtopology)
    then show "compactin X D"
      using compactin_subtopology_imp_compact by blast
    show "connectedin X D"
      using D connectedin_connected_components_of connectedin_subtopology by blast
    have "K  topspace X"
      using K a by blast
    moreover have "V  X interior_of K"
      by (simp add: openin X V V  K interior_of_maximal)
    ultimately have "C  D"
      using boundary_bumping_theorem_closed_gen [of X K C] D C  V 
      by (auto simp add: assms K compactin_imp_closedin frontier_of_def)
    then show "C  D"
      using C  D by blast
    have "D  U"
      using K(3) closedin (subtopology X K) D closedin_imp_subset by blast
    moreover have "D  U"
      using K XKD C  D assms
      by (metis K  topspace X cloD closedin_imp_subset compactin_imp_closedin connected_space_clopen_in
                inf_bot_left inf_le2 subset_antisym)
    ultimately
    show "D  U" by blast
  qed
qed

lemma boundary_bumping_theorem_gen:
  assumes X: "connected_space X" "locally_compact_space X" "Hausdorff_space X" 
   and "S  topspace X" and C: "C  connected_components_of(subtopology X S)" 
   and compC: "compactin X (X closure_of C)"
 shows "X frontier_of C  X frontier_of S  {}"
proof -
  have Csub: "C  topspace X" "C  S" and "connectedin X C"
    using C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology
    by fastforce+
  have "C  {}"
    using C nonempty_connected_components_of by blast
  obtain "X interior_of C  X interior_of S" "X closure_of C  X closure_of S"
    by (simp add: Csub closure_of_mono interior_of_mono)
  moreover have False if "X closure_of C  X interior_of S"
  proof -
    have "X closure_of C = C"
      by (meson C closedin_connected_component_of_subtopology closure_of_eq interior_of_subset order_trans that)
    with that have "C  X interior_of S"
      by simp
    then obtain D where  "compactin X D" and "connectedin X D" and "C  D" and "D  X interior_of S"
      using intermediate_continuum_exists assms  X closure_of C = C compC Csub
      by (metis C  {} connectedin X C openin_interior_of psubsetE)
    then have "D  C"
      by (metis C C  {} connected_components_of_maximal connectedin_subtopology disjnt_def inf.orderE interior_of_subset order_trans psubsetE)
    then show False
      using C  D by blast
  qed
  ultimately show ?thesis
    by (smt (verit, ccfv_SIG) DiffI disjoint_iff_not_equal frontier_of_def subset_eq)
qed

lemma boundary_bumping_theorem:
   "connected_space X; compact_space X; Hausdorff_space X; S  topspace X; 
     C  connected_components_of(subtopology X S)
     X frontier_of C  X frontier_of S  {}"
  by (simp add: boundary_bumping_theorem_gen closedin_compact_space compact_imp_locally_compact_space)

subsection ‹Compactly generated spaces (k-spaces)›

text ‹These don't have to be Hausdorff›

definition k_space where
  "k_space X 
    S. S  topspace X  
        (closedin X S  (K. compactin X K  closedin (subtopology X K) (K  S)))"

lemma k_space:
   "k_space X 
    (S. S  topspace X 
         (K. compactin X K  closedin (subtopology X K) (K  S))  closedin X S)"
  by (metis closedin_subtopology inf_commute k_space_def)

lemma k_space_open:
   "k_space X 
    (S. S  topspace X 
         (K. compactin X K  openin (subtopology X K) (K  S))  openin X S)"
proof -
  have "openin X S"
    if "k_space X" "S  topspace X"
      and "K. compactin X K  openin (subtopology X K) (K  S)" for S
    using that unfolding k_space openin_closedin_eq
    by (metis Diff_Int_distrib2 Diff_subset inf_commute topspace_subtopology)
  moreover have "k_space X"
    if "S. S  topspace X  (K. compactin X K  openin (subtopology X K) (K  S))  openin X S"
    unfolding k_space openin_closedin_eq
    by (simp add: Diff_Int_distrib closedin_def inf_commute that)
  ultimately show ?thesis
    by blast
qed

lemma k_space_alt:
   "k_space X 
    (S. S  topspace X
         (openin X S  (K. compactin X K  openin (subtopology X K) (K  S))))"
  by (meson k_space_open openin_subtopology_Int2)

lemma k_space_quotient_map_image:
  assumes q: "quotient_map X Y q" and X: "k_space X"
  shows "k_space Y"
  unfolding k_space
proof clarify
  fix S
  assume "S  topspace Y" and S: "K. compactin Y K  closedin (subtopology Y K) (K  S)"
  then have iff: "closedin X {x  topspace X. q x  S}  closedin Y S"
    using q quotient_map_closedin by fastforce
  have "closedin (subtopology X K) (K  {x  topspace X. q x  S})" if "compactin X K" for K
  proof -
    have "{x  topspace X. q x  q ` K}  K = K"
      using compactin_subset_topspace that by blast
    then have *: "subtopology X K = subtopology (subtopology X {x  topspace X. q x  q ` K}) K"
      by (simp add: subtopology_subtopology)
    have **: "K  {x  topspace X. q x  S} =
              K  {x  topspace (subtopology X {x  topspace X. q x  q ` K}). q x  q ` K  S}"
      by auto
    have "K  topspace X"
      by (simp add: compactin_subset_topspace that)
    show ?thesis
      unfolding * **
    proof (intro closedin_continuous_map_preimage closedin_subtopology_Int_closed)
      show "continuous_map (subtopology X {x  topspace X. q x  q ` K}) (subtopology Y (q ` K)) q"
        by (auto simp add: continuous_map_in_subtopology continuous_map_from_subtopology q quotient_imp_continuous_map)
      show "closedin (subtopology Y (q ` K)) (q ` K  S)"
        by (meson S image_compactin q quotient_imp_continuous_map that)
    qed
  qed
  then have "closedin X {x  topspace X. q x  S}"
    by (metis (no_types, lifting) X k_space mem_Collect_eq subsetI)
  with iff show "closedin Y S" by simp
qed

lemma k_space_retraction_map_image:
   "retraction_map X Y r; k_space X  k_space Y"
  using k_space_quotient_map_image retraction_imp_quotient_map by blast

lemma homeomorphic_k_space:
   "X homeomorphic_space Y  k_space X  k_space Y"
  by (meson homeomorphic_map_def homeomorphic_space homeomorphic_space_sym k_space_quotient_map_image)

lemma k_space_perfect_map_image:
   "k_space X; perfect_map X Y f  k_space Y"
  using k_space_quotient_map_image perfect_imp_quotient_map by blast

lemma locally_compact_imp_k_space:
  assumes "locally_compact_space X"
  shows "k_space X"
  unfolding k_space
proof clarify
  fix S
  assume "S  topspace X" and S: "K. compactin X K  closedin (subtopology X K) (K  S)"
  have False if non: "¬ (X closure_of S  S)"
  proof -
    obtain x where "x  X closure_of S" "x  S"
      using non by blast
    then have "x  topspace X"
      by (simp add: in_closure_of)
    then obtain K U where "openin X U" "compactin X K" "x  U" "U  K"
      by (meson assms locally_compact_space_def)
    then show False
      using x  X closure_of S  openin_Int_closure_of_eq [OF openin X U]
      by (smt (verit, ccfv_threshold) Int_iff S x  S closedin_Int_closure_of inf.orderE inf_assoc)
  qed
  then show "closedin X S"
    using S S  topspace X closure_of_subset_eq by blast
qed

lemma compact_imp_k_space:
   "compact_space X  k_space X"
  by (simp add: compact_imp_locally_compact_space locally_compact_imp_k_space)

lemma k_space_discrete_topology: "k_space(discrete_topology U)"
  by (simp add: k_space_open)

lemma k_space_closed_subtopology:
  assumes "k_space X" "closedin X C"
  shows "k_space (subtopology X C)"
unfolding k_space compactin_subtopology
proof clarsimp
  fix S
  assume Ssub: "S  topspace X" "S  C"
      and S: "K. compactin X K  K  C  closedin (subtopology (subtopology X C) K) (K  S)"
  have "closedin (subtopology X K) (K  S)" if "compactin X K" for K
  proof -
    have "closedin (subtopology (subtopology X C) (K  C)) ((K  C)  S)"
      by (simp add: S closedin X C compact_Int_closedin that)
    then show ?thesis
      using closedin X C Ssub by (auto simp add: closedin_subtopology)
  qed
  then show "closedin (subtopology X C) S"
    by (metis Ssub k_space X closedin_subset_topspace k_space_def)
qed

lemma k_space_subtopology:
  assumes 1: "T. T  topspace X; T  S;
                   K. compactin X K  closedin (subtopology X (K  S)) (K  T)  closedin (subtopology X S) T"
  assumes 2: "K. compactin X K  k_space(subtopology X (K  S))"
  shows "k_space (subtopology X S)"
  unfolding k_space
proof (intro conjI strip)
  fix U
  assume §: "U  topspace (subtopology X S)  (K. compactin (subtopology X S) K  closedin (subtopology (subtopology X S) K) (K  U))"
  have "closedin (subtopology X (K  S)) (K  U)" if "compactin X K" for K
  proof -
    have "K  U  topspace (subtopology X (K  S))"
      using "§" by auto
    moreover
    have "K'. compactin (subtopology X (K  S)) K'  closedin (subtopology (subtopology X (K  S)) K') (K'  K  U)"
      by (metis "§" compactin_subtopology inf.orderE inf_commute subtopology_subtopology)
    ultimately show ?thesis
      by (metis (no_types, opaque_lifting) "2" inf.assoc k_space_def that)
  qed
  then show "closedin (subtopology X S) U"
    using "1" § by auto
qed

lemma k_space_subtopology_open:
  assumes 1: "T. T  topspace X; T  S;
                    K. compactin X K  openin (subtopology X (K  S)) (K  T)  openin (subtopology X S) T"
  assumes 2: "K. compactin X K  k_space(subtopology X (K  S))"
  shows "k_space (subtopology X S)"
  unfolding k_space_open
proof (intro conjI strip)
  fix U
  assume §: "U  topspace (subtopology X S)  (K. compactin (subtopology X S) K  openin (subtopology (subtopology X S) K) (K  U))"
  have "openin (subtopology X (K  S)) (K  U)" if "compactin X K" for K
  proof -
    have "K  U  topspace (subtopology X (K  S))"
      using "§" by auto
    moreover
    have "K'. compactin (subtopology X (K  S)) K'  openin (subtopology (subtopology X (K  S)) K') (K'  K  U)"
      by (metis "§" compactin_subtopology inf.orderE inf_commute subtopology_subtopology)
    ultimately show ?thesis
      by (metis (no_types, opaque_lifting) "2" inf.assoc k_space_open that)
  qed
  then show "openin (subtopology X S) U"
    using "1" § by auto
qed


lemma k_space_open_subtopology_aux:
  assumes "kc_space X" "compact_space X" "openin X V"
  shows "k_space (subtopology X V)"
proof (clarsimp simp: k_space subtopology_subtopology compactin_subtopology Int_absorb1)
  fix S
  assume "S  topspace X"
    and "S  V"
    and S: "K. compactin X K  K  V  closedin (subtopology X K) (K  S)"
  then have "V  topspace X"
    using assms openin_subset by blast
  have "S = V  ((topspace X - V)  S)"
    using S  V by auto
  moreover have "closedin (subtopology X V) (V  ((topspace X - V)  S))"
  proof (intro closedin_subtopology_Int_closed compactin_imp_closedin_gen kc_space X)
    show "compactin X (topspace X - V  S)"
      unfolding compactin_def
    proof (intro conjI strip)
      show "topspace X - V  S  topspace X"
        by (simp add: S  topspace X)
      fix 𝒰
      assume 𝒰: "Ball 𝒰 (openin X)  topspace X - V  S  𝒰"
      moreover
      have "compactin X (topspace X - V)"
        using assms closedin_compact_space by blast
      ultimately obtain 𝒢 where "finite 𝒢" "𝒢  𝒰" and 𝒢: "topspace X - V  𝒢"
        unfolding compactin_def using V  topspace X by (metis le_sup_iff)
      then have "topspace X - 𝒢  V"
        by blast
      then have "closedin (subtopology X (topspace X - 𝒢)) ((topspace X - 𝒢)  S)"
        by (meson S 𝒰 𝒢  𝒰 compact_space X closedin_compact_space openin_Union openin_closedin_eq subset_iff)
      then have "compactin X ((topspace X - 𝒢)  S)"
        by (meson 𝒰 𝒢  𝒰compact_space X closedin_compact_space closedin_trans_full openin_Union openin_closedin_eq subset_iff)
      then obtain  where "finite " "  𝒰" "(topspace X - 𝒢)  S  "
        unfolding compactin_def by (smt (verit, best) 𝒰 inf_le2 subset_trans sup.boundedE)
      with 𝒢 have "topspace X - V  S  (𝒢  )"
        using S  topspace X by auto
      then show ". finite     𝒰  topspace X - V  S  "
        by (metis 𝒢  𝒰   𝒰 finite 𝒢 finite  finite_Un le_sup_iff)
    qed
  qed
  ultimately show "closedin (subtopology X V) S"
    by metis
qed


lemma k_space_open_subtopology:
  assumes X: "kc_space X  Hausdorff_space X  regular_space X" and "k_space X" "openin X S"
  shows "k_space(subtopology X S)"
proof (rule k_space_subtopology_open)
  fix T
  assume "T  topspace X"
    and "T  S"
    and T: "K. compactin X K  openin (subtopology X (K  S)) (K  T)"
  have "openin (subtopology X K) (K  T)" if "compactin X K" for K
    by (smt (verit, ccfv_threshold) T assms(3) inf_assoc inf_commute openin_Int openin_subtopology that)
  then show "openin (subtopology X S) T"
    by (metis T  S T  topspace X assms(2) k_space_alt subset_openin_subtopology)
next
  fix K
  assume "compactin X K"
  then have KS: "openin (subtopology X K) (K  S)"
    by (simp add: openin X S openin_subtopology_Int2)
  have XK: "compact_space (subtopology X K)"
    by (simp add: compactin X K compact_space_subtopology)
  show "k_space (subtopology X (K  S))"
    using X
  proof (rule disjE)
    assume "kc_space X"
    then show "k_space (subtopology X (K  S))"
      using k_space_open_subtopology_aux [of "subtopology X K" "K  S"]
      by (simp add: KS XK kc_space_subtopology subtopology_subtopology)
  next
    assume "Hausdorff_space X  regular_space X"
    then have "locally_compact_space (subtopology (subtopology X K) (K  S))"
      using locally_compact_space_open_subset Hausdorff_space_subtopology KS XK 
        compact_imp_locally_compact_space regular_space_subtopology by blast
    then show "k_space (subtopology X (K  S))"
      by (simp add: locally_compact_imp_k_space subtopology_subtopology)
  qed
qed

lemma k_kc_space_subtopology:
   "k_space X; kc_space X; openin X S  closedin X S  k_space(subtopology X S)  kc_space(subtopology X S)"
  by (metis k_space_closed_subtopology k_space_open_subtopology kc_space_subtopology)


lemma k_space_as_quotient_explicit:
  "k_space X  quotient_map (sum_topology (subtopology X) {K. compactin X K}) X snd"
proof -
  have [simp]: "{x  topspace X. x  K  x  U} = K  U" if "U  topspace X" for K U
    using that by blast
  show "?thesis"
    apply (simp add: quotient_map_def openin_sum_topology snd_image_Sigma k_space_alt)
    by (smt (verit, del_insts) Union_iff compactin_sing inf.orderE mem_Collect_eq singletonI subsetI)
qed

lemma k_space_as_quotient:
  fixes X :: "'a topology"
  shows "k_space X  (q. Y:: ('a set * 'a) topology. locally_compact_space Y  quotient_map Y X q)" 
         (is "?lhs=?rhs")
proof
  show "k_space X" if ?rhs
    using that k_space_quotient_map_image locally_compact_imp_k_space by blast 
next
  assume "k_space X"
  show ?rhs
  proof (intro exI conjI)
    show "locally_compact_space (sum_topology (subtopology X) {K. compactin X K})"
      by (simp add: compact_imp_locally_compact_space compact_space_subtopology locally_compact_space_sum_topology)
    show "quotient_map (sum_topology (subtopology X) {K. compactin X K}) X snd"
      using k_space X k_space_as_quotient_explicit by blast
  qed
qed

lemma k_space_prod_topology_left:
  assumes X: "locally_compact_space X" "Hausdorff_space X  regular_space X" and "k_space Y"
  shows "k_space (prod_topology X Y)"
proof -
  obtain q and Z :: "('b set * 'b) topology" where "locally_compact_space Z" and q: "quotient_map Z Y q"
    using k_space Y k_space_as_quotient by blast
  then show ?thesis
    using quotient_map_prod_right [OF X q] X k_space_quotient_map_image locally_compact_imp_k_space 
          locally_compact_space_prod_topology by blast
qed

lemma k_space_prod_topology_right:
  assumes "k_space X" and Y: "locally_compact_space Y" "Hausdorff_space Y  regular_space Y"
  shows "k_space (prod_topology X Y)"
  using assms homeomorphic_k_space homeomorphic_space_prod_topology_swap k_space_prod_topology_left by blast


lemma continuous_map_from_k_space:
  assumes "k_space X" and f: "K. compactin X K  continuous_map(subtopology X K) Y f"
  shows "continuous_map X Y f"
proof -
  have "x. x  topspace X  f x  topspace Y"
    by (metis compactin_absolute compactin_sing f image_compactin image_empty image_insert)
  moreover have "closedin X {x  topspace X. f x  C}" if "closedin Y C" for C
  proof -
    have "{x  topspace X. f x  C}  topspace X"
      by fastforce
    moreover 
    have eq: "K  {x  topspace X. f x  C} = {x. x  topspace(subtopology X K)  f x  (f ` K  C)}" for K
      by auto
    have "closedin (subtopology X K) (K  {x  topspace X. f x  C})" if "compactin X K" for K
      unfolding eq
    proof (rule closedin_continuous_map_preimage)
      show "continuous_map (subtopology X K) (subtopology Y (f`K)) f"
        by (simp add: continuous_map_in_subtopology f image_mono that)
      show "closedin (subtopology Y (f`K)) (f ` K  C)"
        using closedin Y C closedin_subtopology by blast
    qed
    ultimately show ?thesis
      using k_space X k_space by blast
  qed
  ultimately show ?thesis
    by (simp add: continuous_map_closedin)
qed

lemma closed_map_into_k_space:
  assumes "k_space Y" and fim: "f  (topspace X)  topspace Y"
    and f: "K. compactin Y K
                 closed_map(subtopology X {x  topspace X. f x  K}) (subtopology Y K) f"
  shows "closed_map X Y f"
  unfolding closed_map_def
proof (intro strip)
  fix C
  assume "closedin X C"
  have "closedin (subtopology Y K) (K  f ` C)"
    if "compactin Y K" for K
  proof -
    have eq: "K  f ` C = f ` ({x  topspace X. f x  K}  C)"
      using closedin X C closedin_subset by auto
    show ?thesis
      unfolding eq
      by (metis (no_types, lifting) closedin X C closed_map_def closedin_subtopology f inf_commute that)
  qed
  then show "closedin Y (f ` C)"
    using k_space Y unfolding k_space
    by (meson closedin X C closedin_subset order.trans fim funcset_image subset_image_iff)
qed


text ‹Essentially the same proof›
lemma open_map_into_k_space:
  assumes "k_space Y" and fim: "f  (topspace X)  topspace Y"
    and f: "K. compactin Y K
                  open_map (subtopology X {x  topspace X. f x  K}) (subtopology Y K) f"
  shows "open_map X Y f"
  unfolding open_map_def
proof (intro strip)
  fix C
  assume "openin X C"
  have "openin (subtopology Y K) (K  f ` C)"
    if "compactin Y K" for K
  proof -
    have eq: "K  f ` C = f ` ({x  topspace X. f x  K}  C)"
      using openin X C openin_subset by auto
    show ?thesis
      unfolding eq
      by (metis (no_types, lifting) openin X C open_map_def openin_subtopology f inf_commute that)
  qed
  then show "openin Y (f ` C)"
    using k_space Y unfolding k_space_open
    by (meson openin X C openin_subset order.trans fim funcset_image subset_image_iff)
qed

lemma quotient_map_into_k_space:
  fixes f :: "'a  'b"
  assumes "k_space Y" and cmf: "continuous_map X Y f" 
    and fim: "f ` (topspace X) = topspace Y"
    and f: "k. compactin Y k
                  quotient_map (subtopology X {x  topspace X. f x  k})
                                  (subtopology Y k) f"
  shows "quotient_map X Y f"
proof -
  have "closedin Y C"
    if "C  topspace Y" and K: "closedin X {x  topspace X. f x  C}" for C
  proof -
    have "closedin (subtopology Y K) (K  C)" if "compactin Y K" for K
    proof -
      define Kf where "Kf  {x  topspace X. f x  K}"
      have *: "K  C  topspace Y  K  C  K"
        using C  topspace Y by blast
      then have eq: "closedin (subtopology X Kf) (Kf  {x  topspace X. f x  C}) =
                 closedin (subtopology Y K) (K  C)"
        using f [OF that] * unfolding quotient_map_closedin Kf_def
        by (smt (verit, ccfv_SIG) Collect_cong Int_def compactin_subset_topspace mem_Collect_eq that topspace_subtopology topspace_subtopology_subset)
      have dd: "{x  topspace X  Kf. f x  K  C} = Kf  {x  topspace X. f x  C}"
        by (auto simp add: Kf_def)
      have "closedin (subtopology X Kf) {x  topspace X. x  Kf  f x  K  f x  C}"
        using K closedin_subtopology by (fastforce simp add: Kf_def)
      with K closedin_subtopology_Int_closed eq show ?thesis
        by blast
    qed
    then show ?thesis 
      using k_space Y that unfolding k_space by blast
  qed
  moreover have "closedin X {x  topspace X. f x  K}"
    if "K  topspace Y" "closedin Y K" for K
    using that cmf continuous_map_closedin by fastforce
  ultimately show ?thesis
    unfolding quotient_map_closedin using fim by blast
qed

lemma quotient_map_into_k_space_eq:
  assumes "k_space Y" "kc_space Y"
  shows "quotient_map X Y f 
         continuous_map X Y f  f ` (topspace X) = topspace Y 
         (K. compactin Y K
               quotient_map (subtopology X {x  topspace X. f x  K}) (subtopology Y K) f)"
  using assms
  by (auto simp: kc_space_def intro: quotient_map_into_k_space quotient_map_restriction
       dest: quotient_imp_continuous_map quotient_imp_surjective_map)

lemma open_map_into_k_space_eq:
  assumes "k_space Y"
  shows "open_map X Y f 
         f  (topspace X)  topspace Y 
         (k. compactin Y k
               open_map (subtopology X {x  topspace X. f x  k}) (subtopology Y k) f)"
  using assms open_map_imp_subset_topspace open_map_into_k_space open_map_restriction by fastforce

lemma closed_map_into_k_space_eq:
  assumes "k_space Y"
  shows "closed_map X Y f 
         f  (topspace X)  topspace Y 
         (k. compactin Y k
               closed_map (subtopology X {x  topspace X. f x  k}) (subtopology Y k) f)"
       (is "?lhs  ?rhs")
proof
  show "?lhs  ?rhs"
    by (simp add: closed_map_imp_subset_topspace closed_map_restriction)
  show "?rhs  ?lhs"
    by (simp add: assms closed_map_into_k_space)
qed

lemma proper_map_into_k_space:
  assumes "k_space Y" and fim: "f  (topspace X)  topspace Y"
    and f: "K. compactin Y K
                  proper_map (subtopology X {x  topspace X. f x  K})
                                (subtopology Y K) f"
  shows "proper_map X Y f"
proof -
  have "closed_map X Y f"
    by (meson assms closed_map_into_k_space fim proper_map_def)
  with f topspace_subtopology_subset show ?thesis
    apply (simp add: proper_map_alt)
    by (smt (verit, best) Collect_cong compactin_absolute)
qed

lemma proper_map_into_k_space_eq:
  assumes "k_space Y"
  shows "proper_map X Y f 
         f  (topspace X)  topspace Y 
         (K. compactin Y K
               proper_map (subtopology X {x  topspace X. f x  K}) (subtopology Y K) f)"
         (is "?lhs  ?rhs")
proof
  show "?lhs  ?rhs"
    by (simp add: proper_map_imp_subset_topspace proper_map_restriction)
  show "?rhs  ?lhs"
    by (simp add: assms funcset_image proper_map_into_k_space)
qed

lemma compact_imp_proper_map:
  assumes "k_space Y" "kc_space Y" and fim: "f  (topspace X)  topspace Y" 
    and f: "continuous_map X Y f  kc_space X" 
    and comp: "K. compactin Y K  compactin X {x  topspace X. f x  K}"
  shows "proper_map X Y f"
proof (rule compact_imp_proper_map_gen)
  fix S
  assume "S  topspace Y"
      and "K. compactin Y K  compactin Y (S  K)"
  with assms show "closedin Y S"
    by (simp add: closedin_subset_topspace inf_commute k_space kc_space_def)
qed (use assms in auto)

lemma proper_eq_compact_map:
  assumes "k_space Y" "kc_space Y" 
    and f: "continuous_map X Y f  kc_space X" 
  shows  "proper_map X Y f 
             f  (topspace X)  topspace Y 
             (K. compactin Y K  compactin X {x  topspace X. f x  K})"
         (is "?lhs  ?rhs")
proof
  show "?lhs  ?rhs"
    using k_space Y compactin_proper_map_preimage proper_map_into_k_space_eq by blast
qed (use assms compact_imp_proper_map in auto)

lemma compact_imp_perfect_map:
  assumes "k_space Y" "kc_space Y" and "f ` (topspace X) = topspace Y" 
    and "continuous_map X Y f" 
    and "K. compactin Y K  compactin X {x  topspace X. f x  K}"
  shows "perfect_map X Y f"
  by (simp add: assms compact_imp_proper_map perfect_map_def flip: image_subset_iff_funcset)

end