Theory HOL-Analysis.T1_Spaces

section‹T1 and Hausdorff spaces›

theory T1_Spaces
imports Product_Topology
begin

section‹T1 spaces with equivalences to many naturally "nice" properties. ›

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

lemma t1_space_expansive:
   "topspace Y = topspace X; U. openin X U  openin Y U  t1_space X  t1_space Y"
  by (metis t1_space_def)

lemma t1_space_alt:
   "t1_space X  (x  topspace X. y  topspace X. xy  (U. closedin X U  x  U  y  U))"
 by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)

lemma t1_space_empty [iff]: "t1_space trivial_topology"
  by (simp add: t1_space_def)

lemma t1_space_derived_set_of_singleton:
  "t1_space X  (x  topspace X. X derived_set_of {x} = {})"
  apply (simp add: t1_space_def derived_set_of_def, safe)
   apply (metis openin_topspace)
  by force

lemma t1_space_derived_set_of_finite:
   "t1_space X  (S. finite S  X derived_set_of S = {})"
proof (intro iffI allI impI)
  fix S :: "'a set"
  assume "finite S"
  then have fin: "finite ((λx. {x}) ` (topspace X  S))"
    by blast
  assume "t1_space X"
  then have "X derived_set_of (x  topspace X  S. {x}) = {}"
    unfolding derived_set_of_Union [OF fin]
    by (auto simp: t1_space_derived_set_of_singleton)
  then have "X derived_set_of (topspace X  S) = {}"
    by simp
  then show "X derived_set_of S = {}"
    by simp
qed (auto simp: t1_space_derived_set_of_singleton)

lemma t1_space_closedin_singleton:
   "t1_space X  (x  topspace X. closedin X {x})"
  apply (rule iffI)
  apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
  using t1_space_alt by auto

lemma continuous_closed_imp_proper_map:
   "compact_space X; t1_space Y; continuous_map X Y f; closed_map X Y f  proper_map X Y f"
  unfolding proper_map_def
  by (smt (verit) closedin_compact_space closedin_continuous_map_preimage 
      Collect_cong singleton_iff t1_space_closedin_singleton)

lemma t1_space_euclidean: "t1_space (euclidean :: 'a::metric_space topology)"
  by (simp add: t1_space_closedin_singleton)

lemma closedin_t1_singleton:
   "t1_space X; a  topspace X  closedin X {a}"
  by (simp add: t1_space_closedin_singleton)

lemma t1_space_closedin_finite:
   "t1_space X  (S. finite S  S  topspace X  closedin X S)"
  apply (rule iffI)
  apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite)
  by (simp add: t1_space_closedin_singleton)

lemma closure_of_singleton:
   "t1_space X  X closure_of {a} = (if a  topspace X then {a} else {})"
  by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen)

lemma separated_in_singleton:
  assumes "t1_space X"
  shows "separatedin X {a} S  a  topspace X  S  topspace X  (a  X closure_of S)"
        "separatedin X S {a}  a  topspace X  S  topspace X  (a  X closure_of S)"
  unfolding separatedin_def
  using assms closure_of closure_of_singleton by fastforce+

lemma t1_space_openin_delete:
   "t1_space X  (U x. openin X U  x  U  openin X (U - {x}))"
  apply (rule iffI)
  apply (meson closedin_t1_singleton in_mono openin_diff openin_subset)
  by (simp add: closedin_def t1_space_closedin_singleton)

lemma t1_space_openin_delete_alt:
   "t1_space X  (U x. openin X U  openin X (U - {x}))"
  by (metis Diff_empty Diff_insert0 t1_space_openin_delete)


lemma t1_space_singleton_Inter_open:
      "t1_space X  (x  topspace X. {U. openin X U  x  U} = {x})"  (is "?P=?Q")
  and t1_space_Inter_open_supersets:
     "t1_space X  (S. S  topspace X  {U. openin X U  S  U} = S)" (is "?P=?R")
