Impressum Abstract_Topological_Spaces.thy Interaktion und
PortierbarkeitIsabelle

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

section \<open>Various Forms of Topological Spaces\<close>

theory Abstract_Topological_Spaces
 imports Lindelof_Spaces Locally Abstract_Euclidean_Space Sum_Topology FSigma
begin

subsection\<open>Connected topological spaces\<close>

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
 \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> S = {} \<or> 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 \<subseteq> topspace X \<and> (\<forall>S T. separatedin X S T \<and> C \<subseteq> S \<union> T \<longrightarrow> C \<subseteq> S \<or> C \<subseteq> 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\<open>The notion of "separated between" (complement of "connected between)"\<close>

definition separated_between
 where "separated_between X S T \
 \<exists>U V. openin X U \<and> openin X V \<and> U \<union> V = topspace X \<and> disjnt U V \<and> S \<subseteq> U \<and> T \<subseteq> V"

lemma separated_between_alt:
 "separated_between X S T \
 (\<exists>U V. closedin X U \<and> closedin X V \<and> U \<union> V = topspace X \<and> disjnt U V \<and> S \<subseteq> U \<and> T \<subseteq> 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 \
 (\<exists>U. closedin X U \<and> openin X U \<and> S \<subseteq> U \<and> T \<subseteq> 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 = {} \<longrightarrow> T \<subseteq> topspace X) \<and> (\<forall>x \<in> 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) \<open>K \<subseteq> S\<close> 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) \<open>finite K\<close> closedin_Union finite_imageI image_iff)
 show "openin X (\ (U ` K))"
 using U(1) \<open>K \<subseteq> S\<close> 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) \<open>K \<subseteq> S\<close> disjnt_iff subsetD)
 then show "T \ topspace X - \ (U ` K)"
 using \<open>T \<subseteq> topspace X\<close> by auto
 qed
 qed
qed

lemma separated_between_pointwise_right:
 "compactin X T
 \<Longrightarrow> separated_between X S T \<longleftrightarrow> (T = {} \<longrightarrow> S \<subseteq> topspace X) \<and> (\<forall>y \<in> 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 \<subseteq> topspace X \<and> disjnt S T \<and> 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\
 \<Longrightarrow> (separated_between X (X frontier_of S) T \<longleftrightarrow> separated_between X S T)"
 using separated_between_frontier_of_eq by blast

lemma separated_between_frontier_of':
"\T \ topspace X; disjnt S T\
 \<Longrightarrow> (separated_between X S (X frontier_of T) \<longleftrightarrow> 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
 \<Longrightarrow> (separated_between X S T \<longleftrightarrow> S = {} \<and> T \<subseteq> topspace X \<or> S \<subseteq> topspace X \<and> T = {})"
 by (metis connected_space_separated_between separated_between_empty)

subsection\<open>Connected components\<close>

lemma connected_component_of_subtopology_eq:
 "connected_component_of (subtopology X U) a = connected_component_of X a \
 connected_component_of_set X a \<subseteq> 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 \<open>a \<in> U\<close> \<open>a \<in> topspace X\<close> 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\
 \<Longrightarrow> 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\
 \<Longrightarrow> 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 \<times> 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 \<times> D |C D. C \<in> connected_components_of X \<and> D \<in> 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 \<in> extensional I then PiE I (\<lambda>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 = (\\<^sub>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 \<open>C \<subseteq> extensional I\<close> 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. \<forall>i \<in> I. B i \<in> 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\<^sub>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) \ ((\\<^sub>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 \<open>Monotone maps (in the general topological sense)\<close>

definition monotone_map
 where "monotone_map X Y f ==
 f ` (topspace X) \<subseteq> topspace Y \<and>
 (\<forall>y \<in> topspace Y. connectedin X {x \<in> topspace X. f x = y})"

lemma monotone_map:
 "monotone_map X Y f \
 f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>y. connectedin X {x \<in> 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
 \<Longrightarrow> 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: \<open>U \<noteq> {}\<close>)
 show "(f`V) \ {}"
 by (simp add: \<open>V \<noteq> {}\<close>)
 have *: "y \ f ` V" if "y \ f ` U" for y
 proof -
 have \<section>: "connectedin X {x \<in> topspace X. f x = y}"
 using f(1) monotone_map by fastforce
 show ?thesis
 using connectedinD [OF \<section> \<open>openin X U\<close> \<open>openin X V\<close>] UVsub topUV \<open>U \<inter> V = {}\<close> that
 by (force simp: disjoint_iff)
 qed
 then show "f`U \ f`V = {}"
 by blast
 show "openin Y (f`U)"
 using f \<open>openin X U\<close> topUV * unfolding quotient_map_saturated_open by force
 show "openin Y (f`V)"
 using f \<open>openin X V\<close> 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 \<open>connectedin Y C\<close> 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 \<open>monotone_map X Y f\<close> 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\<open>Other countability properties\<close>

