Theory Abstract_Topological_Spaces

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

section ‹Various Forms of Topological Spaces›

theory Abstract_Topological_Spaces
  imports Lindelof_Spaces Locally Abstract_Euclidean_Space Sum_Topology FSigma
begin


subsection‹Connected topological spaces›

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

lemma connected_space_frontier_eq_empty:
   "connected_space X  S  topspace X
         (X frontier_of S = {}  S = {}  S = topspace X)"
  by (meson connected_space_eq_frontier_eq_empty frontier_of_empty frontier_of_topspace)

lemma connectedin_eq_subset_separated_union:
   "connectedin X C 
        C  topspace X  (S T. separatedin X S T  C  S  T  C  S  C  T)" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
  using connectedin_subset_topspace connectedin_subset_separated_union by blast
next
  assume ?rhs
  then show ?lhs
  by (metis closure_of_subset connectedin_separation dual_order.eq_iff inf.orderE separatedin_def sup.boundedE)
qed


lemma connectedin_clopen_cases:
   "connectedin X C; closedin X T; openin X T  C  T  disjnt C T"
  by (metis Diff_eq_empty_iff Int_empty_right clopenin_eq_frontier_of connectedin_Int_frontier_of disjnt_def)

lemma connected_space_retraction_map_image:
   "retraction_map X X' r; connected_space X  connected_space X'"
  using connected_space_quotient_map_image retraction_imp_quotient_map by blast

lemma connectedin_imp_perfect_gen:
  assumes X: "t1_space X" and S: "connectedin X S" and nontriv: "a. S = {a}"
  shows "S  X derived_set_of S"
unfolding derived_set_of_def
proof (intro subsetI CollectI conjI strip)
  show XS: "x  topspace X" if "x  S" for x
    using that S connectedin by fastforce 
  show "y. y  x  y  S  y  T"
    if "x  S" and "x  T  openin X T" for x T
  proof -
    have opeXx: "openin X (topspace X - {x})"
      by (meson X openin_topspace t1_space_openin_delete_alt)
    moreover
    have "S  T  (topspace X - {x})"
      using XS that(2) by auto
    moreover have "(topspace X - {x})  S  {}"
      by (metis Diff_triv S connectedin double_diff empty_subsetI inf_commute insert_subsetI nontriv that(1))
    ultimately show ?thesis
      using that connectedinD [OF S, of T "topspace X - {x}"]
      by blast
  qed
qed

lemma connectedin_imp_perfect:
  "Hausdorff_space X; connectedin X S; a. S = {a}  S  X derived_set_of S"
  by (simp add: Hausdorff_imp_t1_space connectedin_imp_perfect_gen)



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

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

lemma separated_between_alt:
   "separated_between X S T 
        (U V. closedin X U  closedin X V  U  V = topspace X  disjnt U V  S  U  T  V)"
  unfolding separated_between_def
  by (metis separatedin_open_sets separation_closedin_Un_gen subtopology_topspace 
            separatedin_closed_sets separation_openin_Un_gen)

lemma separated_between:
   "separated_between X S T 
        (U. closedin X U  openin X U  S  U  T  topspace X - U)"
  unfolding separated_between_def closedin_def disjnt_def
  by (smt (verit, del_insts) Diff_cancel Diff_disjoint Diff_partition Un_Diff Un_Diff_Int openin_subset)

lemma separated_between_mono:
   "separated_between X S T; S'  S; T'  T  separated_between X S' T'"
  by (meson order.trans separated_between)

lemma separated_between_refl:
   "separated_between X S S  S = {}"
  unfolding separated_between_def
  by (metis Un_empty_right disjnt_def disjnt_empty2 disjnt_subset2 disjnt_sym le_iff_inf openin_empty openin_topspace)

lemma separated_between_sym:
   "separated_between X S T  separated_between X T S"
  by (metis disjnt_sym separated_between_alt sup_commute)

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

lemma separated_between_empty: 
  "(separated_between X {} S  S  topspace X)  (separated_between X S {}  S  topspace X)"
  by (metis Diff_empty bot.extremum closedin_empty openin_empty separated_between separated_between_imp_subset separated_between_sym)


lemma separated_between_Un: 
  "separated_between X S (T  U)  separated_between X S T  separated_between X S U"
  by (auto simp: separated_between)

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

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

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

lemma separated_between_full:
  assumes "S  T = topspace X"
  shows "separated_between X S T  disjnt S T  closedin X S  openin X S  closedin X T  openin X T"
proof -
  have "separated_between X S T  separatedin X S T"
    by (simp add: separated_between_imp_separatedin)
  then show ?thesis
    unfolding separated_between_def
    by (metis assms separation_closedin_Un_gen separation_openin_Un_gen subset_refl subtopology_topspace)
qed

lemma separated_between_eq_separatedin:
   "S  T = topspace X  (separated_between X S T  separatedin X S T)"
  by (simp add: separated_between_full separatedin_full)

lemma separated_between_pointwise_left:
  assumes "compactin X S"
  shows "separated_between X S T 
         (S = {}  T  topspace X)  (x  S. separated_between X {x} T)"  (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    using separated_between_imp_subset separated_between_mono by fastforce
next
  assume R: ?rhs
  then have "T  topspace X"
    by (meson equals0I separated_between_imp_subset)
  show ?lhs
  proof -
    obtain U where U: "x  S. openin X (U x)"
      "x  S. V. openin X V  U x  V = topspace X  disjnt (U x) V  {x}  U x  T  V"
      using R unfolding separated_between_def by metis
    then have "S  (U ` S)"
      by blast
    then obtain K where "finite K" "K  S" and K: "S  (iK. U i)"
      using assms U unfolding compactin_def by (smt (verit) finite_subset_image imageE)
    show ?thesis
      unfolding separated_between
    proof (intro conjI exI)
      have "x. x  K  closedin X (U x)"
        by (smt (verit) K  S Diff_cancel U(2) Un_Diff Un_Diff_Int disjnt_def openin_closedin_eq subsetD)
      then show "closedin X ( (U ` K))"
        by (metis (mono_tags, lifting) finite K closedin_Union finite_imageI image_iff)
      show "openin X ( (U ` K))"
        using U(1) K  S by blast
      show "S   (U ` K)"
        by (simp add: K)
      have "x i. x  T; i  K; x  U i  False"
        by (meson U(2) K  S disjnt_iff subsetD)
      then show "T  topspace X -  (U ` K)"
        using T  topspace X by auto
    qed
  qed
qed

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

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


lemma separated_between_closure_of':
 "T  topspace X  separated_between X S (X closure_of T)  separated_between X S T"
  by (meson separated_between_closure_of separated_between_sym)

lemma separated_between_closure_of_eq:
 "separated_between X S T  S  topspace X  separated_between X (X closure_of S) T"
  by (metis separated_between_closure_of separated_between_imp_subset)

lemma separated_between_closure_of_eq':
 "separated_between X S T  T  topspace X  separated_between X S (X closure_of T)"
  by (metis separated_between_closure_of' separated_between_imp_subset)

lemma separated_between_frontier_of_eq':
  "separated_between X S T 
   T  topspace X  disjnt S T  separated_between X S (X frontier_of T)" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    by (metis interior_of_union_frontier_of separated_between_Un separated_between_closure_of_eq' 
        separated_between_imp_disjoint)
