# 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"

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"

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"
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)"

lemma separated_between_pointwise_left:
assumes "compactin X S"
shows "separated_between X S T ⟷
(S = {} ⟶ T ⊆ topspace X) ∧ (∀x ∈ S. separated_between X {x} T)"  (is "?lhs=?rhs")
proof
assume ?lhs then show ?rhs
using separated_between_imp_subset separated_between_mono by fastforce
next
assume R: ?rhs
then have "T ⊆ topspace X"
by (meson equals0I separated_between_imp_subset)
show ?lhs
proof -
obtain U where U: "∀x ∈ S. openin X (U x)"
"∀x ∈ S. ∃V. openin X V ∧ U x ∪ V = topspace X ∧ disjnt (U x) V ∧ {x} ⊆ U x ∧ T ⊆ V"
using R unfolding separated_between_def by metis
then have "S ⊆ ⋃(U ` S)"
by blast
then obtain K where "finite K" "K ⊆ S" and K: "S ⊆ (⋃i∈K. U i)"
using assms U unfolding compactin_def by (smt (verit) finite_subset_image imageE)
show ?thesis
unfolding separated_between
proof (intro conjI exI)
have "⋀x. x ∈ K ⟹ closedin X (U x)"
by (smt (verit) ‹K ⊆ S› Diff_cancel U(2) Un_Diff Un_Diff_Int disjnt_def openin_closedin_eq subsetD)
then show "closedin X (⋃ (U ` K))"
by (metis (mono_tags, lifting) ‹finite K› closedin_Union finite_imageI image_iff)
show "openin X (⋃ (U ` K))"
using U(1) ‹K ⊆ S› by blast
show "S ⊆ ⋃ (U ` K)"
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"
then have *: "U - T = U - X interior_of T"
using U(4) interior_of_subset by fastforce
then show "closedin X (U - T)"
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)"
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"
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)"

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"

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

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

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

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

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

lemma connected_component_of_product_topology:
"connected_component_of_set (product_topology X I) x =
(if x ∈ extensional I then PiE I (λi. connected_component_of_set (X i) (x i)) else {})"
(is "?lhs = If _ ?R _")
proof (cases "x ∈ topspace(product_topology X I)")
case True
have "?lhs = (Π⇩E i∈I. connected_component_of_set (X i) (x i))"
if xX: "⋀i. i∈I ⟹ x i ∈ topspace (X i)" and ext: "x ∈ extensional I"
proof (rule connected_component_of_unique)
show "x ∈ ?R"
by (simp add: PiE_iff connected_component_of_refl local.ext xX)
show "connectedin (product_topology X I) ?R"
show "C ⊆ ?R"
if "x ∈ C ∧ connectedin (product_topology X I) C" for C
proof -
have "C ⊆ extensional I"
using PiE_def connectedin_subset_topspace that by fastforce
have "⋀y. y ∈ C ⟹ y ∈ (Π i∈I. connected_component_of_set (X i) (x i))"
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
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 = Pi⇩E I B" and
"∀i∈I. ∃x∈topspace (X i). B i = connected_component_of_set (X i) x"
by (force simp: connected_components_of_def connected_component_of_product_topology image_iff)
then obtain f where
f: "⋀i. i ∈ I ⟹ f i ∈ topspace (X i) ∧ B i = connected_component_of_set (X i) (f i)"
by metis
then have "(λi∈I. f i) ∈ ((Π⇩E i∈I. topspace (X i)) ∩ extensional I)"
by simp
with f show "F ∈ ?lhs"
unfolding Feq connected_components_of_def connected_component_of_product_topology image_iff
by (smt (verit, del_insts) PiE_cong restrict_PiE_iff restrict_apply' restrict_extensional topspace_product_topology)
qed
qed

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

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

lemma monotone_map:
"monotone_map X Y f ⟷
f ` (topspace X) ⊆ topspace Y ∧ (∀y. connectedin X {x ∈ topspace X. f x = y})"
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"

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
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"
ultimately show ?thesis
using ‹monotone_map X Y f› connected_space_monotone_quotient_map_preimage monotone_map_restriction by blast
qed
then show ?thesis
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"
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 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
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"
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 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
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"
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"
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)))"
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)"
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}"
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})"
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"

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)"

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

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

lemma XY: "{x}×{y} = {(x,y)}"
by simp

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

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

proposition t0_space_product_topology:
"t0_space (product_topology X I) ⟷ product_topology X I = trivial_topology ∨ (∀i ∈ I. t0_space (X i))"
(is "?lhs=?rhs")
proof
assume ?lhs
then show ?rhs
by (meson retraction_map_product_projection t0_space_retraction_map_image)
next
assume R: ?rhs
show ?lhs
proof (cases "product_topology X I = trivial_topology")
case True
then show ?thesis
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)
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"

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
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"

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)"
then have "Kolmogorov_quotient X ` topspace X ⊆ topspace X"
then show ?thesis
by (meson retract_of_space_retraction_maps retraction_maps_Kolmogorov_quotient)
qed

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

subsection‹Closed diagonals and graphs›

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

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

lemma proper_map_diag_eq [simp]:
"proper_map X (prod_topology X X) (λx. (x,x)) ⟷ Hausdorff_space X"
by (simp add: closed_map_diag_eq inj_on_convol_ident injective_imp_proper_eq_closed_map)

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

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

lemma forall_in_closure_of_eq:
assumes x: "x ∈ X closure_of S"
and Y: "Hausdorff_space Y"
and f: "continuous_map X Y f" and g: "continuous_map X Y g"
and fg: "⋀x. x ∈ S ⟹ f x = g x"
shows "f x = g x"
proof -
have "closedin X {x ∈ topspace X. f x = g x}"
using Y closedin_continuous_maps_eq f g by blast
then show ?thesis
using forall_in_closure_of [OF x fg]
by fastforce
qed

lemma retract_of_space_imp_closedin:
assumes "Hausdorff_space X" and S: "S retract_of_space X"
shows "closedin X S"
proof -
obtain r where r: "continuous_map X (subtopology X S) r" "∀x∈S. r x = x"
using assms by (meson retract_of_space_def)
then have §: "S = {x ∈ topspace X. r x = x}"
using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff)
show ?thesis
unfolding §
using r continuous_map_into_fulltopology assms
by (force intro: closedin_continuous_maps_eq)
qed

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

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

definition kc_space
where "kc_space X ≡ ∀S. compactin X S ⟶ closedin X S"

lemma kc_space_euclidean: "kc_space (euclidean :: 'a::metric_space topology)"

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"

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"
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
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)"
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