section‹T1 and Hausdorff spaces› theory T1_Spaces imports Product_Topology begin section‹T1 spaces with equivalences to many naturally "nice" properties. › definition t1_space where "t1_space X ≡ ∀x ∈ topspace X. ∀y ∈ topspace X. x≠y ⟶ (∃U. openin X U ∧ x ∈ U ∧ y ∉ U)" lemma t1_space_expansive: "⟦topspace Y = topspace X; ⋀U. openin X U ⟹ openin Y U⟧ ⟹ t1_space X ⟹ t1_space Y" by (metis t1_space_def) lemma t1_space_alt: "t1_space X ⟷ (∀x ∈ topspace X. ∀y ∈ topspace X. x≠y ⟶ (∃U. closedin X U ∧ x ∈ U ∧ y ∉ U))" by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def) lemma t1_space_empty [iff]: "t1_space trivial_topology" by (simp add: t1_space_def) lemma t1_space_derived_set_of_singleton: "t1_space X ⟷ (∀x ∈ topspace X. X derived_set_of {x} = {})" apply (simp add: t1_space_def derived_set_of_def, safe) apply (metis openin_topspace) by force lemma t1_space_derived_set_of_finite: "t1_space X ⟷ (∀S. finite S ⟶ X derived_set_of S = {})" proof (intro iffI allI impI) fix S :: "'a set" assume "finite S" then have fin: "finite ((λx. {x}) ` (topspace X ∩ S))" by blast assume "t1_space X" then have "X derived_set_of (⋃x ∈ topspace X ∩ S. {x}) = {}" unfolding derived_set_of_Union [OF fin] by (auto simp: t1_space_derived_set_of_singleton) then have "X derived_set_of (topspace X ∩ S) = {}" by simp then show "X derived_set_of S = {}" by simp qed (auto simp: t1_space_derived_set_of_singleton) lemma t1_space_closedin_singleton: "t1_space X ⟷ (∀x ∈ topspace X. closedin X {x})" apply (rule iffI) apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton) using t1_space_alt by auto lemma continuous_closed_imp_proper_map: "⟦compact_space X; t1_space Y; continuous_map X Y f; closed_map X Y f⟧ ⟹ proper_map X Y f" unfolding proper_map_def by (smt (verit) closedin_compact_space closedin_continuous_map_preimage Collect_cong singleton_iff t1_space_closedin_singleton) lemma t1_space_euclidean: "t1_space (euclidean :: 'a::metric_space topology)" by (simp add: t1_space_closedin_singleton) lemma closedin_t1_singleton: "⟦t1_space X; a ∈ topspace X⟧ ⟹ closedin X {a}" by (simp add: t1_space_closedin_singleton) lemma t1_space_closedin_finite: "t1_space X ⟷ (∀S. finite S ∧ S ⊆ topspace X ⟶ closedin X S)" apply (rule iffI) apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite) by (simp add: t1_space_closedin_singleton) lemma closure_of_singleton: "t1_space X ⟹ X closure_of {a} = (if a ∈ topspace X then {a} else {})" by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen) lemma separated_in_singleton: assumes "t1_space X" shows "separatedin X {a} S ⟷ a ∈ topspace X ∧ S ⊆ topspace X ∧ (a ∉ X closure_of S)" "separatedin X S {a} ⟷ a ∈ topspace X ∧ S ⊆ topspace X ∧ (a ∉ X closure_of S)" unfolding separatedin_def using assms closure_of closure_of_singleton by fastforce+ lemma t1_space_openin_delete: "t1_space X ⟷ (∀U x. openin X U ∧ x ∈ U ⟶ openin X (U - {x}))" apply (rule iffI) apply (meson closedin_t1_singleton in_mono openin_diff openin_subset) by (simp add: closedin_def t1_space_closedin_singleton) lemma t1_space_openin_delete_alt: "t1_space X ⟷ (∀U x. openin X U ⟶ openin X (U - {x}))" by (metis Diff_empty Diff_insert0 t1_space_openin_delete) lemma t1_space_singleton_Inter_open: "t1_space X ⟷ (∀x ∈ topspace X. ⋂{U. openin X U ∧ x ∈ U} = {x})" (is "?P=?Q") and t1_space_Inter_open_supersets: "t1_space X ⟷ (∀S. S ⊆ topspace X ⟶ ⋂{U. openin X U ∧ S ⊆ U} = S)" (is "?P=?R") proof - have "?R ⟹ ?Q" apply clarify apply (drule_tac x="{x}" in spec, simp) done moreover have "?Q ⟹ ?P" apply (clarsimp simp add: t1_space_def) apply (drule_tac x=x in bspec) apply (simp_all add: set_eq_iff) by (metis (no_types, lifting)) moreover have "?P ⟹ ?R" proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym) fix S assume S: "∀x∈topspace X. closedin X {x}" "S ⊆ topspace X" then show "⋂ {U. openin X U ∧ S ⊆ U} ⊆ S" apply clarsimp by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert) qed force ultimately show "?P=?Q" "?P=?R" by auto qed lemma t1_space_derived_set_of_infinite_openin: "t1_space X ⟷ (∀S. X derived_set_of S = {x ∈ topspace X. ∀U. x ∈ U ∧ openin X U ⟶ infinite(S ∩ U)})" (is "_ = ?rhs") proof assume "t1_space X" show ?rhs proof safe fix S x U assume "x ∈ X derived_set_of S" "x ∈ U" "openin X U" "finite (S ∩ U)" with ‹t1_space X› show "False" apply (simp add: t1_space_derived_set_of_finite) by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym) next fix S x have eq: "(∃y. (y ≠ x) ∧ y ∈ S ∧ y ∈ T) ⟷ ~((S ∩ T) ⊆ {x})" for x S T by blast assume "x ∈ topspace X" "∀U. x ∈ U ∧ openin X U ⟶ infinite (S ∩ U)" then show "x ∈ X derived_set_of S" apply (clarsimp simp add: derived_set_of_def eq) by (meson finite.emptyI finite.insertI finite_subset) qed (auto simp: in_derived_set_of) qed (auto simp: t1_space_derived_set_of_singleton) lemma finite_t1_space_imp_discrete_topology: "⟦topspace X = U; finite U; t1_space X⟧ ⟹ X = discrete_topology U" by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite) lemma t1_space_subtopology: "t1_space X ⟹ t1_space(subtopology X U)" by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite) lemma closedin_derived_set_of_gen: "t1_space X ⟹ closedin X (X derived_set_of S)" apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace) by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete) lemma derived_set_of_derived_set_subset_gen: "t1_space X ⟹ X derived_set_of (X derived_set_of S) ⊆ X derived_set_of S" by (meson closedin_contains_derived_set closedin_derived_set_of_gen) lemma subtopology_eq_discrete_topology_gen_finite: "⟦t1_space X; finite S⟧ ⟹ subtopology X S = discrete_topology(topspace X ∩ S)" by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite) lemma subtopology_eq_discrete_topology_finite: "⟦t1_space X; S ⊆ topspace X; finite S⟧ ⟹ subtopology X S = discrete_topology S" by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite) lemma t1_space_closed_map_image: "⟦closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X⟧ ⟹ t1_space Y" by (metis closed_map_def finite_subset_image t1_space_closedin_finite) lemma homeomorphic_t1_space: "X homeomorphic_space Y ⟹ (t1_space X ⟷ t1_space Y)" apply (clarsimp simp add: homeomorphic_space_def) by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image) proposition t1_space_product_topology: "t1_space (product_topology X I) ⟷ (product_topology X I) = trivial_topology ∨ (∀i ∈ I. t1_space (X i))" proof (cases "(product_topology X I) = trivial_topology") case True then show ?thesis using True t1_space_empty by force next case False then obtain f where f: "f ∈ (Π⇩_{E}i∈I. topspace(X i))" using discrete_topology_unique by (fastforce iff: null_topspace_iff_trivial) have "t1_space (product_topology X I) ⟷ (∀i∈I. t1_space (X i))" proof (intro iffI ballI) show "t1_space (X i)" if "t1_space (product_topology X I)" and "i ∈ I" for i proof - have clo: "⋀h. h ∈ (Π⇩_{E}i∈I. topspace (X i)) ⟹ closedin (product_topology X I) {h}" using that by (simp add: t1_space_closedin_singleton) show ?thesis unfolding t1_space_closedin_singleton proof clarify show "closedin (X i) {xi}" if "xi ∈ topspace (X i)" for xi using clo [of "λj ∈ I. if i=j then xi else f j"] f that ‹i ∈ I› by (fastforce simp add: closedin_product_topology_singleton) qed qed next next show "t1_space (product_topology X I)" if "∀i∈I. t1_space (X i)" using that by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton) qed then show ?thesis using False by blast qed lemma t1_space_prod_topology: "t1_space(prod_topology X Y) ⟷ (prod_topology X Y) = trivial_topology ∨ t1_space X ∧ t1_space Y" proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis by auto next case False have eq: "{(x,y)} = {x} × {y}" for x::'a and y::'b by simp have "t1_space (prod_topology X Y) ⟷ (t1_space X ∧ t1_space Y)" using False apply(simp add: t1_space_closedin_singleton closedin_prod_Times_iff eq del: insert_Times_insert flip: null_topspace_iff_trivial ex_in_conv) by blast with False show ?thesis by simp qed subsection‹Hausdorff Spaces› definition Hausdorff_space where "Hausdorff_space X ≡ ∀x y. x ∈ topspace X ∧ y ∈ topspace X ∧ (x ≠ y) ⟶ (∃U V. openin X U ∧ openin X V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V)" lemma Hausdorff_space_expansive: "⟦Hausdorff_space X; topspace X = topspace Y; ⋀U. openin X U ⟹ openin Y U⟧ ⟹ Hausdorff_space Y" by (metis Hausdorff_space_def) lemma Hausdorff_space_topspace_empty [iff]: "Hausdorff_space trivial_topology" by (simp add: Hausdorff_space_def) lemma Hausdorff_imp_t1_space: "Hausdorff_space X ⟹ t1_space X" by (metis Hausdorff_space_def disjnt_iff t1_space_def) lemma closedin_derived_set_of: "Hausdorff_space X ⟹ closedin X (X derived_set_of S)" by (simp add: Hausdorff_imp_t1_space closedin_derived_set_of_gen) lemma t1_or_Hausdorff_space: "t1_space X ∨ Hausdorff_space X ⟷ t1_space X" using Hausdorff_imp_t1_space by blast lemma Hausdorff_space_sing_Inter_opens: "⟦Hausdorff_space X; a ∈ topspace X⟧ ⟹ ⋂{u. openin X u ∧ a ∈ u} = {a}" using Hausdorff_imp_t1_space t1_space_singleton_Inter_open by force lemma Hausdorff_space_subtopology: assumes "Hausdorff_space X" shows "Hausdorff_space(subtopology X S)" proof - have *: "disjnt U V ⟹ disjnt (S ∩ U) (S ∩ V)" for U V by (simp add: disjnt_iff) from assms show ?thesis apply (simp add: Hausdorff_space_def openin_subtopology_alt) apply (fast intro: * elim!: all_forward) done qed lemma Hausdorff_space_compact_separation: assumes X: "Hausdorff_space X" and S: "compactin X S" and T: "compactin X T" and "disjnt S T" obtains U V where "openin X U" "openin X V" "S ⊆ U" "T ⊆ V" "disjnt U V" proof (cases "S = {}") case True then show thesis by (metis ‹compactin X T› compactin_subset_topspace disjnt_empty1 empty_subsetI openin_empty openin_topspace that) next case False have "∀x ∈ S. ∃U V. openin X U ∧ openin X V ∧ x ∈ U ∧ T ⊆ V ∧ disjnt U V" proof fix a assume "a ∈ S" then have "a ∉ T" by (meson assms(4) disjnt_iff) have a: "a ∈ topspace X" using S ‹a ∈ S› compactin_subset_topspace by blast show "∃U V. openin X U ∧ openin X V ∧ a ∈ U ∧ T ⊆ V ∧ disjnt U V" proof (cases "T = {}") case True then show ?thesis using a disjnt_empty2 openin_empty by blast next case False have "∀x ∈ topspace X - {a}. ∃U V. openin X U ∧ openin X V ∧ x ∈ U ∧ a ∈ V ∧ disjnt U V" using X a by (simp add: Hausdorff_space_def) then obtain U V where UV: "∀x ∈ topspace X - {a}. openin X (U x) ∧ openin X (V x) ∧ x ∈ U x ∧ a ∈ V x ∧ disjnt (U x) (V x)" by metis with ‹a ∉ T› compactin_subset_topspace [OF T] have Topen: "∀W ∈ U ` T. openin X W" and Tsub: "T ⊆ ⋃ (U ` T)" by auto then obtain ℱ where ℱ: "finite ℱ" "ℱ ⊆ U ` T" and "T ⊆ ⋃ℱ" using T unfolding compactin_def by meson then obtain F where F: "finite F" "F ⊆ T" "ℱ = U ` F" and SUF: "T ⊆ ⋃(U ` F)" and "a ∉ F" using finite_subset_image [OF ℱ] ‹a ∉ T› by (metis subsetD) have U: "⋀x. ⟦x ∈ topspace X; x ≠ a⟧ ⟹ openin X (U x)" and V: "⋀x. ⟦x ∈ topspace X; x ≠ a⟧ ⟹ openin X (V x)" and disj: "⋀x. ⟦x ∈ topspace X; x ≠ a⟧ ⟹ disjnt (U x) (V x)" using UV by blast+ show ?thesis proof (intro exI conjI) have "F ≠ {}" using False SUF by blast with ‹a ∉ F› show "openin X (⋂(V ` F))" using F compactin_subset_topspace [OF T] by (force intro: V) show "openin X (⋃(U ` F))" using F Topen Tsub by (force intro: U) show "disjnt (⋂(V ` F)) (⋃(U ` F))" using disj apply (auto simp: disjnt_def) using ‹F ⊆ T› ‹a ∉ F› compactin_subset_topspace [OF T] by blast show "a ∈ (⋂(V ` F))" using ‹F ⊆ T› T UV ‹a ∉ T› compactin_subset_topspace by blast qed (auto simp: SUF) qed qed then obtain U V where UV: "∀x ∈ S. openin X (U x) ∧ openin X (V x) ∧ x ∈ U x ∧ T ⊆ V x ∧ disjnt (U x) (V x)" by metis then have "S ⊆ ⋃ (U ` S)" by auto moreover have "∀W ∈ U ` S. openin X W" using UV by blast ultimately obtain I where I: "S ⊆ ⋃ (U ` I)" "I ⊆ S" "finite I" by (metis S compactin_def finite_subset_image) show thesis proof show "openin X (⋃(U ` I))" using ‹I ⊆ S› UV by blast show "openin X (⋂ (V ` I))" using False UV ‹I ⊆ S› ‹S ⊆ ⋃ (U ` I)› ‹finite I› by blast show "disjnt (⋃(U ` I)) (⋂ (V ` I))" by simp (meson UV ‹I ⊆ S› disjnt_subset2 in_mono le_INF_iff order_refl) qed (use UV I in auto) qed lemma Hausdorff_space_compact_sets: "Hausdorff_space X ⟷ (∀S T. compactin X S ∧ compactin X T ∧ disjnt S T ⟶ (∃U V. openin X U ∧ openin X V ∧ S ⊆ U ∧ T ⊆ V ∧ disjnt U V))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (meson Hausdorff_space_compact_separation) next assume R [rule_format]: ?rhs show ?lhs proof (clarsimp simp add: Hausdorff_space_def) fix x y assume "x ∈ topspace X" "y ∈ topspace X" "x ≠ y" then show "∃U. openin X U ∧ (∃V. openin X V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V)" using R [of "{x}" "{y}"] by auto qed qed lemma compactin_imp_closedin: assumes X: "Hausdorff_space X" and S: "compactin X S" shows "closedin X S" proof - have "S ⊆ topspace X" by (simp add: assms compactin_subset_topspace) moreover have "∃T. openin X T ∧ x ∈ T ∧ T ⊆ topspace X - S" if "x ∈ topspace X" "x ∉ S" for x using Hausdorff_space_compact_separation [OF X _ S, of "{x}"] that apply (simp add: disjnt_def) by (metis Diff_mono Diff_triv openin_subset) ultimately show ?thesis using closedin_def openin_subopen by force qed lemma closedin_Hausdorff_singleton: "⟦Hausdorff_space X; x ∈ topspace X⟧ ⟹ closedin X {x}" by (simp add: Hausdorff_imp_t1_space closedin_t1_singleton) lemma closedin_Hausdorff_sing_eq: "Hausdorff_space X ⟹ closedin X {x} ⟷ x ∈ topspace X" by (meson closedin_Hausdorff_singleton closedin_subset insert_subset) lemma Hausdorff_space_discrete_topology [simp]: "Hausdorff_space (discrete_topology U)" unfolding Hausdorff_space_def by (metis Hausdorff_space_compact_sets Hausdorff_space_def compactin_discrete_topology equalityE openin_discrete_topology) lemma compactin_Int: "⟦Hausdorff_space X; compactin X S; compactin X T⟧ ⟹ compactin X (S ∩ T)" by (simp add: closed_Int_compactin compactin_imp_closedin) lemma finite_topspace_imp_discrete_topology: "⟦topspace X = U; finite U; Hausdorff_space X⟧ ⟹ X = discrete_topology U" using Hausdorff_imp_t1_space finite_t1_space_imp_discrete_topology by blast lemma derived_set_of_finite: "⟦Hausdorff_space X; finite S⟧ ⟹ X derived_set_of S = {}" using Hausdorff_imp_t1_space t1_space_derived_set_of_finite by auto lemma infinite_perfect_set: "⟦Hausdorff_space X; S ⊆ X derived_set_of S; S ≠ {}⟧ ⟹ infinite S" using derived_set_of_finite by blast lemma derived_set_of_singleton: "Hausdorff_space X ⟹ X derived_set_of {x} = {}" by (simp add: derived_set_of_finite) lemma closedin_Hausdorff_finite: "⟦Hausdorff_space X; S ⊆ topspace X; finite S⟧ ⟹ closedin X S" by (simp add: compactin_imp_closedin finite_imp_compactin_eq) lemma open_in_Hausdorff_delete: "⟦Hausdorff_space X; openin X S⟧ ⟹ openin X (S - {x})" using Hausdorff_imp_t1_space t1_space_openin_delete_alt by auto lemma closedin_Hausdorff_finite_eq: "⟦Hausdorff_space X; finite S⟧ ⟹ closedin X S ⟷ S ⊆ topspace X" by (meson closedin_Hausdorff_finite closedin_def) lemma derived_set_of_infinite_openin: "Hausdorff_space X ⟹ X derived_set_of S = {x ∈ topspace X. ∀U. x ∈ U ∧ openin X U ⟶ infinite(S ∩ U)}" using Hausdorff_imp_t1_space t1_space_derived_set_of_infinite_openin by fastforce lemma Hausdorff_space_discrete_compactin: "Hausdorff_space X ⟹ S ∩ X derived_set_of S = {} ∧ compactin X S ⟷ S ⊆ topspace X ∧ finite S" using derived_set_of_finite discrete_compactin_eq_finite by fastforce lemma Hausdorff_space_finite_topspace: "Hausdorff_space X ⟹ X derived_set_of (topspace X) = {} ∧ compact_space X ⟷ finite(topspace X)" using derived_set_of_finite discrete_compact_space_eq_finite by auto lemma derived_set_of_derived_set_subset: "Hausdorff_space X ⟹ X derived_set_of (X derived_set_of S) ⊆ X derived_set_of S" by (simp add: Hausdorff_imp_t1_space derived_set_of_derived_set_subset_gen) lemma Hausdorff_space_injective_preimage: assumes "Hausdorff_space Y" and cmf: "continuous_map X Y f" and "inj_on f (topspace X)" shows "Hausdorff_space X" unfolding Hausdorff_space_def proof clarify fix x y assume x: "x ∈ topspace X" and y: "y ∈ topspace X" and "x ≠ y" then obtain U V where "openin Y U" "openin Y V" "f x ∈ U" "f y ∈ V" "disjnt U V" using assms by (smt (verit, ccfv_threshold) Hausdorff_space_def continuous_map image_subset_iff inj_on_def) show "∃U V. openin X U ∧ openin X V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V" proof (intro exI conjI) show "openin X {x ∈ topspace X. f x ∈ U}" using ‹openin Y U› cmf continuous_map by fastforce show "openin X {x ∈ topspace X. f x ∈ V}" using ‹openin Y V› cmf openin_continuous_map_preimage by blast show "disjnt {x ∈ topspace X. f x ∈ U} {x ∈ topspace X. f x ∈ V}" using ‹disjnt U V› by (auto simp add: disjnt_def) qed (use x ‹f x ∈ U› y ‹f y ∈ V› in auto) qed lemma homeomorphic_Hausdorff_space: "X homeomorphic_space Y ⟹ Hausdorff_space X ⟷ Hausdorff_space Y" unfolding homeomorphic_space_def homeomorphic_maps_map by (auto simp: homeomorphic_eq_everything_map Hausdorff_space_injective_preimage) lemma Hausdorff_space_retraction_map_image: "⟦retraction_map X Y r; Hausdorff_space X⟧ ⟹ Hausdorff_space Y" unfolding retraction_map_def using Hausdorff_space_subtopology homeomorphic_Hausdorff_space retraction_maps_section_image2 by blast lemma compact_Hausdorff_space_optimal: assumes eq: "topspace Y = topspace X" and XY: "⋀U. openin X U ⟹ openin Y U" and "Hausdorff_space X" "compact_space Y" shows "Y = X" proof - have "⋀U. closedin X U ⟹ closedin Y U" using XY using topology_finer_closedin [OF eq] by metis have "openin Y S = openin X S" for S by (metis XY assms(3) assms(4) closedin_compact_space compactin_contractive compactin_imp_closedin eq openin_closedin_eq) then show ?thesis by (simp add: topology_eq) qed lemma continuous_map_imp_closed_graph: assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y" shows "closedin (prod_topology X Y) ((λx. (x,f x)) ` topspace X)" unfolding closedin_def proof show "(λx. (x, f x)) ` topspace X ⊆ topspace (prod_topology X Y)" using continuous_map_def f by fastforce show "openin (prod_topology X Y) (topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X)" unfolding openin_prod_topology_alt proof (intro allI impI) show "∃U V. openin X U ∧ openin Y V ∧ x ∈ U ∧ y ∈ V ∧ U × V ⊆ topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X" if "(x,y) ∈ topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X" for x y proof - have "x ∈ topspace X" and y: "y ∈ topspace Y" "y ≠ f x" using that by auto then have "f x ∈ topspace Y" using continuous_map_image_subset_topspace f by blast then obtain U V where UV: "openin Y U" "openin Y V" "f x ∈ U" "y ∈ V" "disjnt U V" using Y y Hausdorff_space_def by metis show ?thesis proof (intro exI conjI) show "openin X {x ∈ topspace X. f x ∈ U}" using ‹openin Y U› f openin_continuous_map_preimage by blast show "{x ∈ topspace X. f x ∈ U} × V ⊆ topspace (prod_topology X Y) - (λx. (x, f x)) ` topspace X" using UV by (auto simp: disjnt_iff dest: openin_subset) qed (use UV ‹x ∈ topspace X› in auto) qed qed qed lemma continuous_imp_closed_map: "⟦continuous_map X Y f; compact_space X; Hausdorff_space Y⟧ ⟹ closed_map X Y f" by (meson closed_map_def closedin_compact_space compactin_imp_closedin image_compactin) lemma continuous_imp_quotient_map: "⟦continuous_map X Y f; compact_space X; Hausdorff_space Y; f ` (topspace X) = topspace Y⟧ ⟹ quotient_map X Y f" by (simp add: continuous_imp_closed_map continuous_closed_imp_quotient_map) lemma continuous_imp_homeomorphic_map: "⟦continuous_map X Y f; compact_space X; Hausdorff_space Y; f ` (topspace X) = topspace Y; inj_on f (topspace X)⟧ ⟹ homeomorphic_map X Y f" by (simp add: continuous_imp_closed_map bijective_closed_imp_homeomorphic_map) lemma continuous_imp_embedding_map: "⟦continuous_map X Y f; compact_space X; Hausdorff_space Y; inj_on f (topspace X)⟧ ⟹ embedding_map X Y f" by (simp add: continuous_imp_closed_map injective_closed_imp_embedding_map) lemma continuous_inverse_map: assumes "compact_space X" "Hausdorff_space Y" and cmf: "continuous_map X Y f" and gf: "⋀x. x ∈ topspace X ⟹ g(f x) = x" and Sf: "S ⊆ f ` (topspace X)" shows "continuous_map (subtopology Y S) X g" proof (rule continuous_map_from_subtopology_mono [OF _ ‹S ⊆ f ` (topspace X)›]) show "continuous_map (subtopology Y (f ` (topspace X))) X g" unfolding continuous_map_closedin proof (intro conjI ballI allI impI) show "g ∈ topspace (subtopology Y (f ` topspace X)) → topspace X" using gf by auto next fix C assume C: "closedin X C" show "closedin (subtopology Y (f ` topspace X)) {x ∈ topspace (subtopology Y (f ` topspace X)). g x ∈ C}" proof (rule compactin_imp_closedin) show "Hausdorff_space (subtopology Y (f ` topspace X))" using Hausdorff_space_subtopology [OF ‹Hausdorff_space Y›] by blast have "compactin Y (f ` C)" using C cmf image_compactin closedin_compact_space [OF ‹compact_space X›] by blast moreover have "{x ∈ topspace Y. x ∈ f ` topspace X ∧ g x ∈ C} = f ` C" using closedin_subset [OF C] cmf by (auto simp: gf continuous_map_def) ultimately have "compactin Y {x ∈ topspace Y. x ∈ f ` topspace X ∧ g x ∈ C}" by simp then show "compactin (subtopology Y (f ` topspace X)) {x ∈ topspace (subtopology Y (f ` topspace X)). g x ∈ C}" by (auto simp add: compactin_subtopology) qed qed qed lemma closed_map_paired_continuous_map_right: "⟦continuous_map X Y f; Hausdorff_space Y⟧ ⟹ closed_map X (prod_topology X Y) (λx. (x,f x))" by (simp add: continuous_map_imp_closed_graph embedding_map_graph embedding_imp_closed_map) lemma closed_map_paired_continuous_map_left: assumes f: "continuous_map X Y f" and Y: "Hausdorff_space Y" shows "closed_map X (prod_topology Y X) (λx. (f x,x))" proof - have eq: "(λx. (f x,x)) = (λ(a,b). (b,a)) ∘ (λx. (x,f x))" by auto show ?thesis unfolding eq proof (rule closed_map_compose) show "closed_map X (prod_topology X Y) (λx. (x, f x))" using Y closed_map_paired_continuous_map_right f by blast show "closed_map (prod_topology X Y) (prod_topology Y X) (λ(a, b). (b, a))" by (metis homeomorphic_map_swap homeomorphic_imp_closed_map) qed qed lemma proper_map_paired_continuous_map_right: "⟦continuous_map X Y f; Hausdorff_space Y⟧ ⟹ proper_map X (prod_topology X Y) (λx. (x,f x))" using closed_injective_imp_proper_map closed_map_paired_continuous_map_right by (metis (mono_tags, lifting) Pair_inject inj_onI) lemma proper_map_paired_continuous_map_left: "⟦continuous_map X Y f; Hausdorff_space Y⟧ ⟹ proper_map X (prod_topology Y X) (λx. (f x,x))" using closed_injective_imp_proper_map closed_map_paired_continuous_map_left by (metis (mono_tags, lifting) Pair_inject inj_onI) lemma Hausdorff_space_prod_topology: "Hausdorff_space(prod_topology X Y) ⟷ (prod_topology X Y) = trivial_topology ∨ Hausdorff_space X ∧ Hausdorff_space Y" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (rule topological_property_of_prod_component) (auto simp: Hausdorff_space_subtopology homeomorphic_Hausdorff_space) next assume R: ?rhs show ?lhs proof (cases "(topspace X × topspace Y) = {}") case False with R have ne: "topspace X ≠ {}" "topspace Y ≠ {}" and X: "Hausdorff_space X" and Y: "Hausdorff_space Y" by auto show ?thesis unfolding Hausdorff_space_def proof clarify fix x y x' y' assume xy: "(x, y) ∈ topspace (prod_topology X Y)" and xy': "(x',y') ∈ topspace (prod_topology X Y)" and *: "∄U V. openin (prod_topology X Y) U ∧ openin (prod_topology X Y) V ∧ (x, y) ∈ U ∧ (x', y') ∈ V ∧ disjnt U V" have False if "x ≠ x' ∨ y ≠ y'" using that proof assume "x ≠ x'" then obtain U V where "openin X U" "openin X V" "x ∈ U" "x' ∈ V" "disjnt U V" by (metis Hausdorff_space_def X mem_Sigma_iff topspace_prod_topology xy xy') let ?U = "U × topspace Y" let ?V = "V × topspace Y" have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V" by (simp_all add: openin_prod_Times_iff ‹openin X U› ‹openin X V›) moreover have "disjnt ?U ?V" by (simp add: ‹disjnt U V›) ultimately show False using * ‹x ∈ U› ‹x' ∈ V› xy xy' by (metis SigmaD2 SigmaI topspace_prod_topology) next assume "y ≠ y'" then obtain U V where "openin Y U" "openin Y V" "y ∈ U" "y' ∈ V" "disjnt U V" by (metis Hausdorff_space_def Y mem_Sigma_iff topspace_prod_topology xy xy') let ?U = "topspace X × U" let ?V = "topspace X × V" have "openin (prod_topology X Y) ?U" "openin (prod_topology X Y) ?V" by (simp_all add: openin_prod_Times_iff ‹openin Y U› ‹openin Y V›) moreover have "disjnt ?U ?V" by (simp add: ‹disjnt U V›) ultimately show False using "*" ‹y ∈ U› ‹y' ∈ V› xy xy' by (metis SigmaD1 SigmaI topspace_prod_topology) qed then show "x = x' ∧ y = y'" by blast qed qed force qed lemma Hausdorff_space_product_topology: "Hausdorff_space (product_topology X I) ⟷ (Π⇩_{E}i∈I. topspace(X i)) = {} ∨ (∀i ∈ I. Hausdorff_space (X i))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (simp add: Hausdorff_space_subtopology PiE_eq_empty_iff homeomorphic_Hausdorff_space topological_property_of_product_component) next assume R: ?rhs show ?lhs proof (cases "(Π⇩_{E}i∈I. topspace(X i)) = {}") case True then show ?thesis by (simp add: Hausdorff_space_def) next case False have "∃U V. openin (product_topology X I) U ∧ openin (product_topology X I) V ∧ f ∈ U ∧ g ∈ V ∧ disjnt U V" if f: "f ∈ (Π⇩_{E}i∈I. topspace (X i))" and g: "g ∈ (Π⇩_{E}i∈I. topspace (X i))" and "f ≠ g" for f g :: "'a ⇒ 'b" proof - obtain m where "f m ≠ g m" using ‹f ≠ g› by blast then have "m ∈ I" using f g by fastforce then have "Hausdorff_space (X m)" using False that R by blast then obtain U V where U: "openin (X m) U" and V: "openin (X m) V" and "f m ∈ U" "g m ∈ V" "disjnt U V" by (metis Hausdorff_space_def PiE_mem ‹f m ≠ g m› ‹m ∈ I› f g) show ?thesis proof (intro exI conjI) let ?U = "(Π⇩_{E}i∈I. topspace(X i)) ∩ {x. x m ∈ U}" let ?V = "(Π⇩_{E}i∈I. topspace(X i)) ∩ {x. x m ∈ V}" show "openin (product_topology X I) ?U" "openin (product_topology X I) ?V" using ‹m ∈ I› U V by (force simp add: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)+ show "f ∈ ?U" using ‹f m ∈ U› f by blast show "g ∈ ?V" using ‹g m ∈ V› g by blast show "disjnt ?U ?V" using ‹disjnt U V› by (auto simp: PiE_def Pi_def disjnt_def) qed qed then show ?thesis by (simp add: Hausdorff_space_def) qed qed lemma Hausdorff_space_closed_neighbourhood: "Hausdorff_space X ⟷ (∀x ∈ topspace X. ∃U C. openin X U ∧ closedin X C ∧ Hausdorff_space(subtopology X C) ∧ x ∈ U ∧ U ⊆ C)" (is "_ = ?rhs") proof assume R: ?rhs show "Hausdorff_space X" unfolding Hausdorff_space_def proof clarify fix x y assume x: "x ∈ topspace X" and y: "y ∈ topspace X" and "x ≠ y" obtain T C where *: "openin X T" "closedin X C" "x ∈ T" "T ⊆ C" and C: "Hausdorff_space (subtopology X C)" by (meson R ‹x ∈ topspace X›) show "∃U V. openin X U ∧ openin X V ∧ x ∈ U ∧ y ∈ V ∧ disjnt U V" proof (cases "y ∈ C") case True with * C obtain U V where U: "openin (subtopology X C) U" and V: "openin (subtopology X C) V" and "x ∈ U" "y ∈ V" "disjnt U V" unfolding Hausdorff_space_def by (smt (verit, best) ‹x ≠ y› closedin_subset subsetD topspace_subtopology_subset) then obtain U' V' where UV': "U = U' ∩ C" "openin X U'" "V = V' ∩ C" "openin X V'" by (meson openin_subtopology) have "disjnt (T ∩ U') V'" using ‹disjnt U V› UV' ‹T ⊆ C› by (force simp: disjnt_iff) with ‹T ⊆ C› have "disjnt (T ∩ U') (V' ∪ (topspace X - C))" unfolding disjnt_def by blast moreover have "openin X (T ∩ U')" by (simp add: ‹openin X T› ‹openin X U'› openin_Int) moreover have "openin X (V' ∪ (topspace X - C))" using ‹closedin X C› ‹openin X V'› by auto ultimately show ?thesis using UV' ‹x ∈ T› ‹x ∈ U› ‹y ∈ V› by blast next case False with * y show ?thesis by (force simp: closedin_def disjnt_def) qed qed qed fastforce end