src/HOL/Analysis/T1_Spaces.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69939 812ce526da33
child 69986 f2d327275065
permissions -rw-r--r--
more strict AFP properties;
     1 section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
     2 
     3 theory T1_Spaces
     4 imports Product_Topology 
     5 begin
     6 
     7 definition t1_space where
     8  "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)"
     9 
    10 lemma t1_space_expansive:
    11    "\<lbrakk>topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> t1_space X \<Longrightarrow> t1_space Y"
    12   by (metis t1_space_def)
    13 
    14 lemma t1_space_alt:
    15    "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))"
    16  by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)
    17 
    18 lemma t1_space_empty: "topspace X = {} \<Longrightarrow> t1_space X"
    19   by (simp add: t1_space_def)
    20 
    21 lemma t1_space_derived_set_of_singleton:
    22   "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. X derived_set_of {x} = {})"
    23   apply (simp add: t1_space_def derived_set_of_def, safe)
    24    apply (metis openin_topspace)
    25   by force
    26 
    27 lemma t1_space_derived_set_of_finite:
    28    "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<longrightarrow> X derived_set_of S = {})"
    29 proof (intro iffI allI impI)
    30   fix S :: "'a set"
    31   assume "finite S"
    32   then have fin: "finite ((\<lambda>x. {x}) ` (topspace X \<inter> S))"
    33     by blast
    34   assume "t1_space X"
    35   then have "X derived_set_of (\<Union>x \<in> topspace X \<inter> S. {x}) = {}"
    36     unfolding derived_set_of_Union [OF fin]
    37     by (auto simp: t1_space_derived_set_of_singleton)
    38   then have "X derived_set_of (topspace X \<inter> S) = {}"
    39     by simp
    40   then show "X derived_set_of S = {}"
    41     by simp
    42 qed (auto simp: t1_space_derived_set_of_singleton)
    43 
    44 lemma t1_space_closedin_singleton:
    45    "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. closedin X {x})"
    46   apply (rule iffI)
    47   apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
    48   using t1_space_alt by auto
    49 
    50 lemma closedin_t1_singleton:
    51    "\<lbrakk>t1_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {a}"
    52   by (simp add: t1_space_closedin_singleton)
    53 
    54 lemma t1_space_closedin_finite:
    55    "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<and> S \<subseteq> topspace X \<longrightarrow> closedin X S)"
    56   apply (rule iffI)
    57   apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite)
    58   by (simp add: t1_space_closedin_singleton)
    59 
    60 lemma closure_of_singleton:
    61    "t1_space X \<Longrightarrow> X closure_of {a} = (if a \<in> topspace X then {a} else {})"
    62   by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen)
    63 
    64 lemma separated_in_singleton:
    65   assumes "t1_space X"
    66   shows "separatedin X {a} S \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
    67         "separatedin X S {a} \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
    68   unfolding separatedin_def
    69   using assms closure_of closure_of_singleton by fastforce+
    70 
    71 lemma t1_space_openin_delete:
    72    "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (U - {x}))"
    73   apply (rule iffI)
    74   apply (meson closedin_t1_singleton in_mono openin_diff openin_subset)
    75   by (simp add: closedin_def t1_space_closedin_singleton)
    76 
    77 lemma t1_space_openin_delete_alt:
    78    "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<longrightarrow> openin X (U - {x}))"
    79   by (metis Diff_empty Diff_insert0 t1_space_openin_delete)
    80 
    81 
    82 lemma t1_space_singleton_Inter_open:
    83       "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<Inter>{U. openin X U \<and> x \<in> U} = {x})"  (is "?P=?Q")
    84   and t1_space_Inter_open_supersets:
    85      "t1_space X \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> \<Inter>{U. openin X U \<and> S \<subseteq> U} = S)" (is "?P=?R")
    86 proof -
    87   have "?R \<Longrightarrow> ?Q"
    88     apply clarify
    89     apply (drule_tac x="{x}" in spec, simp)
    90     done
    91   moreover have "?Q \<Longrightarrow> ?P"
    92     apply (clarsimp simp add: t1_space_def)
    93     apply (drule_tac x=x in bspec)
    94      apply (simp_all add: set_eq_iff)
    95     by (metis (no_types, lifting))
    96   moreover have "?P \<Longrightarrow> ?R"
    97   proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
    98     fix S
    99     assume S: "\<forall>x\<in>topspace X. closedin X {x}" "S \<subseteq> topspace X"
   100     then show "\<Inter> {U. openin X U \<and> S \<subseteq> U} \<subseteq> S"
   101       apply clarsimp
   102       by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert)
   103   qed force
   104   ultimately show "?P=?Q" "?P=?R"
   105     by auto
   106 qed
   107 
   108 lemma t1_space_derived_set_of_infinite_openin:
   109    "t1_space X \<longleftrightarrow>
   110         (\<forall>S. X derived_set_of S =
   111              {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)})"
   112          (is "_ = ?rhs")
   113 proof
   114   assume "t1_space X"
   115   show ?rhs
   116   proof safe
   117     fix S x U
   118     assume "x \<in> X derived_set_of S" "x \<in> U" "openin X U" "finite (S \<inter> U)"
   119     with \<open>t1_space X\<close> show "False"
   120       apply (simp add: t1_space_derived_set_of_finite)
   121       by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym)
   122   next
   123     fix S x
   124     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
   125       by blast
   126     assume "x \<in> topspace X" "\<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite (S \<inter> U)"
   127     then show "x \<in> X derived_set_of S"
   128       apply (clarsimp simp add: derived_set_of_def eq)
   129       by (meson finite.emptyI finite.insertI finite_subset)
   130   qed (auto simp: in_derived_set_of)
   131 qed (auto simp: t1_space_derived_set_of_singleton)
   132 
   133 lemma finite_t1_space_imp_discrete_topology:
   134    "\<lbrakk>topspace X = U; finite U; t1_space X\<rbrakk> \<Longrightarrow> X = discrete_topology U"
   135   by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)
   136 
   137 lemma t1_space_subtopology: "t1_space X \<Longrightarrow> t1_space(subtopology X U)"
   138   by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite)
   139 
   140 lemma closedin_derived_set_of_gen:
   141    "t1_space X \<Longrightarrow> closedin X (X derived_set_of S)"
   142   apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace)
   143   by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete)
   144 
   145 lemma derived_set_of_derived_set_subset_gen:
   146    "t1_space X \<Longrightarrow> X derived_set_of (X derived_set_of S) \<subseteq> X derived_set_of S"
   147   by (meson closedin_contains_derived_set closedin_derived_set_of_gen)
   148 
   149 lemma subtopology_eq_discrete_topology_gen_finite:
   150    "\<lbrakk>t1_space X; finite S\<rbrakk> \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
   151   by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)
   152 
   153 lemma subtopology_eq_discrete_topology_finite:
   154    "\<lbrakk>t1_space X; S \<subseteq> topspace X; finite S\<rbrakk>
   155         \<Longrightarrow> subtopology X S = discrete_topology S"
   156   by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite)
   157 
   158 lemma t1_space_closed_map_image:
   159    "\<lbrakk>closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X\<rbrakk> \<Longrightarrow> t1_space Y"
   160   by (metis closed_map_def finite_subset_image t1_space_closedin_finite)
   161 
   162 lemma homeomorphic_t1_space: "X homeomorphic_space Y \<Longrightarrow> (t1_space X \<longleftrightarrow> t1_space Y)"
   163   apply (clarsimp simp add: homeomorphic_space_def)
   164   by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image)
   165 
   166 proposition t1_space_product_topology:
   167    "t1_space (product_topology X I)
   168 \<longleftrightarrow> topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t1_space (X i))"
   169 proof (cases "topspace(product_topology X I) = {}")
   170   case True
   171   then show ?thesis
   172     using True t1_space_empty by blast
   173 next
   174   case False
   175   then obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
   176     by fastforce
   177   have "t1_space (product_topology X I) \<longleftrightarrow> (\<forall>i\<in>I. t1_space (X i))"
   178   proof (intro iffI ballI)
   179     show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \<in> I" for i
   180     proof -
   181       have clo: "\<And>h. h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<Longrightarrow> closedin (product_topology X I) {h}"
   182         using that by (simp add: t1_space_closedin_singleton)
   183       show ?thesis
   184         unfolding t1_space_closedin_singleton
   185       proof clarify
   186         show "closedin (X i) {xi}" if "xi \<in> topspace (X i)" for xi
   187           using clo [of "\<lambda>j \<in> I. if i=j then xi else f j"] f that \<open>i \<in> I\<close>
   188           by (fastforce simp add: closedin_product_topology_singleton)
   189       qed
   190     qed
   191   next
   192   next
   193     show "t1_space (product_topology X I)" if "\<forall>i\<in>I. t1_space (X i)"
   194       using that
   195       by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton)
   196   qed
   197   then show ?thesis
   198     using False by blast
   199 qed
   200 
   201 lemma t1_space_prod_topology:
   202    "t1_space(prod_topology X Y) \<longleftrightarrow> topspace(prod_topology X Y) = {} \<or> t1_space X \<and> t1_space Y"
   203 proof (cases "topspace (prod_topology X Y) = {}")
   204   case True then show ?thesis
   205   by (auto simp: t1_space_empty)
   206 next
   207   case False
   208   have eq: "{(x,y)} = {x} \<times> {y}" for x y
   209     by simp
   210   have "t1_space (prod_topology X Y) \<longleftrightarrow> (t1_space X \<and> t1_space Y)"
   211     using False
   212     by (force simp: t1_space_closedin_singleton closedin_Times eq simp del: insert_Times_insert)
   213   with False show ?thesis
   214     by simp
   215 qed
   216 
   217 end