proof -
  have "?R  ?Q"
    apply clarify
    apply (drule_tac x="{x}" in spec, simp)
    done
  moreover have "?Q  ?P"
    apply (clarsimp simp add: t1_space_def)
    apply (drule_tac x=x in bspec)
     apply (simp_all add: set_eq_iff)
    by (metis (no_types, lifting))
  moreover have "?P  ?R"
  proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
    fix S
    assume S: "xtopspace X. closedin X {x}" "S  topspace X"
    then show " {U. openin X U  S  U}  S"
      apply clarsimp
      by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert)
  qed force
  ultimately show "?P=?Q" "?P=?R"
    by auto
qed

lemma t1_space_derived_set_of_infinite_openin:
   "t1_space X 
        (S. X derived_set_of S =
             {x  topspace X. U. x  U  openin X U  infinite(S  U)})"
         (is "_ = ?rhs")
proof
  assume "t1_space X"
  show ?rhs
  proof safe
    fix S x U
    assume "x  X derived_set_of S" "x  U" "openin X U" "finite (S  U)"
    with t1_space X show "False"
      apply (simp add: t1_space_derived_set_of_finite)
      by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym)
  next
    fix S x
    have eq: "(y. (y  x)  y  S  y  T)  ~((S  T)  {x})" for x S T
      by blast
    assume "x  topspace X" "U. x  U  openin X U  infinite (S  U)"
    then show "x  X derived_set_of S"
      apply (clarsimp simp add: derived_set_of_def eq)
      by (meson finite.emptyI finite.insertI finite_subset)
  qed (auto simp: in_derived_set_of)
qed (auto simp: t1_space_derived_set_of_singleton)

lemma finite_t1_space_imp_discrete_topology:
   "topspace X = U; finite U; t1_space X  X = discrete_topology U"
  by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)

lemma t1_space_subtopology: "t1_space X  t1_space(subtopology X U)"
  by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite)

lemma closedin_derived_set_of_gen:
   "t1_space X  closedin X (X derived_set_of S)"
  apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace)
  by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete)

lemma derived_set_of_derived_set_subset_gen:
   "t1_space X  X derived_set_of (X derived_set_of S)  X derived_set_of S"
  by (meson closedin_contains_derived_set closedin_derived_set_of_gen)

lemma subtopology_eq_discrete_topology_gen_finite:
   "t1_space X; finite S  subtopology X S = discrete_topology(topspace X  S)"
  by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)

lemma subtopology_eq_discrete_topology_finite:
   "t1_space X; S  topspace X; finite S
         subtopology X S = discrete_topology S"
  by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite)

lemma t1_space_closed_map_image:
   "closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X  t1_space Y"
  by (metis closed_map_def finite_subset_image t1_space_closedin_finite)

lemma homeomorphic_t1_space: "X homeomorphic_space Y  (t1_space X  t1_space Y)"
  apply (clarsimp simp add: homeomorphic_space_def)
  by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image)

proposition t1_space_product_topology:
   "t1_space (product_topology X I)
 (product_topology X I) = trivial_topology  (i  I. t1_space (X i))"
proof (cases "(product_topology X I) = trivial_topology")
  case True
  then show ?thesis
    using True t1_space_empty by force
next
  case False
  then obtain f where f: "f  (ΠE iI. topspace(X i))"
    using discrete_topology_unique by (fastforce iff: null_topspace_iff_trivial)
  have "t1_space (product_topology X I)  (iI. t1_space (X i))"
  proof (intro iffI ballI)
    show "t1_space (X i)" if "t1_space (product_topology X I)" and "i  I" for i
    proof -
      have clo: "h. h  (ΠE iI. topspace (X i))  closedin (product_topology X I) {h}"
        using that by (simp add: t1_space_closedin_singleton)
      show ?thesis
        unfolding t1_space_closedin_singleton
      proof clarify
        show "closedin (X i) {xi}" if "xi  topspace (X i)" for xi
          using clo [of "λj  I. if i=j then xi else f j"] f that i  I
          by (fastforce simp add: closedin_product_topology_singleton)
      qed
    qed
  next
  next
    show "t1_space (product_topology X I)" if "iI. t1_space (X i)"
      using that
      by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton)
  qed
  then show ?thesis
    using False by blast
