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