--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/T1_Spaces.thy Thu Mar 07 14:08:05 2019 +0000
@@ -0,0 +1,201 @@
+section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
+
+theory T1_Spaces
+imports Function_Topology
+begin
+
+definition t1_space where
+ "t1_space X \<equiv> \<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> y \<notin> U)"
+
+lemma t1_space_expansive:
+ "\<lbrakk>topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> t1_space X \<Longrightarrow> t1_space Y"
+ by (metis t1_space_def)
+
+lemma t1_space_alt:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. closedin X U \<and> x \<in> U \<and> y \<notin> U))"
+ by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)
+
+lemma t1_space_empty: "topspace X = {} \<Longrightarrow> t1_space X"
+ by (simp add: t1_space_def)
+
+lemma t1_space_derived_set_of_singleton:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> 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 \<longleftrightarrow> (\<forall>S. finite S \<longrightarrow> X derived_set_of S = {})"
+proof (intro iffI allI impI)
+ fix S :: "'a set"
+ assume "finite S"
+ then have fin: "finite ((\<lambda>x. {x}) ` (topspace X \<inter> S))"
+ by blast
+ assume "t1_space X"
+ then have "X derived_set_of (\<Union>x \<in> topspace X \<inter> 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 \<inter> 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 \<longleftrightarrow> (\<forall>x \<in> 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 closedin_t1_singleton:
+ "\<lbrakk>t1_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {a}"
+ by (simp add: t1_space_closedin_singleton)
+
+lemma t1_space_closedin_finite:
+ "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<and> S \<subseteq> topspace X \<longrightarrow> 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 \<Longrightarrow> X closure_of {a} = (if a \<in> 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 \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
+ "separatedin X S {a} \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
+ unfolding separatedin_def
+ using assms closure_of closure_of_singleton by fastforce+
+
+lemma t1_space_openin_delete:
+ "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> 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 \<longleftrightarrow> (\<forall>U x. openin X U \<longrightarrow> openin X (U - {x}))"
+ by (metis Diff_empty Diff_insert0 t1_space_openin_delete)
+
+
+lemma t1_space_singleton_Inter_open:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<Inter>{U. openin X U \<and> x \<in> U} = {x})" (is "?P=?Q")
+ and t1_space_Inter_open_supersets:
+ "t1_space X \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> \<Inter>{U. openin X U \<and> S \<subseteq> U} = S)" (is "?P=?R")
+proof -
+ have "?R \<Longrightarrow> ?Q"
+ apply clarify
+ apply (drule_tac x="{x}" in spec, simp)
+ done
+ moreover have "?Q \<Longrightarrow> ?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 \<Longrightarrow> ?R"
+ proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
+ fix S
+ assume S: "\<forall>x\<in>topspace X. closedin X {x}" "S \<subseteq> topspace X"
+ then show "\<Inter> {U. openin X U \<and> S \<subseteq> U} \<subseteq> 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 \<longleftrightarrow>
+ (\<forall>S. X derived_set_of S =
+ {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)})"
+ (is "_ = ?rhs")
+proof
+ assume "t1_space X"
+ show ?rhs
+ proof safe
+ fix S x U
+ assume "x \<in> X derived_set_of S" "x \<in> U" "openin X U" "finite (S \<inter> U)"
+ with \<open>t1_space X\<close> 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: "(\<exists>y. (y \<noteq> x) \<and> y \<in> S \<and> y \<in> T) \<longleftrightarrow> ~((S \<inter> T) \<subseteq> {x})" for x S T
+ by blast
+ assume "x \<in> topspace X" "\<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite (S \<inter> U)"
+ then show "x \<in> 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:
+ "\<lbrakk>topspace X = U; finite U; t1_space X\<rbrakk> \<Longrightarrow> X = discrete_topology U"
+ by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)
+
+lemma t1_space_subtopology: "t1_space X \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> X derived_set_of (X derived_set_of S) \<subseteq> X derived_set_of S"
+ by (meson closedin_contains_derived_set closedin_derived_set_of_gen)
+
+lemma subtopology_eq_discrete_topology_gen_finite:
+ "\<lbrakk>t1_space X; finite S\<rbrakk> \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
+ by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)
+
+lemma subtopology_eq_discrete_topology_finite:
+ "\<lbrakk>t1_space X; S \<subseteq> topspace X; finite S\<rbrakk>
+ \<Longrightarrow> 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:
+ "\<lbrakk>closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X\<rbrakk> \<Longrightarrow> t1_space Y"
+ by (metis closed_map_def finite_subset_image t1_space_closedin_finite)
+
+lemma homeomorphic_t1_space: "X homeomorphic_space Y \<Longrightarrow> (t1_space X \<longleftrightarrow> 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)
+\<longleftrightarrow> topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t1_space (X i))"
+proof (cases "topspace(product_topology X I) = {}")
+ case True
+ then show ?thesis
+ using True t1_space_empty by blast
+next
+ case False
+ then obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
+ by fastforce
+ have "t1_space (product_topology X I) \<longleftrightarrow> (\<forall>i\<in>I. t1_space (X i))"
+ proof (intro iffI ballI)
+ show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \<in> I" for i
+ proof -
+ have clo: "\<And>h. h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<Longrightarrow> 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 \<in> topspace (X i)" for xi
+ using clo [of "\<lambda>j \<in> I. if i=j then xi else f j"] f that \<open>i \<in> I\<close>
+ by (fastforce simp add: closedin_product_topology_singleton)
+ qed
+ qed
+ next
+ next
+ show "t1_space (product_topology X I)" if "\<forall>i\<in>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
+
+end