qed

lemma t1_space_prod_topology:
   "t1_space(prod_topology X Y)  (prod_topology X Y) = trivial_topology  t1_space X  t1_space Y"
proof (cases "(prod_topology X Y) = trivial_topology")
  case True then show ?thesis
  by auto
next
  case False
  have eq: "{(x,y)} = {x} × {y}" for x::'a and y::'b
    by simp
  have "t1_space (prod_topology X Y)  (t1_space X  t1_space Y)"
    using False  
    apply(simp add: t1_space_closedin_singleton closedin_prod_Times_iff eq 
               del: insert_Times_insert flip: null_topspace_iff_trivial ex_in_conv)
    by blast
  with False show ?thesis
    by simp
qed

subsection‹Hausdorff Spaces›

definition Hausdorff_space
  where
 "Hausdorff_space X 
        x y. x  topspace X  y  topspace X  (x  y)
               (U V. openin X U  openin X V  x  U  y  V  disjnt U V)"

lemma Hausdorff_space_expansive:
   "Hausdorff_space X; topspace X = topspace Y; U. openin X U  openin Y U  Hausdorff_space Y"
  by (metis Hausdorff_space_def)

lemma Hausdorff_space_topspace_empty [iff]: "Hausdorff_space trivial_topology"
  by (simp add: Hausdorff_space_def)

lemma Hausdorff_imp_t1_space:
   "Hausdorff_space X  t1_space X"
  by (metis Hausdorff_space_def disjnt_iff t1_space_def)

lemma closedin_derived_set_of:
   "Hausdorff_space X  closedin X (X derived_set_of S)"
  by (simp add: Hausdorff_imp_t1_space closedin_derived_set_of_gen)

lemma t1_or_Hausdorff_space:
   "t1_space X  Hausdorff_space X  t1_space X"
  using Hausdorff_imp_t1_space by blast

lemma Hausdorff_space_sing_Inter_opens:
   "Hausdorff_space X; a  topspace X  {u. openin X u  a  u} = {a}"
  using Hausdorff_imp_t1_space t1_space_singleton_Inter_open by force

lemma Hausdorff_space_subtopology:
  assumes "Hausdorff_space X" shows "Hausdorff_space(subtopology X S)"
proof -
  have *: "disjnt U V  disjnt (S  U) (S  V)" for U V
    by (simp add: disjnt_iff)
  from assms show ?thesis
    apply (simp add: Hausdorff_space_def openin_subtopology_alt)
    apply (fast intro: * elim!: all_forward)
    done
qed

lemma Hausdorff_space_compact_separation:
  assumes X: "Hausdorff_space X" and S: "compactin X S" and T: "compactin X T" and "disjnt S T"
  obtains U V where "openin X U" "openin X V" "S  U" "T  V" "disjnt U V"
proof (cases "S = {}")
  case True
  then show thesis
    by (metis compactin X T compactin_subset_topspace disjnt_empty1 empty_subsetI openin_empty openin_topspace that)