definition second_countable
 where "second_countable X \
 \<exists>\. countable \ \<and> (\<forall>V \<in> \. openin X V) \<and>
 (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \. x \<in> V \<and> V \<subseteq> U))"

definition first_countable
 where "first_countable X \
 \<forall>x \<in> topspace X.
 \<exists>\. countable \ \<and> (\<forall>V \<in> \. openin X V) \<and>
 (\<forall>U. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V \<in> \. x \<in> V \<and> V \<subseteq> U))"

definition separable_space
 where "separable_space X \
 \<exists>C. countable C \<and> C \<subseteq> topspace X \<and> X closure_of C = topspace X"

lemma second_countable:
 "second_countable X \
 (\<exists>\. countable \ \<and> openin X = arbitrary union_of (\<lambda>x. x \<in> \))"
 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 \" "\<And>V. V \<in> \ \<Longrightarrow> 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 \" "\<And>V. V \<in> \ \<Longrightarrow> V \<subseteq> 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 \<open>countable \\<close> 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 \" "\<And>V. V \<in> \ \<Longrightarrow> 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 \: "\<And>V. V \<in> \ \<Longrightarrow> 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 \<open>countable \\<close> 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 \<open>x \<in> U\<close> 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 \<open>y \<in> topspace Y\<close> fim imageE)
 obtain \ where \: "countable \" "\<And>V. V \<in> \ \<Longrightarrow> 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 \ \
 (\<forall>V\<in>\. openin Y V) \<and> (\<forall>U. openin Y U \<and> y \<in> U \<longrightarrow> (\<exists>V\<in>\. y \<in> V \<and> V \<subseteq> 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\
 \<Longrightarrow> \<exists>y. y \<in> S \<and> y \<in> C \<and> y \<in> T"
 by (smt (verit) \<open>openin X S\<close> in_closure_of openin_open_subtopology subsetD)
 with C \<open>openin X S\<close> 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 \" "\<And>V. V \<in> \ \<Longrightarrow> 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 \" "\<And>V. V \<in> \ \<Longrightarrow> 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 \<in> \. \<exists>U. U \<in> \ \<and> B \<subseteq> U}"
 have \': "countable \'" "\<Union>\' = \<Union>\"
 using \ using "*" \<open>\<forall>U\<in>\. openin X U\<close> 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 "\<exists>\<V>. countable \<V> \<and> \<V> \<subseteq> \ \<and> \<Union>\<V> = topspace X"
 by (rule_tac x="G ` \'" in exI) fastforce
qed

subsection \<open>Neigbourhood bases EXTRAS\<close>

text \<open>Neigbourhood bases: useful for "local" properties of various kinds\<close>

lemma openin_topology_neighbourhood_base_unique:
 "openin X = arbitrary union_of P \
 (\<forall>u. P u \<longrightarrow> openin X u) \<and> 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
 \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow>
 (\<forall>w. b w \<and> x \<in> w \<longrightarrow> (\<exists>u v. openin X u \<and> P v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> 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 \
 (\<forall>x \<in> topspace X. \<exists>u v. openin X u \<and> P v \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> 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 \
 (\<exists>\. countable \ \<and> (\<forall>V \<in> \. openin X V) \<and> neighbourhood_base_of (\<lambda>A. A\<in>\) X)"
 by (metis (full_types) openin_topology_neighbourhood_base_unique second_countable)

lemma first_countable_neighbourhood_base_alt:
 "first_countable X \
 (\<forall>x \<in> topspace X. \<exists>\. countable \ \<and> (\<forall>V \<in> \. openin X V) \<and> neighbourhood_base_at x (\<lambda>V. V \<in> \) 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 \
 (\<exists>\. countable \ \<and> neighbourhood_base_of (\<lambda>V. V \<in> \) 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 \: "\<And>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. openin X U \<and> (\<exists>V. V \<in> \ \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> 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 \
 (\<forall>x \<in> topspace X. \<exists>\. countable \ \<and> neighbourhood_base_at x (\<lambda>V. V \<in> \) 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 (\<lambda>V. V \<in> \) 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\<open>$T_0$ spaces and the Kolmogorov quotient\<close>

definition t0_space where
 "t0_space X \
 \<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x \<noteq> y \<longrightarrow> (\<exists>U. openin X U \<and> (x \<notin> U \<longleftrightarrow> y \<in> 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 \<and>
 (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x \<in> X closure_of {y} \<longleftrightarrow> y \<in> 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 \
 (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x \<noteq> y \<longrightarrow> (\<exists>C. closedin X C \<and> (x \<notin> C \<longleftrightarrow> y \<in> 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 \
 (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. X closure_of {x} = X closure_of {y} \<longrightarrow> 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 \<open>i \<in> I\<close> \<open>x i \<noteq> y i\<close> topspace_product_topology x y)
 with \<open>i \<in> I\<close> x y show "\<exists>U. closedin (product_topology X I) U \<and> (x \<notin> U) = (y \<in> 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 \<open>Kolmogorov quotients\<close>

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 \<open>openin X U\<close> 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 \
 (\<forall>U. openin X U \<longrightarrow> (x \<in> U \<longleftrightarrow> y \<in> 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 \
 (\<forall>U. closedin X U \<longrightarrow> (x \<in> U \<longleftrightarrow> y \<in> 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\<open>Closed diagonals and graphs\<close>

lemma Hausdorff_space_closedin_diagonal:
 "Hausdorff_space X \ closedin (prod_topology X X) ((\x. (x,x)) ` topspace X)"
proof -
 have \<section>: "((\<lambda>x. (x, x)) ` topspace X) \<subseteq> topspace X \<times> topspace X"
 by auto
 show ?thesis
 apply (simp add: closedin_def openin_prod_topology_alt Hausdorff_space_def disjnt_iff \<section>)
 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 \<section>:"{x \<in> topspace X. f x = g x} = {x \<in> topspace X. (f x,g x) \<in> ((\<lambda>y.(y,y)) ` topspace Y)}"
 using f continuous_map_image_subset_topspace by fastforce
 show ?thesis
 unfolding \<section>
 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 \<section>: "S = {x \<in> topspace X. r x = x}"
 using S retract_of_space_imp_subset by (force simp: continuous_map_def Pi_iff)
 show ?thesis
 unfolding \<section>
 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)))
 (\<lambda>x. (x, f x)) fst \<longleftrightarrow> 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 \<open> KC spaces, those where all compact sets are closed.\<close>

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\
 \<Longrightarrow> 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

--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.24Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Impressum Abstract_Topological_Spaces.thy Interaktion und PortierbarkeitIsabelle

Haftungshinweis

Bemerkung:

Impressum Abstract_Topological_Spaces.thy Interaktion und
PortierbarkeitIsabelle