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_quotient_map_image:
   "⟦quotient_map X X' q; connected_space X⟧ ⟹ connected_space X'"
  by (metis connectedin_continuous_map_image connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map)

lemma connected_space_retraction_map_image:
   "⟦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 ⊆ (⋃i∈K. U i)"
      using assms U unfolding compactin_def by (smt (verit) finite_subset_image imageE)
    show ?thesis
      unfolding separated_between
    proof (intro conjI exI)
      have "⋀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

thm connected_space_iff_components_eq

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'))"
proof -
  have "C ≠ {}"
    using nonempty_connected_components_of assms by blast
  with assms show ?thesis
    by (metis disjnt_self_iff_empty pairwiseD pairwise_disjoint_connected_components_of)
qed

lemma connected_components_of_overlap:
   "⟦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 i∈I. connected_component_of_set (X i) (x i))"
    if xX: "⋀i. i∈I ⟹ 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 ∈ (Π i∈I. connected_component_of_set (X i) (x i))"
        apply (simp add: connected_component_of_def Pi_def)
        by (metis connectedin_continuous_map_image continuous_map_product_projection imageI that)
      then show ?thesis
        using PiE_def ‹C ⊆ extensional I› by fastforce
    qed
  qed
  with True show ?thesis
    by (simp add: PiE_iff)
next
  case False
  then show ?thesis
    apply (simp add: PiE_iff)
    by (smt (verit) Collect_empty_eq False PiE_eq_empty_iff PiE_iff connected_component_of_eq_empty)
qed


lemma connected_components_of_product_topology:
   "connected_components_of (product_topology X I) =
    {PiE I B |B. ∀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 = Pi⇩E I B" and
      "∀i∈I. ∃x∈topspace (X i). B i = connected_component_of_set (X i) x"
      by (force simp: connected_components_of_def connected_component_of_product_topology image_iff)
    then obtain f where
      f: "⋀i. i ∈ I ⟹ f i ∈ topspace (X i) ∧ B i = connected_component_of_set (X i) (f i)"
      by metis
    then have "(λi∈I. f i) ∈ ((Π⇩E i∈I. 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"
  using assms
  unfolding monotone_map_def connectedin_subtopology
  by (smt (verit, del_insts) Collect_cong Collect_empty_eq IntE IntI connectedin_empty image_subset_iff mem_Collect_eq subsetI topspace_subtopology)

lemma monotone_map_restriction:
  "monotone_map X Y f ∧ {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 XY: "{x}×{y} = {(x,y)}"
  by simp

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: XY 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" "∀x∈S. 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 "ℱ ≡ {Pi⇩E I U |U. finite {i ∈ I. U i ≠ topspace (X i)}
                        ∧ (∀i∈I. 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 ⊆ Pi⇩E 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 "∀i∈I. 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 ⊆ Pi⇩E I W"
          by (simp add: UC PI_def subset_PiE)
      qed
    qed
    then have "neighbourhood_base_of (closedin (product_topology X I)) (product_topology X I)"
      unfolding neighbourhood_base_of_topology_base [OF oo] by (force simp: ℱ_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 ∧ (∀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})"
    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" "∀x∈T. r x = x"
    by (meson retract_of_space_def)
  have "locally_compact_space (subtopology X T)"
    unfolding locally_compact_space_def openin_subtopology_alt
  proof clarsimp
    fix x
    assume "x ∈ 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 *: "(∀U∈U ` 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) ` Pi⇩E I V"
          by (metis ‹z ∈ Pi⇩E I V› empty_iff image_projection_PiE order_refl ‹i ∈ I›)
        also have "… ⊆ (λx. x i) ` C"
          using ‹U ⊆ C› ‹Pi⇩E 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 i∈I. 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) (Pi⇩E I U)"
        by (smt (verit) Collect_cong False R UC compactin_subspace openin_PiE_gen subset_antisym subtopology_topspace)
        show "compactin (product_topology X I) (Pi⇩E I C)"
          by (simp add: UC compactin_PiE)
      qed (use UC z in blast)+
    qed
  qed
qed

lemma locally_compact_space_sum_topology:
   "locally_compact_space (sum_topology X I) ⟷ (∀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 (⋃m≤n. X closure_of V m)"
        by (force intro: closedin_Union)
      then show "openin X (⋃n. U n - (⋃m≤n. X closure_of V m))"
        using U by blast
      have "⋀S n. closedin X (⋃m≤n. X closure_of U m)"
        by (force intro: closedin_Union)
      then show "openin X (⋃n. V n - (⋃m≤n. 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 - (⋃m≤n. 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 - (⋃m≤n. 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; ∀k≤m. x ∉ X closure_of U k⟧ ⟹ ∃k≤n. 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 - (⋃m≤n. X closure_of V m)) (⋃n. V n - (⋃m≤n. 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. (∀n≤N. 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 "∃x∈topspace 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 "∃x∈topspace 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 "∃y∈topspace 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

text ‹Essentially the same proof›
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)"
proof -
  obtain q and Z :: "('a set * 'a) topology" where "locally_compact_space Z" and q: "quotient_map Z X q"
    using ‹k_space X› k_space_as_quotient by blast
  then show ?thesis
    using quotient_map_prod_left [OF Y q] using Y k_space_quotient_map_image locally_compact_imp_k_space 
          locally_compact_space_prod_topology by blast
qed


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)"
       (is "?lhs=?rhs")
proof
  show "?lhs ⟹ ?rhs"
    by (simp add: open_map_imp_subset_topspace open_map_restriction)
  show "?rhs ⟹ ?lhs"
    by (simp add: assms open_map_into_k_space)
qed

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