next
  case False
  have "x  S. U V. openin X U  openin X V  x  U  T  V  disjnt U V"
  proof
    fix a
    assume "a  S"
    then have "a  T"
      by (meson assms(4) disjnt_iff)
    have a: "a  topspace X"
      using S a  S compactin_subset_topspace by blast
    show "U V. openin X U  openin X V  a  U  T  V  disjnt U V"
    proof (cases "T = {}")
      case True
      then show ?thesis
        using a disjnt_empty2 openin_empty by blast
    next
      case False
      have "x  topspace X - {a}. U V. openin X U  openin X V  x  U  a  V  disjnt U V"
        using X a by (simp add: Hausdorff_space_def)
      then obtain U V where UV: "x  topspace X - {a}. openin X (U x)  openin X (V x)  x  U x  a  V x  disjnt (U x) (V x)"
        by metis
      with a  T compactin_subset_topspace [OF T]
      have Topen: "W  U ` T. openin X W" and Tsub: "T   (U ` T)"
        by auto
      then obtain  where : "finite " "  U ` T" and "T  "
        using T unfolding compactin_def by meson
      then obtain F where F: "finite F" "F  T" " = U ` F" and SUF: "T  (U ` F)" and "a  F"
        using finite_subset_image [OF ] a  T by (metis subsetD)
      have U: "x. x  topspace X; x  a  openin X (U x)"
        and V: "x. x  topspace X; x  a  openin X (V x)"
        and disj: "x. x  topspace X; x  a  disjnt (U x) (V x)"
        using UV by blast+
      show ?thesis
      proof (intro exI conjI)
        have "F  {}"
          using False SUF by blast
        with a  F show "openin X ((V ` F))"
          using F compactin_subset_topspace [OF T] by (force intro: V)
        show "openin X ((U ` F))"
          using F Topen Tsub by (force intro: U)
        show "disjnt ((V ` F)) ((U ` F))"
          using disj
          apply (auto simp: disjnt_def)
          using F  T a  F compactin_subset_topspace [OF T] by blast
        show "a  ((V ` F))"
          using F  T T UV a  T compactin_subset_topspace by blast
      qed (auto simp: SUF)
    qed
  qed
  then obtain U V where UV: "x  S. openin X (U x)  openin X (V x)  x  U x  T  V x  disjnt (U x) (V x)"
    by metis
  then have "S   (U ` S)"
    by auto
  moreover have "W  U ` S. openin X W"
    using UV by blast
  ultimately obtain I where I: "S   (U ` I)" "I  S" "finite I"
    by (metis S compactin_def finite_subset_image)
  show thesis
  proof
    show "openin X ((U ` I))"
      using I  S UV by blast
    show "openin X ( (V ` I))"
      using False UV I  S S   (U ` I) finite I by blast
    show "disjnt ((U ` I)) ( (V ` I))"
      by simp (meson UV I  S disjnt_subset2 in_mono le_INF_iff order_refl)
  qed (use UV I in auto)
qed


lemma Hausdorff_space_compact_sets:
  "Hausdorff_space X 
    (S T. compactin X S  compactin 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
    by (meson Hausdorff_space_compact_separation)
next
  assume R [rule_format]: ?rhs
  show ?lhs
  proof (clarsimp simp add: Hausdorff_space_def)
    fix x y
    assume "x  topspace X" "y  topspace X" "x  y"
    then show "U. openin X U  (V. openin X V  x  U  y  V  disjnt U V)"
      using R [of "{x}" "{y}"] by auto
  qed
qed

lemma compactin_imp_closedin:
  assumes X: "Hausdorff_space X" and S: "compactin X S" shows "closedin X S"
proof -
  have "S  topspace X"
    by (simp add: assms compactin_subset_topspace)
  moreover
  have "T. openin X T  x  T  T  topspace X - S" if "x  topspace X" "x  S" for x
    using Hausdorff_space_compact_separation [OF X _ S, of "{x}"] that
    apply (simp add: disjnt_def)
    by (metis Diff_mono Diff_triv openin_subset)
  ultimately show ?thesis
    using closedin_def openin_subopen by force
qed

lemma closedin_Hausdorff_singleton:
   "Hausdorff_space X; x  topspace X  closedin X {x}"
  by (simp add: Hausdorff_imp_t1_space closedin_t1_singleton)

lemma closedin_Hausdorff_sing_eq:
   "Hausdorff_space X  closedin X {x}  x  topspace X"
  by (meson closedin_Hausdorff_singleton closedin_subset insert_subset)

lemma Hausdorff_space_discrete_topology [simp]:
   "Hausdorff_space (discrete_topology U)"
  unfolding Hausdorff_space_def
  by (metis Hausdorff_space_compact_sets Hausdorff_space_def compactin_discrete_topology equalityE openin_discrete_topology)

lemma compactin_Int:
   "Hausdorff_space X; compactin X S; compactin X T  compactin X (S  T)"
  by (simp add: closed_Int_compactin compactin_imp_closedin)

lemma finite_topspace_imp_discrete_topology:
   "topspace X = U; finite U; Hausdorff_space X  X = discrete_topology U"
  using Hausdorff_imp_t1_space finite_t1_space_imp_discrete_topology by blast

lemma derived_set_of_finite:
   "Hausdorff_space X; finite S  X derived_set_of S = {}"
  using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto

lemma infinite_perfect_set:
   "Hausdorff_space X; S  X derived_set_of S; S  {}  infinite S"
  using derived_set_of_finite by blast

lemma derived_set_of_singleton:
   "Hausdorff_space X  X derived_set_of {x} = {}"
  by (simp add: derived_set_of_finite)

lemma closedin_Hausdorff_finite:
   "Hausdorff_space X; S  topspace X; finite S  closedin X S"
  by (simp add: compactin_imp_closedin finite_imp_compactin_eq)

lemma open_in_Hausdorff_delete:
   "Hausdorff_space X; openin X S  openin X (S - {x})"
  using Hausdorff_imp_t1_space t1_space_openin_delete_alt by auto

lemma closedin_Hausdorff_finite_eq:
   "Hausdorff_space X; finite S  closedin X S  S  topspace X"
  by (meson closedin_Hausdorff_finite closedin_def)

lemma derived_set_of_infinite_openin:
   "Hausdorff_space X
         X derived_set_of S =
            {x  topspace X. U. x  U  openin X U  infinite(S  U)}"
  using Hausdorff_imp_t1_space t1_space_derived_set_of_infinite_openin by fastforce

lemma Hausdorff_space_discrete_compactin:
   "Hausdorff_space X
         S  X derived_set_of S = {}  compactin X S  S  topspace X  finite S"
  using derived_set_of_finite discrete_compactin_eq_finite by fastforce

lemma Hausdorff_space_finite_topspace:
   "Hausdorff_space X  X derived_set_of (topspace X) = {}  compact_space X  finite(topspace X)"
  using derived_set_of_finite discrete_compact_space_eq_finite by auto

lemma derived_set_of_derived_set_subset:
   "Hausdorff_space X  X derived_set_of (X derived_set_of S)  X derived_set_of S"
  by (simp add: Hausdorff_imp_t1_space derived_set_of_derived_set_subset_gen)


lemma Hausdorff_space_injective_preimage:
  assumes "Hausdorff_space Y" and cmf: "continuous_map X Y f" and "inj_on f (topspace X)"
  shows "Hausdorff_space X"
  unfolding Hausdorff_space_def
proof clarify
  fix x y
  assume x: "x  topspace X" and y: "y  topspace X" and "x  y"
  then obtain U V where "openin Y U" "openin Y V" "f x  U" "f y  V" "disjnt U V"
    using assms
    by (smt (verit, ccfv_threshold) Hausdorff_space_def continuous_map image_subset_iff inj_on_def)
  show "U V. openin X U  openin X V  x  U  y  V  disjnt U V"
  proof (intro exI conjI)
    show "openin X {x  topspace X. f x  U}"
      using openin Y U cmf continuous_map by fastforce
    show "openin X {x  topspace X. f x  V}"
      using openin Y V cmf openin_continuous_map_preimage by blast
    show "disjnt {x  topspace X. f x  U} {x  topspace X. f x  V}"
      using disjnt U V by (auto simp add: disjnt_def)
  qed (use x f x  U y f y  V in auto)
qed

lemma homeomorphic_Hausdorff_space:
   "X homeomorphic_space Y  Hausdorff_space X  Hausdorff_space Y"
  unfolding homeomorphic_space_def homeomorphic_maps_map
  by (auto simp: homeomorphic_eq_everything_map Hausdorff_space_injective_preimage)

lemma Hausdorff_space_retraction_map_image:
   "retraction_map X Y r; Hausdorff_space X  Hausdorff_space Y"
  unfolding retraction_map_def
  using Hausdorff_space_subtopology homeomorphic_Hausdorff_space retraction_maps_section_image2 by blast

lemma compact_Hausdorff_space_optimal:
  assumes eq: "topspace Y = topspace X" and XY: "U. openin X U  openin Y U"
      and "Hausdorff_space X" "compact_space Y"
    shows "Y = X"
proof -
  have "U. closedin X U  closedin Y U"
    using XY using topology_finer_closedin [OF eq]
    by metis
  have "openin Y S = openin X S" for S
    by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq)
  then show ?thesis
    by (simp add: topology_eq)
qed

lemma continuous_map_imp_closed_graph:
  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
  shows "closedin (prod_topology X Y) ((λx. (x,f x)) ` topspace X)"
  unfolding closedin_def
proof
  show "(λx. (x, f x)) ` topspace X  topspace (prod_topology X Y)"
    using continuous_map_def f by fastforce
  show "openin (prod_topology X Y) (topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X)"
    unfolding openin_prod_topology_alt
  proof (intro allI impI)
    show "U V. openin X U  openin Y V  x  U  y  V  U × V  topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X"
      if "(x,y)  topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X"
      for x y
    proof -
      have "x  topspace X" and y: "y  topspace Y" "y  f x"
        using that by auto
      then have "f x  topspace Y"
        using continuous_map_image_subset_topspace f by blast
      then obtain U V where UV: "openin Y U" "openin Y V" "f x  U" "y  V" "disjnt U V"
        using Y y Hausdorff_space_def by metis
      show ?thesis
      proof (intro exI conjI)
        show "openin X {x  topspace X. f x  U}"
          using openin Y U f openin_continuous_map_preimage by blast
        show "{x  topspace X. f x  U} × V  topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X"
          using UV by (auto simp: disjnt_iff dest: openin_subset)
      qed (use UV x  topspace X in auto)
    qed
  qed
qed

lemma continuous_imp_closed_map:
   "continuous_map X Y f; compact_space X; Hausdorff_space Y  closed_map X Y f"
  by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin)