next
  assume R: ?rhs
  then obtain U where U: "closedin X U" "openin X U" "S  U" "X closure_of T - X interior_of T  topspace X - U"
    by (metis frontier_of_def separated_between)
  show ?lhs
  proof (rule separated_between_mono [of _ S "X closure_of T"])
    have "separated_between X S T"
      unfolding separated_between
    proof (intro conjI exI)
      show "S  U - T" "T  topspace X - (U - T)"
        using R U(3) by (force simp: disjnt_iff)+
      have "T  X closure_of T"
        by (simp add: R closure_of_subset)
      then have *: "U - T = U - X interior_of T"
        using U(4) interior_of_subset by fastforce
      then show "closedin X (U - T)"
        by (simp add: U(1) closedin_diff)
      have "U  X frontier_of T = {}"
        using U(4) frontier_of_def by fastforce
      then show "openin X (U - T)"
        by (metis * Diff_Un U(2) Un_Diff_Int Un_Int_eq(1) closedin_closure_of interior_of_union_frontier_of openin_diff sup_bot_right)
    qed
    then show "separated_between X S (X closure_of T)"
      by (simp add: R separated_between_closure_of')
  qed (auto simp: R closure_of_subset)
qed

lemma separated_between_frontier_of_eq:
  "separated_between X S T  S  topspace X  disjnt S T  separated_between X (X frontier_of S) T"
  by (metis disjnt_sym separated_between_frontier_of_eq' separated_between_sym)

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

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

lemma connected_space_separated_between:
  "connected_space X  (S T. separated_between X S T  S = {}  T = {})" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    by (metis Diff_cancel connected_space_clopen_in separated_between subset_empty)
next
  assume ?rhs then show ?lhs
    by (meson connected_space_eq_not_separated separated_between_eq_separatedin)
qed

lemma connected_space_imp_separated_between_trivial:
   "connected_space X
         (separated_between X S T  S = {}  T  topspace X  S  topspace X  T = {})"
  by (metis connected_space_separated_between separated_between_empty)


subsection‹Connected components›

lemma connected_component_of_subtopology_eq:
   "connected_component_of (subtopology X U) a = connected_component_of X a 
    connected_component_of_set X a  U"
  by (force simp: connected_component_of_set connectedin_subtopology connected_component_of_def fun_eq_iff subset_iff)

lemma connected_components_of_subtopology:
  assumes "C  connected_components_of X" "C  U"
  shows "C  connected_components_of (subtopology X U)"
proof -
  obtain a where a: "connected_component_of_set X a  U" and "a  topspace X"
             and Ceq: "C = connected_component_of_set X a"
    using assms by (force simp: connected_components_of_def)
  then have "a  U"
    by (simp add: connected_component_of_refl in_mono)
  then have "connected_component_of_set X a = connected_component_of_set (subtopology X U) a"
    by (metis a connected_component_of_subtopology_eq)
  then show ?thesis
    by (simp add: Ceq a  U a  topspace X connected_component_in_connected_components_of)
qed

lemma open_in_finite_connected_components:
  assumes "finite(connected_components_of X)" "C  connected_components_of X"
  shows "openin X C"
proof -
  have "closedin X (topspace X - C)"
    by (metis DiffD1 assms closedin_Union closedin_connected_components_of complement_connected_components_of_Union finite_Diff)
  then show ?thesis
    by (simp add: assms connected_components_of_subset openin_closedin)
qed
thm connected_component_of_eq_overlap

lemma connected_components_of_disjoint:
  assumes "C  connected_components_of X" "C'  connected_components_of X"
    shows "(disjnt C C'  (C  C'))"
  using assms nonempty_connected_components_of pairwiseD pairwise_disjoint_connected_components_of by fastforce

lemma connected_components_of_overlap:
   "C  connected_components_of X; C'  connected_components_of X  C  C'  {}  C = C'"
  by (meson connected_components_of_disjoint disjnt_def)

lemma pairwise_separated_connected_components_of:
   "pairwise (separatedin X) (connected_components_of X)"
  by (simp add: closedin_connected_components_of connected_components_of_disjoint pairwiseI separatedin_closed_sets)

lemma finite_connected_components_of_finite:
   "finite(topspace X)  finite(connected_components_of X)"
  by (simp add: Union_connected_components_of finite_UnionD)

lemma connected_component_of_unique:
   "x  C; connectedin X C; C'. x  C'  connectedin X C'  C'  C
         connected_component_of_set X x = C"
  by (meson connected_component_of_maximal connectedin_connected_component_of subsetD subset_antisym)

lemma closedin_connected_component_of_subtopology:
   "C  connected_components_of (subtopology X s); X closure_of C  s  closedin X C"
  by (metis closedin_Int_closure_of closedin_connected_components_of closure_of_eq inf.absorb_iff2)

lemma connected_component_of_discrete_topology:
   "connected_component_of_set (discrete_topology U) x = (if x  U then {x} else {})"
  by (simp add: locally_path_connected_space_discrete_topology flip: path_component_eq_connected_component_of)

lemma connected_components_of_discrete_topology:
   "connected_components_of (discrete_topology U) = (λx. {x}) ` U"
  by (simp add: connected_component_of_discrete_topology connected_components_of_def)

lemma connected_component_of_continuous_image:
   "continuous_map X Y f; connected_component_of X x y
         connected_component_of Y (f x) (f y)"
  by (meson connected_component_of_def connectedin_continuous_map_image image_eqI)

lemma homeomorphic_map_connected_component_of:
  assumes "homeomorphic_map X Y f" and x: "x  topspace X"
  shows "connected_component_of_set Y (f x) = f ` (connected_component_of_set X x)"
proof -
  obtain g where g: "continuous_map X Y f"
    "continuous_map Y X g " "x. x  topspace X  g (f x) = x" 
    "y. y  topspace Y  f (g y) = y"
    using assms(1) homeomorphic_map_maps homeomorphic_maps_def by fastforce
  show ?thesis
    using connected_component_in_topspace [of Y] x g
          connected_component_of_continuous_image [of X Y f]
          connected_component_of_continuous_image [of Y X g]
    by force
qed

lemma homeomorphic_map_connected_components_of:
  assumes "homeomorphic_map X Y f"
  shows "connected_components_of Y = (image f) ` (connected_components_of X)"
proof -
  have "topspace Y = f ` topspace X"
    by (metis assms homeomorphic_imp_surjective_map)
  with homeomorphic_map_connected_component_of [OF assms] show ?thesis
    by (auto simp: connected_components_of_def image_iff)
qed

lemma connected_component_of_pair:
   "connected_component_of_set (prod_topology X Y) (x,y) =
        connected_component_of_set X x × connected_component_of_set Y y"
proof (cases "x  topspace X  y  topspace Y")
  case True
  show ?thesis
  proof (rule connected_component_of_unique)
    show "(x, y)  connected_component_of_set X x × connected_component_of_set Y y"
      using True by (simp add: connected_component_of_refl)
    show "connectedin (prod_topology X Y) (connected_component_of_set X x × connected_component_of_set Y y)"
      by (metis connectedin_Times connectedin_connected_component_of)
    show "C  connected_component_of_set X x × connected_component_of_set Y y"
      if "(x, y)  C  connectedin (prod_topology X Y) C" for C 
      using that unfolding connected_component_of_def
      apply clarsimp
      by (metis (no_types) connectedin_continuous_map_image continuous_map_fst continuous_map_snd fst_conv imageI snd_conv)
  qed
next
  case False then show ?thesis
    by (metis Sigma_empty1 Sigma_empty2 connected_component_of_eq_empty mem_Sigma_iff topspace_prod_topology)
qed

lemma connected_components_of_prod_topology:
  "connected_components_of (prod_topology X Y) =
    {C × D |C D. C  connected_components_of X  D  connected_components_of Y}" (is "?lhs=?rhs")
proof
  show "?lhs  ?rhs"
    apply (clarsimp simp: connected_components_of_def)
    by (metis (no_types) connected_component_of_pair imageI)
next
  show "?rhs  ?lhs"
    using connected_component_of_pair
    by (fastforce simp: connected_components_of_def)
qed


lemma connected_component_of_product_topology:
   "connected_component_of_set (product_topology X I) x =
    (if x  extensional I then PiE I (λi. connected_component_of_set (X i) (x i)) else {})"
    (is "?lhs = If _ ?R _")    
proof (cases "x  topspace(product_topology X I)")
  case True
  have "?lhs = (ΠE iI. connected_component_of_set (X i) (x i))"
    if xX: "i. iI  x i  topspace (X i)" and ext: "x  extensional I"
  proof (rule connected_component_of_unique)
    show "x  ?R"
      by (simp add: PiE_iff connected_component_of_refl local.ext xX)
    show "connectedin (product_topology X I) ?R"
      by (simp add: connectedin_PiE connectedin_connected_component_of)
    show "C  ?R"
      if "x  C  connectedin (product_topology X I) C" for C 
    proof -
      have "C  extensional I"
        using PiE_def connectedin_subset_topspace that by fastforce
      have "y. y  C  y  (Π iI. connected_component_of_set (X i) (x i))"
        apply (simp add: connected_component_of_def Pi_def)
        by (metis connectedin_continuous_map_image continuous_map_product_projection imageI that)
      then show ?thesis
        using PiE_def C  extensional I by fastforce
    qed
  qed
  with True show ?thesis
    by (simp add: PiE_iff)
next
  case False
  then show ?thesis
    by (smt (verit, best) PiE_eq_empty_iff PiE_iff connected_component_of_eq_empty topspace_product_topology)
qed


lemma connected_components_of_product_topology:
   "connected_components_of (product_topology X I) =
    {PiE I B |B. i  I. B i  connected_components_of(X i)}"  (is "?lhs=?rhs")
proof
  show "?lhs  ?rhs"
    by (auto simp: connected_components_of_def connected_component_of_product_topology PiE_iff)
  show "?rhs  ?lhs"
  proof
    fix F
    assume "F  ?rhs"
    then obtain B where Feq: "F = PiE I B" and
      "iI. xtopspace (X i). B i = connected_component_of_set (X i) x"
      by (force simp: connected_components_of_def connected_component_of_product_topology image_iff)
    then obtain f where
      f: "i. i  I  f i  topspace (X i)  B i = connected_component_of_set (X i) (f i)"
      by metis
    then have "(λiI. f i)  ((ΠE iI. topspace (X i))  extensional I)"
      by simp
    with f show "F  ?lhs"
      unfolding Feq connected_components_of_def connected_component_of_product_topology image_iff
      by (smt (verit, del_insts) PiE_cong restrict_PiE_iff restrict_apply' restrict_extensional topspace_product_topology)
  qed
qed


subsection ‹Monotone maps (in the general topological sense)›


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

lemma monotone_map:
  "monotone_map X Y f 
   f ` (topspace X)  topspace Y  (y. connectedin X {x  topspace X. f x = y})"
  apply (simp add: monotone_map_def)
  by (metis (mono_tags, lifting) connectedin_empty [of X] Collect_empty_eq image_subset_iff) 


lemma monotone_map_in_subtopology:
   "monotone_map X (subtopology Y S) f  monotone_map X Y f  f ` (topspace X)  S"
  by (smt (verit, del_insts) le_inf_iff monotone_map topspace_subtopology)

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

lemma monotone_map_restriction:
  "monotone_map X Y f  {x  topspace X. f x  v} = u
         monotone_map (subtopology X u) (subtopology Y v) f"
  by (smt (verit, best) IntI Int_Collect image_subset_iff mem_Collect_eq monotone_map monotone_map_from_subtopology topspace_subtopology)

lemma injective_imp_monotone_map:
  assumes "f ` topspace X  topspace Y"  "inj_on f (topspace X)"
  shows "monotone_map X Y f"
  unfolding monotone_map_def
proof (intro conjI assms strip)
  fix y
  assume "y  topspace Y"
  then have "{x  topspace X. f x = y} = {}  (a  topspace X. {x  topspace X. f x = y} = {a})"
    using assms(2) unfolding inj_on_def by blast
  then show "connectedin X {x  topspace X. f x = y}"
    by (metis (no_types, lifting) connectedin_empty connectedin_sing)
qed

lemma embedding_imp_monotone_map:
   "embedding_map X Y f  monotone_map X Y f"
  by (metis (no_types) embedding_map_def homeomorphic_eq_everything_map inf.absorb_iff2 injective_imp_monotone_map topspace_subtopology)

lemma section_imp_monotone_map:
   "section_map X Y f  monotone_map X Y f"
  by (simp add: embedding_imp_monotone_map section_imp_embedding_map)

lemma homeomorphic_imp_monotone_map:
   "homeomorphic_map X Y f  monotone_map X Y f"
  by (meson section_and_retraction_eq_homeomorphic_map section_imp_monotone_map)

proposition connected_space_monotone_quotient_map_preimage:
  assumes f: "monotone_map X Y f" "quotient_map X Y f" and "connected_space Y"
  shows "connected_space X"
proof (rule ccontr)
  assume "¬ connected_space X"
  then obtain U V where "openin X U" "openin X V" "U  V = {}"
    "U  {}" "V  {}" and topUV: "topspace X  U  V"
    by (auto simp: connected_space_def)
  then have UVsub: "U  topspace X" "V  topspace X"
    by (auto simp: openin_subset)
  have "¬ connected_space Y"
    unfolding connected_space_def not_not
  proof (intro exI conjI)
    show "topspace Y  f`U  f`V"
      by (metis f(2) image_Un quotient_imp_surjective_map subset_Un_eq topUV)
    show "f`U  {}"
      by (simp add: U  {})
    show "(f`V)  {}"
      by (simp add: V  {})
    have *: "y  f ` V" if "y  f ` U" for y
    proof -
      have §: "connectedin X {x  topspace X. f x = y}"
        using f(1) monotone_map by fastforce
      show ?thesis
        using connectedinD [OF § openin X U openin X V] UVsub topUV U  V = {} that
        by (force simp: disjoint_iff)
    qed
    then show "f`U  f`V = {}"
      by blast
    show "openin Y (f`U)"
      using f openin X U topUV * unfolding quotient_map_saturated_open by force
    show "openin Y (f`V)"
      using f openin X V topUV * unfolding quotient_map_saturated_open by force
  qed
  then show False
    by (simp add: assms)
qed

lemma connectedin_monotone_quotient_map_preimage:
  assumes "monotone_map X Y f" "quotient_map X Y f" "connectedin Y C" "openin Y C  closedin Y C"
  shows "connectedin X {x  topspace X. f x  C}"
proof -
  have "connected_space (subtopology X {x  topspace X. f x  C})"
  proof -
    have "connected_space (subtopology Y C)"
      using connectedin Y C connectedin_def by blast
    moreover have "quotient_map (subtopology X {a  topspace X. f a  C}) (subtopology Y C) f"
      by (simp add: assms quotient_map_restriction)
    ultimately show ?thesis
      using monotone_map X Y f connected_space_monotone_quotient_map_preimage monotone_map_restriction by blast
  qed
  then show ?thesis
    by (simp add: connectedin_def)
qed

lemma monotone_open_map:
  assumes "continuous_map X Y f" "open_map X Y f" and fim: "f ` (topspace X) = topspace Y"
  shows "monotone_map X Y f  (C. connectedin Y C  connectedin X {x  topspace X. f x  C})"
         (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding connectedin_def
  proof (intro strip conjI)
    fix C
    assume C: "C  topspace Y  connected_space (subtopology Y C)"
    show "connected_space (subtopology X {x  topspace X. f x  C})"
    proof (rule connected_space_monotone_quotient_map_preimage)
      show "monotone_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
        by (simp add: L monotone_map_restriction)
      show "quotient_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
      proof (rule continuous_open_imp_quotient_map)
        show "continuous_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
          using assms continuous_map_from_subtopology continuous_map_in_subtopology by fastforce
      qed (use open_map_restriction assms in fastforce)+
    qed (simp add: C)
  qed auto
next
  assume ?rhs 
  then have "y. connectedin Y {y}  connectedin X {x  topspace X. f x = y}"
    by (smt (verit) Collect_cong singletonD singletonI)
  then show ?lhs
    by (simp add: fim monotone_map_def)
qed

lemma monotone_closed_map:
  assumes "continuous_map X Y f" "closed_map X Y f" and fim: "f ` (topspace X) = topspace Y"
  shows "monotone_map X Y f  (C. connectedin Y C  connectedin X {x  topspace X. f x  C})" 
         (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  show ?rhs
    unfolding connectedin_def
  proof (intro strip conjI)
    fix C
    assume C: "C  topspace Y  connected_space (subtopology Y C)"
    show "connected_space (subtopology X {x  topspace X. f x  C})"
    proof (rule connected_space_monotone_quotient_map_preimage)
      show "monotone_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
        by (simp add: L monotone_map_restriction)
      show "quotient_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
      proof (rule continuous_closed_imp_quotient_map)
        show "continuous_map (subtopology X {x  topspace X. f x  C}) (subtopology Y C) f"
          using assms continuous_map_from_subtopology continuous_map_in_subtopology by fastforce
      qed (use closed_map_restriction assms in fastforce)+
    qed (simp add: C)
  qed auto
next
  assume ?rhs 
  then have "y. connectedin Y {y}  connectedin X {x  topspace X. f x = y}"
    by (smt (verit) Collect_cong singletonD singletonI)
  then show ?lhs
    by (simp add: fim monotone_map_def)
qed

subsection‹Other countability properties›

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

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

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

lemma second_countable:
   "second_countable X 
        (. countable   openin X = arbitrary union_of (λx. x  ))"
  by (smt (verit) openin_topology_base_unique second_countable_def)

lemma second_countable_subtopology:
  assumes "second_countable X"
  shows "second_countable (subtopology X S)"
proof -
  obtain  where : "countable " "V. V    openin X V"
    "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  show ?thesis
    unfolding second_countable_def
  proof (intro exI conjI)
    show "V((∩)S) ` . openin (subtopology X S) V"
      using openin_subtopology_Int2  by blast
    show "U x. openin (subtopology X S) U  x  U  (V((∩)S) ` . x  V  V  U)"
      using  unfolding openin_subtopology
      by (smt (verit, del_insts) IntI image_iff inf_commute inf_le1 subset_iff)
  qed (use  in auto)
qed


lemma second_countable_discrete_topology:
   "second_countable(discrete_topology U)  countable U" (is "?lhs=?rhs")
proof
  assume L: ?lhs 
  then
  obtain  where : "countable " "V. V    V  U"
    "W x. W  U  x  W  (V  . x  V  V  W)"
    by (auto simp: second_countable_def)
  then have "{x}  " if "x  U" for x
    by (metis empty_subsetI insertCI insert_subset subset_antisym that)
  then show ?rhs
    by (smt (verit) countable_subset image_subsetI countable  countable_image_inj_on [OF _ inj_singleton])
next
  assume ?rhs 
  then show ?lhs
    unfolding second_countable_def
    by (rule_tac x="(λx. {x}) ` U" in exI) auto
qed

lemma second_countable_open_map_image:
  assumes "continuous_map X Y f" "open_map X Y f" 
   and fim: "f ` (topspace X) = topspace Y" and "second_countable X"
 shows "second_countable Y"
proof -
  have openXYf: "U. openin X U  openin Y (f ` U)"
    using assms by (auto simp: open_map_def)
  obtain  where : "countable " "V. V    openin X V"
    and *: "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  show ?thesis
    unfolding second_countable_def
  proof (intro exI conjI strip)
    fix V y
    assume V: "openin Y V  y  V"
    then obtain x where "x  topspace X" and x: "f x = y"
      by (metis fim image_iff openin_subset subsetD)

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

lemma homeomorphic_space_second_countability:
   "X homeomorphic_space Y  (second_countable X  second_countable Y)"
  by (meson homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym second_countable_open_map_image)

lemma second_countable_retraction_map_image:
   "retraction_map X Y r; second_countable X  second_countable Y"
  using hereditary_imp_retractive_property homeomorphic_space_second_countability second_countable_subtopology by blast

lemma second_countable_imp_first_countable:
   "second_countable X  first_countable X"
  by (metis first_countable_def second_countable_def)

lemma first_countable_subtopology:
  assumes "first_countable X"
  shows "first_countable (subtopology X S)"
  unfolding first_countable_def
proof
  fix x
  assume "x  topspace (subtopology X S)"
  then obtain  where "countable " and : "V. V    openin X V"
    "U. openin X U  x  U  (V  . x  V  V  U)"
    using assms first_countable_def by force
  show ". countable   (V. openin (subtopology X S) V)  (U. openin (subtopology X S) U  x  U  (V. x  V  V  U))"
  proof (intro exI conjI strip)
    show "countable (((∩)S) ` )"
      using countable  by blast
    show "openin (subtopology X S) V" if "V  ((∩)S) ` " for V
      using  openin_subtopology_Int2 that by fastforce
    show "V((∩)S) ` . x  V  V  U"
      if "openin (subtopology X S) U  x  U" for U 
      using that (2) by (clarsimp simp: openin_subtopology) (meson le_infI2)
  qed
qed

lemma first_countable_discrete_topology:
   "first_countable (discrete_topology U)"
  unfolding first_countable_def topspace_discrete_topology openin_discrete_topology
proof
  fix x assume "x  U"
  show ". countable   (V. V  U)  (Ua. Ua  U  x  Ua  (V. x  V  V  Ua))"
    using x  U by (rule_tac x="{{x}}" in exI) auto
qed

lemma first_countable_open_map_image:
  assumes "continuous_map X Y f" "open_map X Y f" 
   and fim: "f ` (topspace X) = topspace Y" and "first_countable X"
 shows "first_countable Y"
  unfolding first_countable_def
proof
  fix y
  assume "y  topspace Y"
  have openXYf: "U. openin X U  openin Y (f ` U)"
    using assms by (auto simp: open_map_def)
  then obtain x where x: "x  topspace X" "f x = y"
    by (metis y  topspace Y fim imageE)
  obtain  where : "countable " "V. V    openin X V"
    and *: "U. openin X U  x  U  (V  . x  V  V  U)"
    using assms x first_countable_def by force
  show ". countable  
              (V. openin Y V)  (U. openin Y U  y  U  (V. y  V  V  U))"
  proof (intro exI conjI strip)
    fix V assume "openin Y V  y  V"
    then have "W. x  W  W  {x  topspace X. f x  V}"
      using * [of "{x  topspace X. f x  V}"] assms openin_continuous_map_preimage x 
      by fastforce
    then show "V'  (image f) ` . y  V'  V'  V"
      using image_mono x by auto 
  qed (use  openXYf in force)+
qed

lemma homeomorphic_space_first_countability:
  "X homeomorphic_space Y  first_countable X  first_countable Y"
  by (meson first_countable_open_map_image homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym)

lemma first_countable_retraction_map_image:
   "retraction_map X Y r; first_countable X  first_countable Y"
  using first_countable_subtopology hereditary_imp_retractive_property homeomorphic_space_first_countability by blast

lemma separable_space_open_subset:
  assumes "separable_space X" "openin X S"
  shows "separable_space (subtopology X S)"
proof -
  obtain C where C: "countable C" "C  topspace X" "X closure_of C = topspace X"
    by (meson assms separable_space_def)
  then have "x T. x  topspace X; x  T; openin (subtopology X S) T
            y. y  S  y  C  y  T"
    by (smt (verit) openin X S in_closure_of openin_open_subtopology subsetD)
  with C openin X S show ?thesis
    unfolding separable_space_def
    by (rule_tac x="S  C" in exI) (force simp: in_closure_of)
qed

lemma separable_space_continuous_map_image:
  assumes "separable_space X" "continuous_map X Y f" 
    and fim: "f ` (topspace X) = topspace Y"
  shows "separable_space Y"
proof -
  have cont: "S. f ` (X closure_of S)  Y closure_of f ` S"
    by (simp add: assms continuous_map_image_closure_subset)
  obtain C where C: "countable C" "C  topspace X" "X closure_of C = topspace X"
    by (meson assms separable_space_def)
  then show ?thesis
    unfolding separable_space_def
    by (metis cont fim closure_of_subset_topspace countable_image image_mono subset_antisym)
qed

lemma separable_space_quotient_map_image:
  "quotient_map X Y q; separable_space X  separable_space Y"
  by (meson quotient_imp_continuous_map quotient_imp_surjective_map separable_space_continuous_map_image)

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

lemma homeomorphic_separable_space:
  "X homeomorphic_space Y  (separable_space X  separable_space Y)"
  by (meson homeomorphic_eq_everything_map homeomorphic_maps_map homeomorphic_space_def separable_space_continuous_map_image)

lemma separable_space_discrete_topology:
   "separable_space(discrete_topology U)  countable U"
  by (metis countable_Int2 discrete_topology_closure_of dual_order.refl inf.orderE separable_space_def topspace_discrete_topology)

lemma second_countable_imp_separable_space:
  assumes "second_countable X"
  shows "separable_space X"
proof -
  obtain  where : "countable " "V. V    openin X V"
    and *: "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  obtain c where c: "V. V  ; V  {}  c V  V"
    by (metis all_not_in_conv)
  then have **: "x. x  topspace X  x  X closure_of c ` ( - {{}})"
    using * by (force simp: closure_of_def)
  show ?thesis
    unfolding separable_space_def
  proof (intro exI conjI)
    show "countable (c ` (-{{}}))"
      using (1) by blast
    show "(c ` (-{{}}))  topspace X"
      using (2) c openin_subset by fastforce
    show "X closure_of (c ` (-{{}})) = topspace X"
      by (meson ** closure_of_subset_topspace subsetI subset_antisym)
  qed
qed

lemma second_countable_imp_Lindelof_space:
  assumes "second_countable X"
  shows "Lindelof_space X"
unfolding Lindelof_space_def
proof clarify
  fix 𝒰
  assume "U  𝒰. openin X U" and UU: "𝒰 = topspace X"
  obtain  where : "countable " "V. V    openin X V"
    and *: "U x. openin X U  x  U  (V  . x  V  V  U)"
    using assms by (auto simp: second_countable_def)
  define ℬ' where "ℬ' = {B  . U. U  𝒰  B  U}"
  have ℬ': "countable ℬ'" "ℬ' = 𝒰"
    using  using "*" U𝒰. openin X U by (fastforce simp: ℬ'_def)+
  have "b. U. b  ℬ'  U  𝒰  b  U" 
    by (simp add: ℬ'_def)
  then obtain G where G: "b. b  ℬ'  G b  𝒰  b  G b" 
    by metis
  with ℬ' UU show "𝒱. countable 𝒱  𝒱  𝒰  𝒱 = topspace X"
    by (rule_tac x="G ` ℬ'" in exI) fastforce
qed

subsection ‹Neigbourhood bases EXTRAS›

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

lemma openin_topology_neighbourhood_base_unique:
   "openin X = arbitrary union_of P 
        (u. P u  openin X u)  neighbourhood_base_of P X"
  by (smt (verit, best) open_neighbourhood_base_of openin_topology_base_unique)

lemma neighbourhood_base_at_topology_base:
   "        openin X = arbitrary union_of b
         (neighbourhood_base_at x P X 
             (w. b w  x  w  (u v. openin X u  P v  x  u  u  v  v  w)))"
  apply (simp add: neighbourhood_base_at_def)
  by (smt (verit, del_insts) openin_topology_base_unique subset_trans)

lemma neighbourhood_base_of_unlocalized:
  assumes "S t. P S  openin X t  (t  {})  t  S  P t"
  shows "neighbourhood_base_of P X 
         (x  topspace X. u v. openin X u  P v  x  u  u  v  v  topspace X)"
  apply (simp add: neighbourhood_base_of_def)
  by (smt (verit, ccfv_SIG) assms empty_iff neighbourhood_base_at_unlocalized)

lemma neighbourhood_base_at_discrete_topology:
   "neighbourhood_base_at x P (discrete_topology u)  x  u  P {x}"
  apply (simp add: neighbourhood_base_at_def)
  by (smt (verit) empty_iff empty_subsetI insert_subset singletonI subsetD subset_singletonD)

lemma neighbourhood_base_of_discrete_topology:
   "neighbourhood_base_of P (discrete_topology u)  (x  u. P {x})"
  apply (simp add: neighbourhood_base_of_def)
  using neighbourhood_base_at_discrete_topology[of _ P u]
  by (metis empty_subsetI insert_subset neighbourhood_base_at_def openin_discrete_topology singletonI)

lemma second_countable_neighbourhood_base_alt:
  "second_countable X  
  (. countable   (V  . openin X V)  neighbourhood_base_of (λA. A) X)"
  by (metis (full_types) openin_topology_neighbourhood_base_unique second_countable)

lemma first_countable_neighbourhood_base_alt:
   "first_countable X 
    (x  topspace X. . countable   (V  . openin X V)  neighbourhood_base_at x (λV. V  ) X)"
  unfolding first_countable_def
  apply (intro ball_cong refl ex_cong conj_cong)
  by (metis (mono_tags, lifting) open_neighbourhood_base_at)

lemma second_countable_neighbourhood_base:
   "second_countable X 
        (. countable   neighbourhood_base_of (λV. V  ) X)" (is "?lhs=?rhs")
proof
  assume ?lhs 
  then show ?rhs
    using second_countable_neighbourhood_base_alt by blast
next
  assume ?rhs 
  then obtain  where "countable "
    and : "W x. openin X W  x  W  (U. openin X U  (V. V    x  U  U  V  V  W))"
    by (metis neighbourhood_base_of)
  then show ?lhs
    unfolding second_countable_neighbourhood_base_alt neighbourhood_base_of
    apply (rule_tac x="(λu. X interior_of u) ` " in exI)
    by (smt (verit, best) interior_of_eq interior_of_mono countable_image image_iff openin_interior_of)
qed

lemma first_countable_neighbourhood_base:
   "first_countable X 
    (x  topspace X. . countable   neighbourhood_base_at x (λV. V  ) X)" (is "?lhs=?rhs")
proof
  assume ?lhs 
  then show ?rhs
    by (metis first_countable_neighbourhood_base_alt)
next
  assume R: ?rhs 
  show ?lhs
    unfolding first_countable_neighbourhood_base_alt
  proof
    fix x
    assume "x  topspace X"
    with R obtain  where "countable " and : "neighbourhood_base_at x (λV. V  ) X"
      by blast
    then
    show ". countable   Ball  (openin X)  neighbourhood_base_at x (λV. V  ) X"
      unfolding neighbourhood_base_at_def
      apply (rule_tac x="(λu. X interior_of u) ` " in exI)
      by (smt (verit, best) countable_image image_iff interior_of_eq interior_of_mono openin_interior_of)
  qed
qed


subsection‹$T_0$ spaces and the Kolmogorov quotient›

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

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

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

lemma t1_eq_symmetric_t0_space_alt:
   "t1_space X 
      t0_space X 
      (x  topspace X. y  topspace X. x  X closure_of {y}  y  X closure_of {x})"
  apply (simp add: t0_space_def t1_space_def closure_of_def)
  by (smt (verit, best) openin_topspace)

lemma t1_eq_symmetric_t0_space:
  "t1_space X  t0_space X  (x y. x  X closure_of {y}  y  X closure_of {x})"
  by (auto simp: t1_eq_symmetric_t0_space_alt in_closure_of)

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

lemma t0_space:
   "t0_space X 
    (x  topspace X. y  topspace X. x  y  (C. closedin X C  (x  C  y  C)))"
  unfolding t0_space_def by (metis Diff_iff closedin_def openin_closedin_eq)

lemma homeomorphic_t0_space:
  assumes "X homeomorphic_space Y"
  shows "t0_space X  t0_space Y"
proof -
  obtain f where f: "homeomorphic_map X Y f" and F: "inj_on f (topspace X)" and "topspace Y = f ` topspace X"
    by (metis assms homeomorphic_imp_injective_map homeomorphic_imp_surjective_map homeomorphic_space)
  with inj_on_image_mem_iff [OF F] 
  show ?thesis
    apply (simp add: t0_space_def homeomorphic_eq_everything_map continuous_map_def open_map_def inj_on_def)
    by (smt (verit)  mem_Collect_eq openin_subset)
qed

lemma t0_space_closure_of_sing:
   "t0_space X 
    (x  topspace X. y  topspace X. X closure_of {x} = X closure_of {y}  x = y)"
  by (simp add: t0_space_def closure_of_def set_eq_iff) (smt (verit))

lemma t0_space_discrete_topology: "t0_space (discrete_topology S)"
  by (simp add: Hausdorff_imp_t0_space)

lemma t0_space_subtopology: "t0_space X  t0_space (subtopology X U)"
  by (simp add: t0_space_def openin_subtopology) (metis Int_iff)

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

lemma t0_space_prod_topologyI: "t0_space X; t0_space Y  t0_space (prod_topology X Y)"
  by (simp add: t0_space_closure_of_sing closure_of_Times closure_of_eq_empty_gen times_eq_iff flip: sing_Times_sing insert_Times_insert)


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

proposition t0_space_product_topology:
   "t0_space (product_topology X I)  product_topology X I = trivial_topology  (i  I. t0_space (X i))" 
    (is "?lhs=?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (meson retraction_map_product_projection t0_space_retraction_map_image)
next
  assume R: ?rhs 
  show ?lhs
  proof (cases "product_topology X I = trivial_topology")
    case True
    then show ?thesis
      by (simp add: t0_space_def)
  next
    case False
    show ?thesis
      unfolding t0_space
    proof (intro strip)
      fix x y
      assume x: "x  topspace (product_topology X I)"
        and y: "y  topspace (product_topology X I)"
        and "x  y"
      then obtain i where "i  I" "x i  y i"
        by (metis PiE_ext topspace_product_topology)
      then have "t0_space (X i)"
        using False R by blast
      then obtain U where "closedin (X i) U" "(x i  U  y i  U)"
        by (metis t0_space PiE_mem i  I x i  y i topspace_product_topology x y)
      with i  I x y show "U. closedin (product_topology X I) U  (x  U) = (y  U)"
        by (rule_tac x="PiE I (λj. if j = i then U else topspace(X j))" in exI)
          (simp add: closedin_product_topology PiE_iff)
    qed
  qed
qed


subsection ‹Kolmogorov quotients›

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

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

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

lemma Kolmogorov_quotient_in_closed:
  "closedin X C  (Kolmogorov_quotient X x  C  x  C)"
  unfolding closedin_def
  by (meson DiffD2 DiffI Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace in_mono)
 
lemma continuous_map_Kolmogorov_quotient:
   "continuous_map X X (Kolmogorov_quotient X)"
  using Kolmogorov_quotient_in_open openin_subopen openin_subset 
    by (fastforce simp: continuous_map_def Kolmogorov_quotient_in_topspace)

lemma open_map_Kolmogorov_quotient_explicit:
   "openin X U  Kolmogorov_quotient X ` U = Kolmogorov_quotient X ` topspace X  U"
  using Kolmogorov_quotient_in_open openin_subset by fastforce


lemma open_map_Kolmogorov_quotient_gen:
   "open_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
proof (clarsimp simp: open_map_def openin_subtopology_alt image_iff)
  fix U
  assume "openin X U"
  then have "Kolmogorov_quotient X ` (S  U) = Kolmogorov_quotient X ` S  U"
    using Kolmogorov_quotient_in_open [of X U] by auto
  then show "V. openin X V  Kolmogorov_quotient X ` (S  U) = Kolmogorov_quotient X ` S  V"
    using openin X U by blast
qed

lemma open_map_Kolmogorov_quotient:
   "open_map X (subtopology X (Kolmogorov_quotient X ` topspace X))
     (Kolmogorov_quotient X)"
  by (metis open_map_Kolmogorov_quotient_gen subtopology_topspace)

lemma closed_map_Kolmogorov_quotient_explicit:
   "closedin X U  Kolmogorov_quotient X ` U = Kolmogorov_quotient X ` topspace X  U"
  using closedin_subset by (fastforce simp: Kolmogorov_quotient_in_closed)

lemma closed_map_Kolmogorov_quotient_gen:
   "closed_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S))
     (Kolmogorov_quotient X)"
  using Kolmogorov_quotient_in_closed by (force simp: closed_map_def closedin_subtopology_alt image_iff)

lemma closed_map_Kolmogorov_quotient:
   "closed_map X (subtopology X (Kolmogorov_quotient X ` topspace X))
     (Kolmogorov_quotient X)"
  by (metis closed_map_Kolmogorov_quotient_gen subtopology_topspace)

lemma quotient_map_Kolmogorov_quotient_gen:
  "quotient_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
proof (intro continuous_open_imp_quotient_map)
  show "continuous_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
    by (simp add: continuous_map_Kolmogorov_quotient continuous_map_from_subtopology continuous_map_in_subtopology image_mono)
  show "open_map (subtopology X S) (subtopology X (Kolmogorov_quotient X ` S)) (Kolmogorov_quotient X)"
    using open_map_Kolmogorov_quotient_gen by blast
  show "Kolmogorov_quotient X ` topspace (subtopology X S) = topspace (subtopology X (Kolmogorov_quotient X ` S))"
    by (force simp: Kolmogorov_quotient_in_open)
qed

lemma quotient_map_Kolmogorov_quotient:
   "quotient_map X (subtopology X (Kolmogorov_quotient X ` topspace X)) (Kolmogorov_quotient X)"
  by (metis quotient_map_Kolmogorov_quotient_gen subtopology_topspace)

lemma Kolmogorov_quotient_eq:
   "Kolmogorov_quotient X x = Kolmogorov_quotient X y 
    (U. openin X U  (x  U  y  U))" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    by (metis Kolmogorov_quotient_in_open)
next
  assume ?rhs then show ?lhs
    by (simp add: Kolmogorov_quotient_def)
qed

lemma Kolmogorov_quotient_eq_alt:
   "Kolmogorov_quotient X x = Kolmogorov_quotient X y 
    (U. closedin X U  (x  U  y  U))" (is "?lhs=?rhs")
proof
  assume ?lhs then show ?rhs
    by (metis Kolmogorov_quotient_in_closed)
next
  assume ?rhs then show ?lhs
    by (smt (verit) Diff_iff Kolmogorov_quotient_eq closedin_topspace in_mono openin_closedin_eq)
qed

lemma Kolmogorov_quotient_continuous_map:
  assumes "continuous_map X Y f" "t0_space Y" and x: "x  topspace X"
  shows "f (Kolmogorov_quotient X x) = f x"
  using assms unfolding continuous_map_def t0_space_def
  by (smt (verit, ccfv_threshold) Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace PiE mem_Collect_eq)

lemma t0_space_Kolmogorov_quotient:
  "t0_space (subtopology X (Kolmogorov_quotient X ` topspace X))"
  apply (clarsimp simp: t0_space_def )
  by (smt (verit, best) Kolmogorov_quotient_eq imageE image_eqI open_map_Kolmogorov_quotient open_map_def)

lemma Kolmogorov_quotient_id:
   "t0_space X  x  topspace X  Kolmogorov_quotient X x = x"
  by (metis Kolmogorov_quotient_in_open Kolmogorov_quotient_in_topspace t0_space_def)

lemma Kolmogorov_quotient_idemp:
   "Kolmogorov_quotient X (Kolmogorov_quotient X x) = Kolmogorov_quotient X x"
  by (simp add: Kolmogorov_quotient_eq Kolmogorov_quotient_in_open)

lemma retraction_maps_Kolmogorov_quotient:
   "retraction_maps X
     (subtopology X (Kolmogorov_quotient X ` topspace X))
     (Kolmogorov_quotient X) id"
  unfolding retraction_maps_def continuous_map_in_subtopology
  using Kolmogorov_quotient_idemp continuous_map_Kolmogorov_quotient by force

lemma retraction_map_Kolmogorov_quotient:
   "retraction_map X
     (subtopology X (Kolmogorov_quotient X ` topspace X))
     (Kolmogorov_quotient X)"
  using retraction_map_def retraction_maps_Kolmogorov_quotient by blast

lemma retract_of_space_Kolmogorov_quotient_image:
   "Kolmogorov_quotient X ` topspace X retract_of_space X"
proof -
  have "continuous_map X X (Kolmogorov_quotient X)"
    by (simp add: continuous_map_Kolmogorov_quotient)
  then have "Kolmogorov_quotient X ` topspace X  topspace X"
    by (simp add: continuous_map_image_subset_topspace)
  then show ?thesis
    by (meson retract_of_space_retraction_maps retraction_maps_Kolmogorov_quotient)
qed

lemma Kolmogorov_quotient_lift_exists:
  assumes "S  topspace X" "t0_space Y" and f: "continuous_map (subtopology X S) Y f"
  obtains g where "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
              "x. x  S  g(Kolmogorov_quotient X x) = f x"
proof -
  have "x y. x  S; y  S; Kolmogorov_quotient X x = Kolmogorov_quotient X y  f x = f y"
    using assms
    apply (simp add: Kolmogorov_quotient_eq t0_space_def continuous_map_def Int_absorb1 openin_subtopology)
    by (smt (verit, del_insts) Int_iff mem_Collect_eq Pi_iff)
  then obtain g where g: "continuous_map (subtopology X (Kolmogorov_quotient X ` S)) Y g"
    "g ` (topspace X  Kolmogorov_quotient X ` S) = f ` S"
    "x. x  S  g (Kolmogorov_quotient X x) = f x"
    using quotient_map_lift_exists [OF quotient_map_Kolmogorov_quotient_gen [of X S] f]
    by (metis assms(1) topspace_subtopology topspace_subtopology_subset) 
  show ?thesis
    proof qed (use g in auto)
qed

subsection‹Closed diagonals and graphs›

lemma Hausdorff_space_closedin_diagonal:
  "Hausdorff_space X  closedin (prod_topology X X) ((λx. (x,x)) ` topspace X)"
proof -
  have §: "((λx. (x, x)) ` topspace X)  topspace X × topspace X"
    by auto
  show ?thesis
    apply (simp add: closedin_def openin_prod_topology_alt Hausdorff_space_def disjnt_iff §)
    apply (intro all_cong1 imp_cong ex_cong1 conj_cong refl)
    by (force dest!: openin_subset)+
qed

lemma closed_map_diag_eq:
   "closed_map X (prod_topology X X) (λx. (x,x))  Hausdorff_space X"
proof -
  have "section_map X (prod_topology X X) (λx. (x, x))"
    unfolding section_map_def retraction_maps_def
    by (smt (verit) continuous_map_fst continuous_map_of_fst continuous_map_on_empty continuous_map_pairwise fst_conv fst_diag_fst snd_diag_fst)
  then have "embedding_map X (prod_topology X X) (λx. (x, x))"
    by (rule section_imp_embedding_map)
  then show ?thesis
    using Hausdorff_space_closedin_diagonal embedding_imp_closed_map_eq by blast
qed

lemma proper_map_diag_eq [simp]:
   "proper_map X (prod_topology X X) (λx. (x,x))  Hausdorff_space X"
  by (simp add: closed_map_diag_eq inj_on_convol_ident injective_imp_proper_eq_closed_map)
  
lemma closedin_continuous_maps_eq:
  assumes "Hausdorff_space Y" and f: "continuous_map X Y f" and g: "continuous_map X Y g"
  shows "closedin X {x  topspace X. f x = g x}"
proof -
  have §:"{x  topspace X. f x = g x} = {x  topspace X. (f x,g x)  ((λy.(y,y)) ` topspace Y)}"
    using f continuous_map_image_subset_topspace by fastforce
  show ?thesis
    unfolding §
  proof (intro closedin_continuous_map_preimage)
    show "continuous_map X (prod_topology Y Y) (λx. (f x, g x))"
      by (simp add: continuous_map_pairedI f g)
    show "closedin (prod_topology Y Y) ((λy. (y, y)) ` topspace Y)"
      using Hausdorff_space_closedin_diagonal assms by blast
  qed
qed

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

lemma forall_in_closure_of_eq:
  assumes x: "x  X closure_of S"
    and Y: "Hausdorff_space Y" 
    and f: "continuous_map X Y f" and g: "continuous_map X Y g"
    and fg: "x. x  S  f x = g x"
  shows "f x = g x"
proof -
  have "closedin X {x  topspace X. f x = g x}"
    using Y closedin_continuous_maps_eq f g by blast
  then show ?thesis
    using forall_in_closure_of [OF x fg]
    by fastforce
qed
    
lemma retract_of_space_imp_closedin:
  assumes "Hausdorff_space X" and S: "S retract_of_space X"
  shows "closedin X S"
proof -
  obtain r where r: "continuous_map X (subtopology X S) r" "xS. r x = x"
    using assms by (meson retract_of_space_def)
  then have §: "S = {x  topspace X. r x = x}"
    using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff)
  show ?thesis
    unfolding § 
    using r continuous_map_into_fulltopology assms
    by (force intro: closedin_continuous_maps_eq)
qed

lemma homeomorphic_maps_graph:
   "homeomorphic_maps X (subtopology (prod_topology X Y) ((λx. (x, f x)) ` (topspace X)))
         (λx. (x, f x)) fst    continuous_map X Y f" 
   (is "?lhs=?rhs")
proof
  assume ?lhs
  then 
  have h: "homeomorphic_map X (subtopology (prod_topology X Y) ((λx. (x, f x)) ` topspace X)) (λx. (x, f x))"
    by (auto simp: homeomorphic_maps_map)
  have "f = snd  (λx. (x, f x))"
    by force
  then show ?rhs
    by (metis (no_types, lifting) h continuous_map_in_subtopology continuous_map_snd_of homeomorphic_eq_everything_map)
next
  assume ?rhs
  then show ?lhs
    unfolding homeomorphic_maps_def
    by (smt (verit, del_insts) continuous_map_eq continuous_map_subtopology_fst embedding_map_def 
        embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.sel(1))
qed


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

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

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

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

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

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

lemma kc_space_subtopology:
   "kc_space X  kc_space(subtopology X S)"
  by (metis closedin_Int_closure_of closure_of_eq compactin_subtopology inf.absorb2 kc_space_def)

lemma kc_space_discrete_topology:
   "kc_space(discrete_topology U)"
  using Hausdorff_space_discrete_topology compactin_imp_closedin kc_space_def by blast

lemma kc_space_continuous_injective_map_preimage:
  assumes "kc_space Y" "continuous_map X Y f" and injf: "inj_on f (topspace X)"
  shows "kc_space X"
  unfolding kc_space_def
proof (intro strip)
  fix S
  assume S: "compactin X S"
  have "S = {x  topspace X. f x  f ` S}"
    using S compactin_subset_topspace inj_onD [OF injf] by blast
  with assms S show "closedin X S"
    by (metis (no_types, lifting) Collect_cong closedin_continuous_map_preimage compactin_imp_closedin_gen image_compactin)
qed

lemma kc_space_retraction_map_image:
  assumes "retraction_map X Y r" "kc_space X"
  shows "kc_space Y"
proof -
  obtain s where s: "continuous_map X Y r" "continuous_map Y X s" "x. x  topspace Y  r (s x) = x"
    using assms by (force simp: retraction_map_def retraction_maps_def)
  then have inj: "inj_on s (topspace Y)"
    by (metis inj_on_def)
  show ?thesis
    unfolding kc_space_def
  proof (intro strip)
    fix S
    assume S: "compactin Y S"
    have "S = {x  topspace Y. s x  s ` S}"
      using S compactin_subset_topspace inj_onD [OF inj] by blast
    with assms S show "closedin Y S"
      by (meson compactin_imp_closedin_gen inj kc_space_continuous_injective_map_preimage s(2))
  qed
qed

lemma homeomorphic_kc_space:
   "X homeomorphic_space Y  kc_space X  kc_space Y"
  by (meson homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym kc_space_continuous_injective_map_preimage)

lemma compact_kc_eq_maximal_compact_space:
  assumes "compact_space X"
  shows "kc_space X 
         (Y. topspace Y = topspace X  (S. openin X S  openin Y S)  compact_space Y  Y = X)" (is "?lhs=?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (metis closedin_compact_space compactin_contractive kc_space_def topology_eq topology_finer_closedin)    
next
  assume R: ?rhs
  show ?lhs
    unfolding kc_space_def
  proof (intro strip)
    fix S
    assume S: "compactin X S"
    define Y where 
      "Y  topology (arbitrary union_of (finite intersection_of (λA. A = topspace X - S  openin X A)
                           relative_to (topspace X)))"
    have "topspace Y = topspace X"
      by (auto simp: Y_def)
    have "openin X T  openin Y T" for T
      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset_inc)
    have "compact_space Y"
    proof (rule Alexander_subbase_alt)
      show "ℱ'. finite ℱ'  ℱ'  𝒞  topspace X   ℱ'" 
        if 𝒞: "𝒞  insert (topspace X - S) (Collect (openin X))" and sub: "topspace X  𝒞" for 𝒞
      proof -
        consider "𝒞  Collect (openin X)" | 𝒱 where "𝒞 = insert (topspace X - S) 𝒱" "𝒱  Collect (openin X)"
          using 𝒞 by (metis insert_Diff subset_insert_iff)
        then show ?thesis
        proof cases
          case 1
          then show ?thesis
            by (metis assms compact_space_alt mem_Collect_eq subsetD that(2))
        next
          case 2
          then have "S  𝒱"
            using S sub compactin_subset_topspace by blast
          with 2 obtain  where "finite     𝒱  S  "
            using S unfolding compactin_def by (metis Ball_Collect)
          with 2 show ?thesis
            by (rule_tac x="insert (topspace X - S) " in exI) blast
        qed
      qed
    qed (auto simp: Y_def)
    have "Y = X"
      using R S. openin X S  openin Y S compact_space Y topspace Y = topspace X by blast
    moreover have "openin Y (topspace X - S)"
      by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset_inc)
    ultimately show "closedin X S"
      unfolding closedin_def using S compactin_subset_topspace by blast
  qed
qed

lemma continuous_imp_closed_map_gen:
   "compact_space X; kc_space Y; continuous_map X Y f  closed_map X Y f"
  by (meson closed_map_def closedin_compact_space compactin_imp_closedin_gen image_compactin)

lemma kc_space_compact_subtopologies:
  "kc_space X  (K. compactin X K  kc_space(subtopology X K))" (is "?lhs=?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: kc_space_def closedin_closed_subtopology compactin_subtopology)
next
  assume R: ?rhs
  show ?lhs
    unfolding kc_space_def
  proof (intro strip)
    fix K
    assume K: "compactin X K"
    then have "K  topspace X"
      by (simp add: compactin_subset_topspace)
    moreover have "X closure_of K  K"
    proof
      fix x
      assume x: "x  X closure_of K"
      have "kc_space (subtopology X K)"
        by (simp add: R compactin X K)
      have "compactin X (insert x K)"
        by (metis K x compactin_Un compactin_sing in_closure_of insert_is_Un)
      then show "x  K"
        by (metis R x K Int_insert_left_if1 closedin_Int_closure_of compact_imp_compactin_subtopology 
            insertCI kc_space_def subset_insertI)
    qed
    ultimately show "closedin X K"
      using closure_of_subset_eq by blast
  qed
qed

lemma kc_space_compact_prod_topology:
  assumes "compact_space X"
  shows "kc_space(prod_topology X X)  Hausdorff_space X" (is "?lhs=?rhs")
proof
  assume L: ?lhs
  show ?rhs
    unfolding closed_map_diag_eq [symmetric]
  proof (intro continuous_imp_closed_map_gen)
    show "continuous_map X (prod_topology X X) (λx. (x, x))"
      by (intro continuous_intros)
  qed (use L assms in auto)
next
  assume ?rhs then show ?lhs
    by (simp add: Hausdorff_imp_kc_space Hausdorff_space_prod_topology)
qed

lemma kc_space_prod_topology:
   "kc_space(prod_topology X X)  (K. compactin X K  Hausdorff_space(subtopology X K))" (is "?lhs=?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (metis compactin_subspace kc_space_compact_prod_topology kc_space_subtopology subtopology_Times)
next
  assume R: ?rhs  
  have "kc_space (subtopology (prod_topology X X) L)" if "compactin (prod_topology X X) L" for L 
  proof -
    define K where "K  fst ` L  snd ` L"
    have "L  K × K"
      by (force simp: K_def)
    have "compactin X K"
      by (metis K_def compactin_Un continuous_map_fst continuous_map_snd image_compactin that)
    then have "Hausdorff_space (subtopology X K)"
      by (simp add: R)
    then have "kc_space (prod_topology (subtopology X K) (subtopology X K))"
      by (simp add: compactin X K compact_space_subtopology kc_space_compact_prod_topology)
    then have "kc_space (subtopology (prod_topology (subtopology X K) (subtopology X K)) L)"
      using kc_space_subtopology by blast
    then show ?thesis
      using L  K × K subtopology_Times subtopology_subtopology
      by (metis (no_types, lifting) Sigma_cong inf.absorb_iff2)
  qed
  then show ?lhs
    using kc_space_compact_subtopologies by blast
qed

lemma kc_space_prod_topology_alt:
   "kc_space(prod_topology X X) 
        kc_space X 
        (K. compactin X K  Hausdorff_space(subtopology X K))"
  using Hausdorff_imp_kc_space kc_space_compact_subtopologies kc_space_prod_topology by blast

proposition kc_space_prod_topology_left:
  assumes X: "kc_space X" and Y: "Hausdorff_space Y"
  shows "kc_space (prod_topology X Y)"
  unfolding kc_space_def
proof (intro strip)
  fix K
  assume K: "compactin (prod_topology X Y) K"
  then have "K  topspace X × topspace Y"
    using compactin_subset_topspace topspace_prod_topology by blast
  moreover have "T. openin (prod_topology X Y) T  (a,b)  T  T  (topspace X × topspace Y) - K"
    if ab: "(a,b)  (topspace X × topspace Y) - K" for a b
  proof - 
    have "compactin Y {b}"
      using that by force
    moreover 
    have "compactin Y {y  topspace Y. (a,y)  K}"
    proof -
      have "compactin (prod_topology X Y) (K  {a} × topspace Y)"
        using that compact_Int_closedin [OF K]
        by (simp add: X closedin_prod_Times_iff compactin_imp_closedin_gen)
      moreover have "subtopology (prod_topology X Y) (K  {a} × topspace Y)  homeomorphic_space 
                     subtopology Y {y  topspace Y. (a, y)  K}"
        unfolding homeomorphic_space_def homeomorphic_maps_def
        using that
        apply (rule_tac x="snd" in exI)
        apply (rule_tac x="Pair a" in exI)
        by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology continuous_map_subtopology_snd continuous_map_paired)
      ultimately show ?thesis
        by (simp add: compactin_subspace homeomorphic_compact_space) 
    qed
    moreover have "disjnt {b} {y  topspace Y. (a,y)  K}"
      using ab by force
    ultimately obtain V U where VU: "openin Y V" "openin Y U" "{b}  V" "{y  topspace Y. (a,y)  K}  U" "disjnt V U"
      using Hausdorff_space_compact_separation [OF Y] by blast
    define V' where "V'  topspace Y - U"
    have W: "closedin Y V'" "{y  topspace Y. (a,y)  K}  topspace Y - V'" "disjnt V (topspace Y - V')"
      using VU by (auto simp: V'_def disjnt_iff)
    with VU obtain "V  topspace Y" "V'  topspace Y"
      by (meson closedin_subset openin_closedin_eq)
    then obtain "b  V" "disjnt {y  topspace Y. (a,y)  K} V'" "V  V'"
      using VU unfolding disjnt_iff V'_def by force
    define C where "C  image fst (K  {z  topspace(prod_topology X Y). snd z  V'})"
    have "closedin (prod_topology