(* 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 ⊆ (⋃i∈K. U i)" using assms U unfolding compactin_def by (smt (verit) finite_subset_image imageE) show ?thesis unfolding separated_between proof (intro conjI exI) have "⋀x. x ∈ K ⟹ closedin X (U x)" by (smt (verit) ‹K ⊆ S› Diff_cancel U(2) Un_Diff Un_Diff_Int disjnt_def openin_closedin_eq subsetD) then show "closedin X (⋃ (U ` K))" by (metis (mono_tags, lifting) ‹finite K› closedin_Union finite_imageI image_iff) show "openin X (⋃ (U ` K))" using U(1) ‹K ⊆ S› by blast show "S ⊆ ⋃ (U ` K)" by (simp add: K) have "⋀x i. ⟦x ∈ T; i ∈ K; x ∈ U i⟧ ⟹ False" by (meson U(2) ‹K ⊆ S› disjnt_iff subsetD) then show "T ⊆ topspace X - ⋃ (U ` K)" using ‹T ⊆ topspace X› by auto qed qed qed lemma separated_between_pointwise_right: "compactin X T ⟹ separated_between X S T ⟷ (T = {} ⟶ S ⊆ topspace X) ∧ (∀y ∈ T. separated_between X S {y})" by (meson separated_between_pointwise_left separated_between_sym) lemma separated_between_closure_of: "S ⊆ topspace X ⟹ separated_between X (X closure_of S) T ⟷ separated_between X S T" by (meson closure_of_minimal_eq separated_between_alt) lemma separated_between_closure_of': "T ⊆ topspace X ⟹ separated_between X S (X closure_of T) ⟷ separated_between X S T" by (meson separated_between_closure_of separated_between_sym) lemma separated_between_closure_of_eq: "separated_between X S T ⟷ S ⊆ topspace X ∧ separated_between X (X closure_of S) T" by (metis separated_between_closure_of separated_between_imp_subset) lemma separated_between_closure_of_eq': "separated_between X S T ⟷ T ⊆ topspace X ∧ separated_between X S (X closure_of T)" by (metis separated_between_closure_of' separated_between_imp_subset) lemma separated_between_frontier_of_eq': "separated_between X S T ⟷ T ⊆ topspace X ∧ disjnt S T ∧ separated_between X S (X frontier_of T)" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (metis interior_of_union_frontier_of separated_between_Un separated_between_closure_of_eq' separated_between_imp_disjoint) next assume R: ?rhs then obtain U where U: "closedin X U" "openin X U" "S ⊆ U" "X closure_of T - X interior_of T ⊆ topspace X - U" by (metis frontier_of_def separated_between) show ?lhs proof (rule separated_between_mono [of _ S "X closure_of T"]) have "separated_between X S T" unfolding separated_between proof (intro conjI exI) show "S ⊆ U - T" "T ⊆ topspace X - (U - T)" using R U(3) by (force simp: disjnt_iff)+ have "T ⊆ X closure_of T" by (simp add: R closure_of_subset) then have *: "U - T = U - X interior_of T" using U(4) interior_of_subset by fastforce then show "closedin X (U - T)" by (simp add: U(1) closedin_diff) have "U ∩ X frontier_of T = {}" using U(4) frontier_of_def by fastforce then show "openin X (U - T)" by (metis * Diff_Un U(2) Un_Diff_Int Un_Int_eq(1) closedin_closure_of interior_of_union_frontier_of openin_diff sup_bot_right) qed then show "separated_between X S (X closure_of T)" by (simp add: R separated_between_closure_of') qed (auto simp: R closure_of_subset) qed lemma separated_between_frontier_of_eq: "separated_between X S T ⟷ S ⊆ topspace X ∧ disjnt S T ∧ separated_between X (X frontier_of S) T" by (metis disjnt_sym separated_between_frontier_of_eq' separated_between_sym) lemma separated_between_frontier_of: "⟦S ⊆ topspace X; disjnt S T⟧ ⟹ (separated_between X (X frontier_of S) T ⟷ separated_between X S T)" using separated_between_frontier_of_eq by blast lemma separated_between_frontier_of': "⟦T ⊆ topspace X; disjnt S T⟧ ⟹ (separated_between X S (X frontier_of T) ⟷ separated_between X S T)" using separated_between_frontier_of_eq' by auto lemma connected_space_separated_between: "connected_space X ⟷ (∀S T. separated_between X S T ⟶ S = {} ∨ T = {})" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (metis Diff_cancel connected_space_clopen_in separated_between subset_empty) next assume ?rhs then show ?lhs by (meson connected_space_eq_not_separated separated_between_eq_separatedin) qed lemma connected_space_imp_separated_between_trivial: "connected_space X ⟹ (separated_between X S T ⟷ S = {} ∧ T ⊆ topspace X ∨ S ⊆ topspace X ∧ T = {})" by (metis connected_space_separated_between separated_between_empty) subsection‹Connected components› lemma connected_component_of_subtopology_eq: "connected_component_of (subtopology X U) a = connected_component_of X a ⟷ connected_component_of_set X a ⊆ U" by (force simp: connected_component_of_set connectedin_subtopology connected_component_of_def fun_eq_iff subset_iff) lemma connected_components_of_subtopology: assumes "C ∈ connected_components_of X" "C ⊆ U" shows "C ∈ connected_components_of (subtopology X U)" proof - obtain a where a: "connected_component_of_set X a ⊆ U" and "a ∈ topspace X" and Ceq: "C = connected_component_of_set X a" using assms by (force simp: connected_components_of_def) then have "a ∈ U" by (simp add: connected_component_of_refl in_mono) then have "connected_component_of_set X a = connected_component_of_set (subtopology X U) a" by (metis a connected_component_of_subtopology_eq) then show ?thesis by (simp add: Ceq ‹a ∈ U› ‹a ∈ topspace X› connected_component_in_connected_components_of) qed 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}i∈I. connected_component_of_set (X i) (x i))" if xX: "⋀i. i∈I ⟹ x i ∈ topspace (X i)" and ext: "x ∈ extensional I" proof (rule connected_component_of_unique) show "x ∈ ?R" by (simp add: PiE_iff connected_component_of_refl local.ext xX) show "connectedin (product_topology X I) ?R" by (simp add: connectedin_PiE connectedin_connected_component_of) show "C ⊆ ?R" if "x ∈ C ∧ connectedin (product_topology X I) C" for C proof - have "C ⊆ extensional I" using PiE_def connectedin_subset_topspace that by fastforce have "⋀y. y ∈ C ⟹ y ∈ (Π i∈I. connected_component_of_set (X i) (x i))" apply (simp add: connected_component_of_def Pi_def) by (metis connectedin_continuous_map_image continuous_map_product_projection imageI that) then show ?thesis using PiE_def ‹C ⊆ extensional I› by fastforce qed qed with True show ?thesis by (simp add: PiE_iff) next case False then show ?thesis 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})" 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" "∀x∈S. r x = x" using assms by (meson retract_of_space_def) then have §: "S = {x ∈ topspace X. r x = x}" using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff) show ?thesis unfolding § using r continuous_map_into_fulltopology assms by (force intro: closedin_continuous_maps_eq) qed lemma homeomorphic_maps_graph: "homeomorphic_maps X (subtopology (prod_topology X Y) ((λx. (x, f x)) ` (topspace X))) (λx. (x, f x)) fst ⟷ continuous_map X Y f" (is "?lhs=?rhs") proof assume ?lhs then have h: "homeomorphic_map X (subtopology (prod_topology X Y) ((λx. (x, f x)) ` topspace X)) (λx. (x, f x))" by (auto simp: homeomorphic_maps_map) have "f = snd ∘ (λx. (x, f x))" by force then show ?rhs by (metis (no_types, lifting) h continuous_map_in_subtopology continuous_map_snd_of homeomorphic_eq_everything_map) next assume ?rhs then show ?lhs unfolding homeomorphic_maps_def by (smt (verit, del_insts) continuous_map_eq continuous_map_subtopology_fst embedding_map_def embedding_map_graph homeomorphic_eq_everything_map image_cong image_iff prod.sel(1)) qed subsection ‹ KC spaces, those where all compact sets are closed.› definition kc_space where "kc_space X ≡ ∀S. compactin X S ⟶ closedin X S" lemma kc_space_euclidean: "kc_space (euclidean :: 'a::metric_space topology)" by (simp add: compact_imp_closed kc_space_def) lemma kc_space_expansive: "⟦kc_space X; topspace Y = topspace X; ⋀U. openin X U ⟹ openin Y U⟧ ⟹ kc_space Y" by (meson compactin_contractive kc_space_def topology_finer_closedin) lemma compactin_imp_closedin_gen: "⟦kc_space X; compactin X S⟧ ⟹ closedin X S" using kc_space_def by blast lemma Hausdorff_imp_kc_space: "Hausdorff_space X ⟹ kc_space X" by (simp add: compactin_imp_closedin kc_space_def) lemma kc_imp_t1_space: "kc_space X ⟹ t1_space X" by (simp add: finite_imp_compactin kc_space_def t1_space_closedin_finite) lemma kc_space_subtopology: "kc_space X ⟹ kc_space(subtopology X S)" by (metis closedin_Int_closure_of closure_of_eq compactin_subtopology inf.absorb2 kc_space_def) lemma kc_space_discrete_topology: "kc_space(discrete_topology U)" using Hausdorff_space_discrete_topology compactin_imp_closedin kc_space_def by blast lemma kc_space_continuous_injective_map_preimage: assumes "kc_space Y" "continuous_map X Y f" and injf: "inj_on f (topspace X)" shows "kc_space X" unfolding kc_space_def proof (intro strip) fix S assume S: "compactin X S" have "S = {x ∈ topspace X. f x ∈ f ` S}" using S compactin_subset_topspace inj_onD [OF injf] by blast with assms S show "closedin X S" by (metis (no_types, lifting) Collect_cong closedin_continuous_map_preimage compactin_imp_closedin_gen image_compactin) qed lemma kc_space_retraction_map_image: assumes "retraction_map X Y r" "kc_space X" shows "kc_space Y" proof - obtain s where s: "continuous_map X Y r" "continuous_map Y X s" "⋀x. x ∈ topspace Y ⟹ r (s x) = x" using assms by (force simp: retraction_map_def retraction_maps_def) then have inj: "inj_on s (topspace Y)" by (metis inj_on_def) show ?thesis unfolding kc_space_def proof (intro strip) fix S assume S: "compactin Y S" have "S = {x ∈ topspace Y. s x ∈ s ` S}" using S compactin_subset_topspace inj_onD [OF inj] by blast with assms S show "closedin Y S" by (meson compactin_imp_closedin_gen inj kc_space_continuous_injective_map_preimage s(2)) qed qed lemma homeomorphic_kc_space: "X homeomorphic_space Y ⟹ kc_space X ⟷ kc_space Y" by (meson homeomorphic_eq_everything_map homeomorphic_space homeomorphic_space_sym kc_space_continuous_injective_map_preimage) lemma compact_kc_eq_maximal_compact_space: assumes "compact_space X" shows "kc_space X ⟷ (∀Y. topspace Y = topspace X ∧ (∀S. openin X S ⟶ openin Y S) ∧ compact_space Y ⟶ Y = X)" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (metis closedin_compact_space compactin_contractive kc_space_def topology_eq topology_finer_closedin) next assume R: ?rhs show ?lhs unfolding kc_space_def proof (intro strip) fix S assume S: "compactin X S" define Y where "Y ≡ topology (arbitrary union_of (finite intersection_of (λA. A = topspace X - S ∨ openin X A) relative_to (topspace X)))" have "topspace Y = topspace X" by (auto simp: Y_def) have "openin X T ⟶ openin Y T" for T by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase openin_subset relative_to_subset_inc) have "compact_space Y" proof (rule Alexander_subbase_alt) show "∃ℱ'. finite ℱ' ∧ ℱ' ⊆ 𝒞 ∧ topspace X ⊆ ⋃ ℱ'" if 𝒞: "𝒞 ⊆ insert (topspace X - S) (Collect (openin X))" and sub: "topspace X ⊆ ⋃𝒞" for 𝒞 proof - consider "𝒞 ⊆ Collect (openin X)" | 𝒱 where "𝒞 = insert (topspace X - S) 𝒱" "𝒱 ⊆ Collect (openin X)" using 𝒞 by (metis insert_Diff subset_insert_iff) then show ?thesis proof cases case 1 then show ?thesis by (metis assms compact_space_alt mem_Collect_eq subsetD that(2)) next case 2 then have "S ⊆ ⋃𝒱" using S sub compactin_subset_topspace by blast with 2 obtain ℱ where "finite ℱ ∧ ℱ ⊆ 𝒱 ∧ S ⊆ ⋃ℱ" using S unfolding compactin_def by (metis Ball_Collect) with 2 show ?thesis by (rule_tac x="insert (topspace X - S) ℱ" in exI) blast qed qed qed (auto simp: Y_def) have "Y = X" using R ‹⋀S. openin X S ⟶ openin Y S› ‹compact_space Y› ‹topspace Y = topspace X› by blast moreover have "openin Y (topspace X - S)" by (simp add: Y_def arbitrary_union_of_inc finite_intersection_of_inc openin_subbase relative_to_subset_inc) ultimately show "closedin X S" unfolding closedin_def using S compactin_subset_topspace by blast qed qed lemma continuous_imp_closed_map_gen: "⟦compact_space X; kc_space Y; continuous_map X Y f⟧ ⟹ closed_map X Y f" by (meson closed_map_def closedin_compact_space compactin_imp_closedin_gen image_compactin) lemma kc_space_compact_subtopologies: "kc_space X ⟷ (∀K. compactin X K ⟶ kc_space(subtopology X K))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (auto simp: kc_space_def closedin_closed_subtopology compactin_subtopology) next assume R: ?rhs show ?lhs unfolding kc_space_def proof (intro strip) fix K assume K: "compactin X K" then have "K ⊆ topspace X" by (simp add: compactin_subset_topspace) moreover have "X closure_of K ⊆ K" proof fix x assume x: "x ∈ X closure_of K" have "kc_space (subtopology X K)" by (simp add: R ‹compactin X K›) have "compactin X (insert x K)" by (metis K x compactin_Un compactin_sing in_closure_of insert_is_Un) then show "x ∈ K" by (metis R x K Int_insert_left_if1 closedin_Int_closure_of compact_imp_compactin_subtopology insertCI kc_space_def subset_insertI) qed ultimately show "closedin X K" using closure_of_subset_eq by blast qed qed lemma kc_space_compact_prod_topology: assumes "compact_space X" shows "kc_space(prod_topology X X) ⟷ Hausdorff_space X" (is "?lhs=?rhs") proof assume L: ?lhs show ?rhs unfolding closed_map_diag_eq [symmetric] proof (intro continuous_imp_closed_map_gen) show "continuous_map X (prod_topology X X) (λx. (x, x))" by (intro continuous_intros) qed (use L assms in auto) next assume ?rhs then show ?lhs by (simp add: Hausdorff_imp_kc_space Hausdorff_space_prod_topology) qed lemma kc_space_prod_topology: "kc_space(prod_topology X X) ⟷ (∀K. compactin X K ⟶ Hausdorff_space(subtopology X K))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (metis compactin_subspace kc_space_compact_prod_topology kc_space_subtopology subtopology_Times) next assume R: ?rhs have "kc_space (subtopology (prod_topology X X) L)" if "compactin (prod_topology X X) L" for L proof - define K where "K ≡ fst ` L ∪ snd ` L" have "L ⊆ K × K" by (force simp: K_def) have "compactin X K" by (metis K_def compactin_Un continuous_map_fst continuous_map_snd image_compactin that) then have "Hausdorff_space (subtopology X K)" by (simp add: R) then have "kc_space (prod_topology (subtopology X K) (subtopology X K))" by (simp add: ‹compactin X K› compact_space_subtopology kc_space_compact_prod_topology) then have "kc_space (subtopology (prod_topology (subtopology X K) (subtopology X K)) L)" using kc_space_subtopology by blast then show ?thesis using ‹L ⊆ K × K› subtopology_Times subtopology_subtopology by (metis (no_types, lifting) Sigma_cong inf.absorb_iff2) qed then show ?lhs using kc_space_compact_subtopologies by blast qed lemma kc_space_prod_topology_alt: "kc_space(prod_topology X X) ⟷ kc_space X ∧ (∀K. compactin X K ⟶ Hausdorff_space(subtopology X K))" using Hausdorff_imp_kc_space kc_space_compact_subtopologies kc_space_prod_topology by blast proposition kc_space_prod_topology_left: assumes X: "kc_space X" and Y: "Hausdorff_space Y" shows "kc_space (prod_topology X Y)" unfolding kc_space_def proof (intro strip) fix K assume K: "compactin (prod_topology X Y) K" then have "K ⊆ topspace X × topspace Y" using compactin_subset_topspace topspace_prod_topology by blast moreover have "∃T. openin (prod_topology X Y) T ∧ (a,b) ∈ T ∧ T ⊆ (topspace X × topspace Y) - K" if ab: "(a,b) ∈ (topspace X × topspace Y) - K" for a b proof - have "compactin Y {b}" using that by force moreover have "compactin Y {y ∈ topspace Y. (a,y) ∈ K}" proof - have "compactin (prod_topology X Y) (K ∩ {a} × topspace Y)" using that compact_Int_closedin [OF K] by (simp add: X closedin_prod_Times_iff compactin_imp_closedin_gen) moreover have "subtopology (prod_topology X Y) (K ∩ {a} × topspace Y) homeomorphic_space subtopology Y {y ∈ topspace Y. (a, y) ∈ K}" unfolding homeomorphic_space_def homeomorphic_maps_def using that apply (rule_tac x="snd" in exI) apply (rule_tac x="Pair a" in exI) by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology continuous_map_subtopology_snd continuous_map_paired) ultimately show ?thesis by (simp add: compactin_subspace homeomorphic_compact_space) qed moreover have "disjnt {b} {y ∈ topspace Y. (a,y) ∈ K}" using ab by force ultimately obtain V U where VU: "openin Y V" "openin Y U" "{b} ⊆ V" "{y ∈ topspace Y. (a,y) ∈ K} ⊆ U" "disjnt V U" using Hausdorff_space_compact_separation [OF Y] by blast define V' where "V' ≡ topspace Y - U" have W: "closedin Y V'" "{y ∈ topspace Y. (a,y) ∈ K} ⊆ topspace Y - V'" "disjnt V (topspace Y - V')" using VU by (auto simp: V'_def disjnt_iff) with VU obtain "V ⊆ topspace Y" "V' ⊆ topspace Y" by (meson closedin_subset openin_closedin_eq) then obtain "b ∈ V" "disjnt {y ∈ topspace Y. (a,y) ∈ K} V'" "V ⊆ V'" using VU unfolding disjnt_iff V'_def by force define C where "C ≡ image fst (K ∩ {z ∈ topspace(prod_topology X Y). snd z ∈ V'})" have "closedin (prod_topology