lemma continuous_imp_quotient_map:
   "continuous_map X Y f; compact_space X; Hausdorff_space Y; f ` (topspace X) = topspace Y
         quotient_map X Y f"
  by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map)

lemma continuous_imp_homeomorphic_map:
   "continuous_map X Y f; compact_space X; Hausdorff_space Y; 
     f ` (topspace X) = topspace Y; inj_on f (topspace X)
         homeomorphic_map X Y f"
  by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map)

lemma continuous_imp_embedding_map:
   "continuous_map X Y f; compact_space X; Hausdorff_space Y; inj_on f (topspace X)
         embedding_map X Y f"
  by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map)

lemma continuous_inverse_map:
  assumes "compact_space X" "Hausdorff_space Y"
    and cmf: "continuous_map X Y f" and gf: "x. x  topspace X  g(f x) = x"
    and Sf:  "S  f ` (topspace X)"
  shows "continuous_map (subtopology Y S) X g"
proof (rule continuous_map_from_subtopology_mono [OF _ S  f ` (topspace X)])
  show "continuous_map (subtopology Y (f ` (topspace X))) X g"
    unfolding continuous_map_closedin
  proof (intro conjI ballI allI impI)
    show "g  topspace (subtopology Y (f ` topspace X))  topspace X"
      using gf by auto
  next
    fix C
    assume C: "closedin X C"
    show "closedin (subtopology Y (f ` topspace X))
           {x  topspace (subtopology Y (f ` topspace X)). g x  C}"
    proof (rule compactin_imp_closedin)
      show "Hausdorff_space (subtopology Y (f ` topspace X))"
        using Hausdorff_space_subtopology [OF Hausdorff_space Y] by blast
      have "compactin Y (f ` C)"
        using C cmf image_compactin closedin_compact_space [OF compact_space X] by blast
      moreover have "{x  topspace Y. x  f ` topspace X  g x  C} = f ` C"
        using closedin_subset [OF C] cmf by (auto simp: gf continuous_map_def)
      ultimately have "compactin Y {x  topspace Y. x  f ` topspace X  g x  C}"
        by simp
      then show "compactin (subtopology Y (f ` topspace X))
              {x  topspace (subtopology Y (f ` topspace X)). g x  C}"
        by (auto simp add: compactin_subtopology)
    qed
  qed
qed

lemma closed_map_paired_continuous_map_right:
   "continuous_map X Y f; Hausdorff_space Y  closed_map X (prod_topology X Y) (λx. (x,f x))"
  by (simp add: continuous_map_imp_closed_graph embedding_map_graph embedding_imp_closed_map)

lemma closed_map_paired_continuous_map_left:
  assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y"
  shows "closed_map X (prod_topology Y X) (λx. (f x,x))"
proof -
  have eq: "(λx. (f x,x)) = (λ(a,b). (b,a))  (λ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))"
      using Y closed_map_paired_continuous_map_right f by blast
    show "closed_map (prod_topology X Y) (prod_topology Y X) (λ(a, b). (b, a))"
      by (metis homeomorphic_map_swap homeomorphic_imp_closed_map)
  qed
qed

lemma proper_map_paired_continuous_map_right:
   "continuous_map X Y f; Hausdorff_space Y
         proper_map X (prod_topology X Y) (λx. (x,f x))"
  using closed_injective_imp_proper_map closed_map_paired_continuous_map_right
  by (metis (mono_tags, lifting) Pair_inject inj_onI)

lemma proper_map_paired_continuous_map_left:
   "continuous_map X Y f; Hausdorff_space Y
         proper_map X (prod_topology Y X) (λx. (f x,x))"
  using closed_injective_imp_proper_map closed_map_paired_continuous_map_left
  by (metis (mono_tags, lifting) Pair_inject inj_onI)

lemma Hausdorff_space_prod_topology:
  "Hausdorff_space(prod_topology X Y)  (prod_topology X Y) = trivial_topology  Hausdorff_space X  Hausdorff_space Y"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (rule topological_property_of_prod_component) (auto simp: Hausdorff_space_subtopology homeomorphic_Hausdorff_space)
next
  assume R: ?rhs
  show ?lhs
  proof (cases "(topspace X × topspace Y) = {}")
    case False
    with R have ne: "topspace X  {}" "topspace Y  {}" and X: "Hausdorff_space X" and Y: "Hausdorff_space Y"
      by auto
    show ?thesis
      unfolding Hausdorff_space_def
    proof clarify
      fix x y x' y'
      assume xy: "(x, y)  topspace (prod_topology X Y)"
        and xy': "(x',y')  topspace (prod_topology X Y)"
        and *: "U V. openin (prod_topology X Y) U  openin (prod_topology X Y) V
                (x, y)  U  (x', y')  V  disjnt U V"
      have False if "x  x'  y  y'"
        using that
      proof
        assume "x  x'"
        then obtain U V where "openin X U" "openin X V" "x  U" "x'  V" "disjnt U V"
          by (metis Hausdorff_space_def X mem_Sigma_iff topspace_prod_topology xy xy')
        let ?U = "U × topspace Y"
        let ?V = "V × topspace Y"
        have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
          by (simp_all add: openin_prod_Times_iff openin X U openin X V)
        moreover have "disjnt ?U ?V"
          by (simp add: disjnt U V)
        ultimately show False
          using * x  U x'  V xy xy' by (metis SigmaD2 SigmaI topspace_prod_topology)
      next
        assume "y  y'"
        then obtain U V where "openin Y U" "openin Y V" "y  U" "y'  V" "disjnt U V"
          by (metis Hausdorff_space_def Y mem_Sigma_iff topspace_prod_topology xy xy')
        let ?U = "topspace X × U"
        let ?V = "topspace X × V"
        have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V"
          by (simp_all add: openin_prod_Times_iff openin Y U openin Y V)
        moreover have "disjnt ?U ?V"
          by (simp add: disjnt U V)
        ultimately show False
          using "*" y  U y'  V xy xy' by (metis SigmaD1 SigmaI topspace_prod_topology)
      qed
      then show "x = x'  y = y'"
        by blast
    qed
  qed force
qed


lemma Hausdorff_space_product_topology:
   "Hausdorff_space (product_topology X I)  (ΠE iI. topspace(X i)) = {}  (i  I. Hausdorff_space (X i))"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (simp add: Hausdorff_space_subtopology PiE_eq_empty_iff homeomorphic_Hausdorff_space 
                  topological_property_of_product_component)
next
  assume R: ?rhs
  show ?lhs
  proof (cases "(ΠE iI. topspace(X i)) = {}")
    case True
    then show ?thesis
      by (simp add: Hausdorff_space_def)
  next
    case False
    have "U V. openin (product_topology X I) U  openin (product_topology X I) V  f  U  g  V  disjnt U V"
      if f: "f  (ΠE iI. topspace (X i))" and g: "g  (ΠE iI. topspace (X i))" and "f  g"
      for f g :: "'a  'b"
    proof -
      obtain m where "f m  g m"
        using f  g by blast
      then have "m  I"
        using f g by fastforce
      then have "Hausdorff_space (X m)" 
        using False that R by blast
      then obtain U V where U: "openin (X m) U" and V: "openin (X m) V" and "f m  U" "g m  V" "disjnt U V"
        by (metis Hausdorff_space_def PiE_mem f m  g m m  I f g)
      show ?thesis
      proof (intro exI conjI)
        let ?U = "(ΠE iI. topspace(X i))  {x. x m  U}"
        let ?V = "(ΠE iI. topspace(X i))  {x. x m  V}"
        show "openin (product_topology X I) ?U" "openin (product_topology X I) ?V"
          using m  I U V
          by (force simp add: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)+
        show "f  ?U"
          using f m  U f by blast
        show "g  ?V"
          using g m  V g by blast
        show "disjnt ?U ?V"
          using disjnt U V by (auto simp: PiE_def Pi_def disjnt_def)
        qed
    qed
    then show ?thesis
      by (simp add: Hausdorff_space_def)   
  qed
qed

lemma Hausdorff_space_closed_neighbourhood:
   "Hausdorff_space X 
    (x  topspace X. U C. openin X U  closedin X C 
                      Hausdorff_space(subtopology X C)  x  U  U  C)" (is "_ = ?rhs")
proof
  assume R: ?rhs
  show "Hausdorff_space X"
    unfolding Hausdorff_space_def
  proof clarify
    fix x y
    assume x: "x  topspace X" and y: "y  topspace X" and "x  y"
    obtain T C where *: "openin X T" "closedin X C" "x  T" "T  C"
                 and C: "Hausdorff_space (subtopology X C)"
      by (meson R x  topspace X)
    show "U V. openin X U  openin X V  x  U  y  V  disjnt U V"
    proof (cases "y  C")
      case True
      with * C obtain U V where U: "openin (subtopology X C) U"
                        and V: "openin (subtopology X C) V"
                        and "x  U" "y  V" "disjnt U V"
        unfolding Hausdorff_space_def
        by (smt (verit, best) x  y closedin_subset subsetD topspace_subtopology_subset)
      then obtain U' V' where UV': "U = U'  C" "openin X U'" "V = V'  C" "openin X V'"
        by (meson openin_subtopology)
      have "disjnt (T  U') V'"
        using disjnt U V UV' T  C by (force simp: disjnt_iff)
      with T  C have "disjnt (T  U') (V'  (topspace X - C))"
        unfolding disjnt_def by blast
      moreover
      have "openin X (T  U')"
        by (simp add: openin X T openin X U' openin_Int)
      moreover have "openin X (V'  (topspace X - C))"
        using closedin X C openin X V' by auto
      ultimately show ?thesis
        using UV' x  T x  U y  V by blast
    next
      case False
      with * y show ?thesis
        by (force simp: closedin_def disjnt_def)
    qed
  qed
qed fastforce

end