src/HOL/Analysis/Abstract_Topology.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69945 35ba13ac6e5c
child 69986 f2d327275065
permissions -rw-r--r--
more strict AFP properties;
lp15@69144
     1
(*  Author:     L C Paulson, University of Cambridge [ported from HOL Light]
lp15@69144
     2
*)
lp15@69144
     3
lp15@69144
     4
section \<open>Operators involving abstract topology\<close>
lp15@69144
     5
lp15@69144
     6
theory Abstract_Topology
immler@69544
     7
  imports
immler@69544
     8
    Complex_Main
immler@69544
     9
    "HOL-Library.Set_Idioms"
immler@69544
    10
    "HOL-Library.FuncSet"
lp15@69144
    11
begin
lp15@69144
    12
immler@69544
    13
subsection \<open>General notion of a topology as a value\<close>
immler@69544
    14
nipkow@69600
    15
definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
nipkow@69600
    16
"istopology L \<longleftrightarrow>
immler@69544
    17
  L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
immler@69544
    18
immler@69544
    19
typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
immler@69544
    20
  morphisms "openin" "topology"
immler@69544
    21
  unfolding istopology_def by blast
immler@69544
    22
immler@69544
    23
lemma istopology_openin[intro]: "istopology(openin U)"
immler@69544
    24
  using openin[of U] by blast
immler@69544
    25
lp15@69710
    26
lemma istopology_open: "istopology open"
lp15@69710
    27
  by (auto simp: istopology_def)
lp15@69710
    28
immler@69544
    29
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
immler@69544
    30
  using topology_inverse[unfolded mem_Collect_eq] .
immler@69544
    31
immler@69544
    32
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
immler@69544
    33
  using topology_inverse[of U] istopology_openin[of "topology U"] by auto
immler@69544
    34
immler@69544
    35
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
immler@69544
    36
proof
immler@69544
    37
  assume "T1 = T2"
immler@69544
    38
  then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
immler@69544
    39
next
immler@69544
    40
  assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
immler@69544
    41
  then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
immler@69544
    42
  then have "topology (openin T1) = topology (openin T2)" by simp
immler@69544
    43
  then show "T1 = T2" unfolding openin_inverse .
immler@69544
    44
qed
immler@69544
    45
immler@69544
    46
immler@69544
    47
text\<open>The "universe": the union of all sets in the topology.\<close>
immler@69544
    48
definition "topspace T = \<Union>{S. openin T S}"
immler@69544
    49
immler@69544
    50
subsubsection \<open>Main properties of open sets\<close>
immler@69544
    51
immler@69544
    52
proposition openin_clauses:
immler@69544
    53
  fixes U :: "'a topology"
immler@69544
    54
  shows
immler@69544
    55
    "openin U {}"
immler@69544
    56
    "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
immler@69544
    57
    "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
immler@69544
    58
  using openin[of U] unfolding istopology_def mem_Collect_eq by fast+
immler@69544
    59
immler@69544
    60
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
immler@69544
    61
  unfolding topspace_def by blast
immler@69544
    62
immler@69544
    63
lemma openin_empty[simp]: "openin U {}"
immler@69544
    64
  by (rule openin_clauses)
immler@69544
    65
immler@69544
    66
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
immler@69544
    67
  by (rule openin_clauses)
immler@69544
    68
immler@69544
    69
lemma openin_Union[intro]: "(\<And>S. S \<in> K \<Longrightarrow> openin U S) \<Longrightarrow> openin U (\<Union>K)"
immler@69544
    70
  using openin_clauses by blast
immler@69544
    71
immler@69544
    72
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
immler@69544
    73
  using openin_Union[of "{S,T}" U] by auto
immler@69544
    74
immler@69544
    75
lemma openin_topspace[intro, simp]: "openin U (topspace U)"
immler@69544
    76
  by (force simp: openin_Union topspace_def)
immler@69544
    77
immler@69544
    78
lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
immler@69544
    79
  (is "?lhs \<longleftrightarrow> ?rhs")
immler@69544
    80
proof
immler@69544
    81
  assume ?lhs
immler@69544
    82
  then show ?rhs by auto
immler@69544
    83
next
immler@69544
    84
  assume H: ?rhs
immler@69544
    85
  let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
immler@69544
    86
  have "openin U ?t" by (force simp: openin_Union)
immler@69544
    87
  also have "?t = S" using H by auto
immler@69544
    88
  finally show "openin U S" .
immler@69544
    89
qed
immler@69544
    90
immler@69544
    91
lemma openin_INT [intro]:
immler@69544
    92
  assumes "finite I"
immler@69544
    93
          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
immler@69544
    94
  shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
immler@69544
    95
using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)
immler@69544
    96
immler@69544
    97
lemma openin_INT2 [intro]:
immler@69544
    98
  assumes "finite I" "I \<noteq> {}"
immler@69544
    99
          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
immler@69544
   100
  shows "openin T (\<Inter>i \<in> I. U i)"
immler@69544
   101
proof -
immler@69544
   102
  have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
immler@69544
   103
    using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
immler@69544
   104
  then show ?thesis
immler@69544
   105
    using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
immler@69544
   106
qed
immler@69544
   107
immler@69544
   108
lemma openin_Inter [intro]:
immler@69544
   109
  assumes "finite \<F>" "\<F> \<noteq> {}" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (\<Inter>\<F>)"
immler@69544
   110
  by (metis (full_types) assms openin_INT2 image_ident)
immler@69544
   111
immler@69544
   112
lemma openin_Int_Inter:
immler@69544
   113
  assumes "finite \<F>" "openin T U" "\<And>X. X \<in> \<F> \<Longrightarrow> openin T X" shows "openin T (U \<inter> \<Inter>\<F>)"
immler@69544
   114
  using openin_Inter [of "insert U \<F>"] assms by auto
immler@69544
   115
immler@69544
   116
immler@69544
   117
subsubsection \<open>Closed sets\<close>
immler@69544
   118
nipkow@69600
   119
definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
nipkow@69600
   120
"closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
immler@69544
   121
immler@69544
   122
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
immler@69544
   123
  by (metis closedin_def)
immler@69544
   124
immler@69544
   125
lemma closedin_empty[simp]: "closedin U {}"
immler@69544
   126
  by (simp add: closedin_def)
immler@69544
   127
immler@69544
   128
lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
immler@69544
   129
  by (simp add: closedin_def)
immler@69544
   130
immler@69544
   131
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
immler@69544
   132
  by (auto simp: Diff_Un closedin_def)
immler@69544
   133
immler@69544
   134
lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
immler@69544
   135
  by auto
immler@69544
   136
immler@69544
   137
lemma closedin_Union:
immler@69544
   138
  assumes "finite S" "\<And>T. T \<in> S \<Longrightarrow> closedin U T"
immler@69544
   139
    shows "closedin U (\<Union>S)"
immler@69544
   140
  using assms by induction auto
immler@69544
   141
immler@69544
   142
lemma closedin_Inter[intro]:
immler@69544
   143
  assumes Ke: "K \<noteq> {}"
immler@69544
   144
    and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
immler@69544
   145
  shows "closedin U (\<Inter>K)"
immler@69544
   146
  using Ke Kc unfolding closedin_def Diff_Inter by auto
immler@69544
   147
immler@69544
   148
lemma closedin_INT[intro]:
immler@69544
   149
  assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
immler@69544
   150
  shows "closedin U (\<Inter>x\<in>A. B x)"
immler@69544
   151
  apply (rule closedin_Inter)
immler@69544
   152
  using assms
immler@69544
   153
  apply auto
immler@69544
   154
  done
immler@69544
   155
immler@69544
   156
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
immler@69544
   157
  using closedin_Inter[of "{S,T}" U] by auto
immler@69544
   158
immler@69544
   159
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
immler@69544
   160
  apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2)
immler@69544
   161
  apply (metis openin_subset subset_eq)
immler@69544
   162
  done
immler@69544
   163
immler@69544
   164
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
immler@69544
   165
  by (simp add: openin_closedin_eq)
immler@69544
   166
immler@69544
   167
lemma openin_diff[intro]:
immler@69544
   168
  assumes oS: "openin U S"
immler@69544
   169
    and cT: "closedin U T"
immler@69544
   170
  shows "openin U (S - T)"
immler@69544
   171
proof -
immler@69544
   172
  have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
immler@69544
   173
    by (auto simp: topspace_def openin_subset)
immler@69544
   174
  then show ?thesis using oS cT
immler@69544
   175
    by (auto simp: closedin_def)
immler@69544
   176
qed
immler@69544
   177
immler@69544
   178
lemma closedin_diff[intro]:
immler@69544
   179
  assumes oS: "closedin U S"
immler@69544
   180
    and cT: "openin U T"
immler@69544
   181
  shows "closedin U (S - T)"
immler@69544
   182
proof -
immler@69544
   183
  have "S - T = S \<inter> (topspace U - T)"
immler@69544
   184
    using closedin_subset[of U S] oS cT by (auto simp: topspace_def)
immler@69544
   185
  then show ?thesis
immler@69544
   186
    using oS cT by (auto simp: openin_closedin_eq)
immler@69544
   187
qed
immler@69544
   188
immler@69544
   189
immler@69544
   190
subsection\<open>The discrete topology\<close>
immler@69544
   191
immler@69544
   192
definition discrete_topology where "discrete_topology U \<equiv> topology (\<lambda>S. S \<subseteq> U)"
immler@69544
   193
immler@69544
   194
lemma openin_discrete_topology [simp]: "openin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
immler@69544
   195
proof -
immler@69544
   196
  have "istopology (\<lambda>S. S \<subseteq> U)"
immler@69544
   197
    by (auto simp: istopology_def)
immler@69544
   198
  then show ?thesis
immler@69544
   199
    by (simp add: discrete_topology_def topology_inverse')
immler@69544
   200
qed
immler@69544
   201
immler@69544
   202
lemma topspace_discrete_topology [simp]: "topspace(discrete_topology U) = U"
immler@69544
   203
  by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)
immler@69544
   204
immler@69544
   205
lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
immler@69544
   206
  by (simp add: closedin_def)
immler@69544
   207
immler@69544
   208
lemma discrete_topology_unique:
immler@69544
   209
   "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
immler@69544
   210
proof
immler@69544
   211
  assume R: ?rhs
immler@69544
   212
  then have "openin X S" if "S \<subseteq> U" for S
immler@69544
   213
    using openin_subopen subsetD that by fastforce
immler@69544
   214
  moreover have "x \<in> topspace X" if "openin X S" and "x \<in> S" for x S
immler@69544
   215
    using openin_subset that by blast
immler@69544
   216
  ultimately
immler@69544
   217
  show ?lhs
immler@69544
   218
    using R by (auto simp: topology_eq)
immler@69544
   219
qed auto
immler@69544
   220
immler@69544
   221
lemma discrete_topology_unique_alt:
immler@69544
   222
  "discrete_topology U = X \<longleftrightarrow> topspace X \<subseteq> U \<and> (\<forall>x \<in> U. openin X {x})"
immler@69544
   223
  using openin_subset
immler@69544
   224
  by (auto simp: discrete_topology_unique)
immler@69544
   225
immler@69544
   226
lemma subtopology_eq_discrete_topology_empty:
immler@69544
   227
   "X = discrete_topology {} \<longleftrightarrow> topspace X = {}"
immler@69544
   228
  using discrete_topology_unique [of "{}" X] by auto
immler@69544
   229
immler@69544
   230
lemma subtopology_eq_discrete_topology_sing:
immler@69544
   231
   "X = discrete_topology {a} \<longleftrightarrow> topspace X = {a}"
immler@69544
   232
  by (metis discrete_topology_unique openin_topspace singletonD)
immler@69544
   233
immler@69544
   234
immler@69544
   235
subsection \<open>Subspace topology\<close>
immler@69544
   236
nipkow@69600
   237
definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
nipkow@69600
   238
"subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
immler@69544
   239
immler@69544
   240
lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
immler@69544
   241
  (is "istopology ?L")
immler@69544
   242
proof -
immler@69544
   243
  have "?L {}" by blast
immler@69544
   244
  {
immler@69544
   245
    fix A B
immler@69544
   246
    assume A: "?L A" and B: "?L B"
immler@69544
   247
    from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V"
immler@69544
   248
      by blast
immler@69544
   249
    have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
immler@69544
   250
      using Sa Sb by blast+
immler@69544
   251
    then have "?L (A \<inter> B)" by blast
immler@69544
   252
  }
immler@69544
   253
  moreover
immler@69544
   254
  {
immler@69544
   255
    fix K
immler@69544
   256
    assume K: "K \<subseteq> Collect ?L"
immler@69544
   257
    have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
immler@69544
   258
      by blast
immler@69544
   259
    from K[unfolded th0 subset_image_iff]
immler@69544
   260
    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
immler@69544
   261
      by blast
immler@69544
   262
    have "\<Union>K = (\<Union>Sk) \<inter> V"
immler@69544
   263
      using Sk by auto
immler@69544
   264
    moreover have "openin U (\<Union>Sk)"
immler@69544
   265
      using Sk by (auto simp: subset_eq)
immler@69544
   266
    ultimately have "?L (\<Union>K)" by blast
immler@69544
   267
  }
immler@69544
   268
  ultimately show ?thesis
immler@69544
   269
    unfolding subset_eq mem_Collect_eq istopology_def by auto
immler@69544
   270
qed
immler@69544
   271
immler@69544
   272
lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
immler@69544
   273
  unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
immler@69544
   274
  by auto
immler@69544
   275
immler@69544
   276
lemma openin_subtopology_Int:
immler@69544
   277
   "openin X S \<Longrightarrow> openin (subtopology X T) (S \<inter> T)"
immler@69544
   278
  using openin_subtopology by auto
immler@69544
   279
immler@69544
   280
lemma openin_subtopology_Int2:
immler@69544
   281
   "openin X T \<Longrightarrow> openin (subtopology X S) (S \<inter> T)"
immler@69544
   282
  using openin_subtopology by auto
immler@69544
   283
immler@69544
   284
lemma openin_subtopology_diff_closed:
immler@69544
   285
   "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> openin (subtopology X S) (S - T)"
immler@69544
   286
  unfolding closedin_def openin_subtopology
immler@69544
   287
  by (rule_tac x="topspace X - T" in exI) auto
immler@69544
   288
immler@69544
   289
lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
immler@69544
   290
  by (force simp: relative_to_def openin_subtopology)
immler@69544
   291
lp15@69874
   292
lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U \<inter> V"
immler@69544
   293
  by (auto simp: topspace_def openin_subtopology)
immler@69544
   294
lp15@69710
   295
lemma topspace_subtopology_subset:
lp15@69710
   296
   "S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
lp15@69710
   297
  by (simp add: inf.absorb_iff2 topspace_subtopology)
lp15@69710
   298
immler@69544
   299
lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
immler@69544
   300
  unfolding closedin_def topspace_subtopology
immler@69544
   301
  by (auto simp: openin_subtopology)
immler@69544
   302
immler@69544
   303
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
immler@69544
   304
  unfolding openin_subtopology
immler@69544
   305
  by auto (metis IntD1 in_mono openin_subset)
immler@69544
   306
immler@69544
   307
lemma subtopology_subtopology:
immler@69544
   308
   "subtopology (subtopology X S) T = subtopology X (S \<inter> T)"
immler@69544
   309
proof -
immler@69544
   310
  have eq: "\<And>T'. (\<exists>S'. T' = S' \<inter> T \<and> (\<exists>T. openin X T \<and> S' = T \<inter> S)) = (\<exists>Sa. T' = Sa \<inter> (S \<inter> T) \<and> openin X Sa)"
immler@69544
   311
    by (metis inf_assoc)
immler@69544
   312
  have "subtopology (subtopology X S) T = topology (\<lambda>Ta. \<exists>Sa. Ta = Sa \<inter> T \<and> openin (subtopology X S) Sa)"
immler@69544
   313
    by (simp add: subtopology_def)
immler@69544
   314
  also have "\<dots> = subtopology X (S \<inter> T)"
immler@69544
   315
    by (simp add: openin_subtopology eq) (simp add: subtopology_def)
immler@69544
   316
  finally show ?thesis .
immler@69544
   317
qed
immler@69544
   318
immler@69544
   319
lemma openin_subtopology_alt:
immler@69544
   320
     "openin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (openin X)"
immler@69544
   321
  by (simp add: image_iff inf_commute openin_subtopology)
immler@69544
   322
immler@69544
   323
lemma closedin_subtopology_alt:
immler@69544
   324
     "closedin (subtopology X U) S \<longleftrightarrow> S \<in> (\<lambda>T. U \<inter> T) ` Collect (closedin X)"
immler@69544
   325
  by (simp add: image_iff inf_commute closedin_subtopology)
immler@69544
   326
immler@69544
   327
lemma subtopology_superset:
immler@69544
   328
  assumes UV: "topspace U \<subseteq> V"
immler@69544
   329
  shows "subtopology U V = U"
immler@69544
   330
proof -
immler@69544
   331
  {
immler@69544
   332
    fix S
immler@69544
   333
    {
immler@69544
   334
      fix T
immler@69544
   335
      assume T: "openin U T" "S = T \<inter> V"
immler@69544
   336
      from T openin_subset[OF T(1)] UV have eq: "S = T"
immler@69544
   337
        by blast
immler@69544
   338
      have "openin U S"
immler@69544
   339
        unfolding eq using T by blast
immler@69544
   340
    }
immler@69544
   341
    moreover
immler@69544
   342
    {
immler@69544
   343
      assume S: "openin U S"
immler@69544
   344
      then have "\<exists>T. openin U T \<and> S = T \<inter> V"
immler@69544
   345
        using openin_subset[OF S] UV by auto
immler@69544
   346
    }
immler@69544
   347
    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
immler@69544
   348
      by blast
immler@69544
   349
  }
immler@69544
   350
  then show ?thesis
immler@69544
   351
    unfolding topology_eq openin_subtopology by blast
immler@69544
   352
qed
immler@69544
   353
immler@69544
   354
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
immler@69544
   355
  by (simp add: subtopology_superset)
immler@69544
   356
immler@69544
   357
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
immler@69544
   358
  by (simp add: subtopology_superset)
immler@69544
   359
lp15@69710
   360
lemma subtopology_restrict:
lp15@69710
   361
   "subtopology X (topspace X \<inter> S) = subtopology X S"
lp15@69710
   362
  by (metis subtopology_subtopology subtopology_topspace)
lp15@69710
   363
immler@69544
   364
lemma openin_subtopology_empty:
immler@69544
   365
   "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
immler@69544
   366
by (metis Int_empty_right openin_empty openin_subtopology)
immler@69544
   367
immler@69544
   368
lemma closedin_subtopology_empty:
immler@69544
   369
   "closedin (subtopology U {}) S \<longleftrightarrow> S = {}"
immler@69544
   370
by (metis Int_empty_right closedin_empty closedin_subtopology)
immler@69544
   371
immler@69544
   372
lemma closedin_subtopology_refl [simp]:
immler@69544
   373
   "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
immler@69544
   374
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
immler@69544
   375
immler@69544
   376
lemma closedin_topspace_empty: "topspace T = {} \<Longrightarrow> (closedin T S \<longleftrightarrow> S = {})"
immler@69544
   377
  by (simp add: closedin_def)
immler@69544
   378
immler@69544
   379
lemma openin_imp_subset:
immler@69544
   380
   "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
immler@69544
   381
by (metis Int_iff openin_subtopology subsetI)
immler@69544
   382
immler@69544
   383
lemma closedin_imp_subset:
immler@69544
   384
   "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
immler@69544
   385
by (simp add: closedin_def topspace_subtopology)
immler@69544
   386
immler@69544
   387
lemma openin_open_subtopology:
immler@69544
   388
     "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
immler@69544
   389
  by (metis inf.orderE openin_Int openin_imp_subset openin_subtopology)
immler@69544
   390
immler@69544
   391
lemma closedin_closed_subtopology:
immler@69544
   392
     "closedin X S \<Longrightarrow> (closedin (subtopology X S) T \<longleftrightarrow> closedin X T \<and> T \<subseteq> S)"
immler@69544
   393
  by (metis closedin_Int closedin_imp_subset closedin_subtopology inf.orderE)
immler@69544
   394
immler@69544
   395
lemma openin_subtopology_Un:
immler@69544
   396
    "\<lbrakk>openin (subtopology X T) S; openin (subtopology X U) S\<rbrakk>
immler@69544
   397
     \<Longrightarrow> openin (subtopology X (T \<union> U)) S"
immler@69544
   398
by (simp add: openin_subtopology) blast
immler@69544
   399
immler@69544
   400
lemma closedin_subtopology_Un:
immler@69544
   401
    "\<lbrakk>closedin (subtopology X T) S; closedin (subtopology X U) S\<rbrakk>
immler@69544
   402
     \<Longrightarrow> closedin (subtopology X (T \<union> U)) S"
immler@69544
   403
by (simp add: closedin_subtopology) blast
immler@69544
   404
lp15@69918
   405
lemma openin_trans_full:
lp15@69918
   406
   "\<lbrakk>openin (subtopology X U) S; openin X U\<rbrakk> \<Longrightarrow> openin X S"
lp15@69918
   407
  by (simp add: openin_open_subtopology)
lp15@69918
   408
lp15@69918
   409
lp15@69918
   410
subsection \<open>The canonical topology from the underlying type class\<close>
immler@69544
   411
lp15@69710
   412
abbreviation%important euclidean :: "'a::topological_space topology"
lp15@69710
   413
  where "euclidean \<equiv> topology open"
lp15@69710
   414
lp15@69710
   415
abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
lp15@69710
   416
  where "top_of_set \<equiv> subtopology (topology open)"
immler@69544
   417
immler@69544
   418
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
immler@69544
   419
  apply (rule cong[where x=S and y=S])
immler@69544
   420
  apply (rule topology_inverse[symmetric])
immler@69544
   421
  apply (auto simp: istopology_def)
immler@69544
   422
  done
immler@69544
   423
immler@69544
   424
declare open_openin [symmetric, simp]
immler@69544
   425
immler@69544
   426
lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
immler@69544
   427
  by (force simp: topspace_def)
immler@69544
   428
lp15@69922
   429
lemma topspace_euclidean_subtopology[simp]: "topspace (top_of_set S) = S"
immler@69544
   430
  by (simp add: topspace_subtopology)
immler@69544
   431
immler@69544
   432
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
immler@69544
   433
  by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
immler@69544
   434
immler@69544
   435
declare closed_closedin [symmetric, simp]
immler@69544
   436
lp15@69922
   437
lemma openin_subtopology_self [simp]: "openin (top_of_set S) S"
immler@69544
   438
  by (metis openin_topspace topspace_euclidean_subtopology)
immler@69544
   439
immler@69544
   440
subsubsection\<open>The most basic facts about the usual topology and metric on R\<close>
immler@69544
   441
immler@69544
   442
abbreviation euclideanreal :: "real topology"
immler@69544
   443
  where "euclideanreal \<equiv> topology open"
immler@69544
   444
immler@69544
   445
subsection \<open>Basic "localization" results are handy for connectedness.\<close>
immler@69544
   446
lp15@69922
   447
lemma openin_open: "openin (top_of_set U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
immler@69544
   448
  by (auto simp: openin_subtopology)
immler@69544
   449
immler@69544
   450
lemma openin_Int_open:
lp15@69922
   451
   "\<lbrakk>openin (top_of_set U) S; open T\<rbrakk>
lp15@69922
   452
        \<Longrightarrow> openin (top_of_set U) (S \<inter> T)"
immler@69544
   453
by (metis open_Int Int_assoc openin_open)
immler@69544
   454
lp15@69922
   455
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (top_of_set U) (U \<inter> S)"
immler@69544
   456
  by (auto simp: openin_open)
immler@69544
   457
immler@69544
   458
lemma open_openin_trans[trans]:
lp15@69922
   459
  "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (top_of_set S) T"
immler@69544
   460
  by (metis Int_absorb1  openin_open_Int)
immler@69544
   461
lp15@69922
   462
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (top_of_set T) S"
immler@69544
   463
  by (auto simp: openin_open)
immler@69544
   464
lp15@69922
   465
lemma closedin_closed: "closedin (top_of_set U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
immler@69544
   466
  by (simp add: closedin_subtopology Int_ac)
immler@69544
   467
lp15@69922
   468
lemma closedin_closed_Int: "closed S \<Longrightarrow> closedin (top_of_set U) (U \<inter> S)"
immler@69544
   469
  by (metis closedin_closed)
immler@69544
   470
lp15@69922
   471
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (top_of_set T) S"
immler@69544
   472
  by (auto simp: closedin_closed)
immler@69544
   473
immler@69544
   474
lemma closedin_closed_subset:
lp15@69922
   475
 "\<lbrakk>closedin (top_of_set U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
lp15@69922
   476
             \<Longrightarrow> closedin (top_of_set T) S"
immler@69544
   477
  by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)
immler@69544
   478
immler@69544
   479
lemma finite_imp_closedin:
immler@69544
   480
  fixes S :: "'a::t1_space set"
lp15@69922
   481
  shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (top_of_set T) S"
immler@69544
   482
    by (simp add: finite_imp_closed closed_subset)
immler@69544
   483
immler@69544
   484
lemma closedin_singleton [simp]:
immler@69544
   485
  fixes a :: "'a::t1_space"
lp15@69922
   486
  shows "closedin (top_of_set U) {a} \<longleftrightarrow> a \<in> U"
immler@69544
   487
using closedin_subset  by (force intro: closed_subset)
immler@69544
   488
immler@69544
   489
lemma openin_euclidean_subtopology_iff:
immler@69544
   490
  fixes S U :: "'a::metric_space set"
lp15@69922
   491
  shows "openin (top_of_set U) S \<longleftrightarrow>
immler@69544
   492
    S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
immler@69544
   493
  (is "?lhs \<longleftrightarrow> ?rhs")
immler@69544
   494
proof
immler@69544
   495
  assume ?lhs
immler@69544
   496
  then show ?rhs
immler@69544
   497
    unfolding openin_open open_dist by blast
immler@69544
   498
next
immler@69544
   499
  define T where "T = {x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}"
immler@69544
   500
  have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
immler@69544
   501
    unfolding T_def
immler@69544
   502
    apply clarsimp
immler@69544
   503
    apply (rule_tac x="d - dist x a" in exI)
immler@69544
   504
    apply (clarsimp simp add: less_diff_eq)
immler@69544
   505
    by (metis dist_commute dist_triangle_lt)
immler@69544
   506
  assume ?rhs then have 2: "S = U \<inter> T"
immler@69544
   507
    unfolding T_def
immler@69544
   508
    by auto (metis dist_self)
immler@69544
   509
  from 1 2 show ?lhs
immler@69544
   510
    unfolding openin_open open_dist by fast
immler@69544
   511
qed
immler@69544
   512
immler@69544
   513
lemma connected_openin:
immler@69544
   514
      "connected S \<longleftrightarrow>
lp15@69922
   515
       \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
lp15@69922
   516
                 openin (top_of_set S) E2 \<and>
immler@69544
   517
                 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
immler@69544
   518
  apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
immler@69544
   519
  by (simp_all, blast+)  (* SLOW *)
immler@69544
   520
immler@69544
   521
lemma connected_openin_eq:
immler@69544
   522
      "connected S \<longleftrightarrow>
lp15@69922
   523
       \<not>(\<exists>E1 E2. openin (top_of_set S) E1 \<and>
lp15@69922
   524
                 openin (top_of_set S) E2 \<and>
immler@69544
   525
                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
immler@69544
   526
                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
immler@69544
   527
  apply (simp add: connected_openin, safe, blast)
immler@69544
   528
  by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
immler@69544
   529
immler@69544
   530
lemma connected_closedin:
immler@69544
   531
      "connected S \<longleftrightarrow>
immler@69544
   532
       (\<nexists>E1 E2.
lp15@69922
   533
        closedin (top_of_set S) E1 \<and>
lp15@69922
   534
        closedin (top_of_set S) E2 \<and>
immler@69544
   535
        S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
immler@69544
   536
       (is "?lhs = ?rhs")
immler@69544
   537
proof
immler@69544
   538
  assume ?lhs
immler@69544
   539
  then show ?rhs 
immler@69544
   540
    by (auto simp add: connected_closed closedin_closed)
immler@69544
   541
next
immler@69544
   542
  assume R: ?rhs
immler@69544
   543
  then show ?lhs 
immler@69544
   544
  proof (clarsimp simp add: connected_closed closedin_closed)
immler@69544
   545
    fix A B 
immler@69544
   546
    assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
immler@69544
   547
      and disj: "A \<inter> B \<inter> S = {}"
immler@69544
   548
      and cl: "closed A" "closed B"
immler@69544
   549
    have "S \<inter> (A \<union> B) = S"
immler@69544
   550
      using s_sub(1) by auto
immler@69544
   551
    have "S - A = B \<inter> S"
immler@69544
   552
      using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
immler@69544
   553
    then have "S \<inter> A = {}"
immler@69544
   554
      by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
immler@69544
   555
    then show "A \<inter> S = {}"
immler@69544
   556
      by blast
immler@69544
   557
  qed
immler@69544
   558
qed
immler@69544
   559
immler@69544
   560
lemma connected_closedin_eq:
immler@69544
   561
      "connected S \<longleftrightarrow>
immler@69544
   562
           \<not>(\<exists>E1 E2.
lp15@69922
   563
                 closedin (top_of_set S) E1 \<and>
lp15@69922
   564
                 closedin (top_of_set S) E2 \<and>
immler@69544
   565
                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
immler@69544
   566
                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
immler@69544
   567
  apply (simp add: connected_closedin, safe, blast)
immler@69544
   568
  by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
immler@69544
   569
immler@69544
   570
text \<open>These "transitivity" results are handy too\<close>
immler@69544
   571
immler@69544
   572
lemma openin_trans[trans]:
lp15@69922
   573
  "openin (top_of_set T) S \<Longrightarrow> openin (top_of_set U) T \<Longrightarrow>
lp15@69922
   574
    openin (top_of_set U) S"
lp15@69710
   575
  by (metis openin_Int_open openin_open)
immler@69544
   576
lp15@69922
   577
lemma openin_open_trans: "openin (top_of_set T) S \<Longrightarrow> open T \<Longrightarrow> open S"
immler@69544
   578
  by (auto simp: openin_open intro: openin_trans)
immler@69544
   579
immler@69544
   580
lemma closedin_trans[trans]:
lp15@69922
   581
  "closedin (top_of_set T) S \<Longrightarrow> closedin (top_of_set U) T \<Longrightarrow>
lp15@69922
   582
    closedin (top_of_set U) S"
immler@69544
   583
  by (auto simp: closedin_closed closed_Inter Int_assoc)
immler@69544
   584
lp15@69922
   585
lemma closedin_closed_trans: "closedin (top_of_set T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
immler@69544
   586
  by (auto simp: closedin_closed intro: closedin_trans)
immler@69544
   587
immler@69544
   588
lemma openin_subtopology_Int_subset:
lp15@69922
   589
   "\<lbrakk>openin (top_of_set u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (top_of_set v) (v \<inter> S)"
immler@69544
   590
  by (auto simp: openin_subtopology)
immler@69544
   591
lp15@69922
   592
lemma openin_open_eq: "open s \<Longrightarrow> (openin (top_of_set s) t \<longleftrightarrow> open t \<and> t \<subseteq> s)"
immler@69544
   593
  using open_subset openin_open_trans openin_subset by fastforce
immler@69544
   594
lp15@69144
   595
lp15@69144
   596
subsection\<open>Derived set (set of limit points)\<close>
lp15@69144
   597
lp15@69144
   598
definition derived_set_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "derived'_set'_of" 80)
lp15@69144
   599
  where "X derived_set_of S \<equiv>
lp15@69144
   600
         {x \<in> topspace X.
lp15@69144
   601
                (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
lp15@69144
   602
lp15@69874
   603
lemma derived_set_of_restrict [simp]:
lp15@69144
   604
   "X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
lp15@69144
   605
  by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
lp15@69144
   606
lp15@69144
   607
lemma in_derived_set_of:
lp15@69144
   608
   "x \<in> X derived_set_of S \<longleftrightarrow> x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))"
lp15@69144
   609
  by (simp add: derived_set_of_def)
lp15@69144
   610
lp15@69144
   611
lemma derived_set_of_subset_topspace:
lp15@69144
   612
   "X derived_set_of S \<subseteq> topspace X"
lp15@69144
   613
  by (auto simp add: derived_set_of_def)
lp15@69144
   614
lp15@69144
   615
lemma derived_set_of_subtopology:
lp15@69144
   616
   "(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
lp15@69144
   617
  by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast
lp15@69144
   618
lp15@69144
   619
lemma derived_set_of_subset_subtopology:
lp15@69144
   620
   "(subtopology X S) derived_set_of T \<subseteq> S"
lp15@69144
   621
  by (simp add: derived_set_of_subtopology)
lp15@69144
   622
lp15@69144
   623
lemma derived_set_of_empty [simp]: "X derived_set_of {} = {}"
lp15@69144
   624
  by (auto simp: derived_set_of_def)
lp15@69144
   625
lp15@69144
   626
lemma derived_set_of_mono:
lp15@69144
   627
   "S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
lp15@69144
   628
  unfolding derived_set_of_def by blast
lp15@69144
   629
lp15@69874
   630
lemma derived_set_of_Un:
lp15@69144
   631
   "X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
lp15@69144
   632
proof
lp15@69144
   633
  show "?lhs \<subseteq> ?rhs"
lp15@69144
   634
    apply (clarsimp simp: in_derived_set_of)
lp15@69144
   635
    by (metis IntE IntI openin_Int)
lp15@69144
   636
  show "?rhs \<subseteq> ?lhs"
lp15@69144
   637
    by (simp add: derived_set_of_mono)
lp15@69144
   638
qed
lp15@69144
   639
lp15@69874
   640
lemma derived_set_of_Union:
lp15@69144
   641
   "finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
lp15@69144
   642
proof (induction \<F> rule: finite_induct)
lp15@69144
   643
  case (insert S \<F>)
lp15@69144
   644
  then show ?case
lp15@69874
   645
    by (simp add: derived_set_of_Un)
lp15@69144
   646
qed auto
lp15@69144
   647
lp15@69144
   648
lemma derived_set_of_topspace:
lp15@69144
   649
  "X derived_set_of (topspace X) = {x \<in> topspace X. \<not> openin X {x}}"
lp15@69144
   650
  apply (auto simp: in_derived_set_of)
lp15@69144
   651
  by (metis Set.set_insert all_not_in_conv insertCI openin_subset subsetCE)
lp15@69144
   652
lp15@69144
   653
lemma discrete_topology_unique_derived_set:
lp15@69144
   654
     "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> X derived_set_of U = {}"
lp15@69144
   655
  by (auto simp: discrete_topology_unique derived_set_of_topspace)
lp15@69144
   656
lp15@69144
   657
lemma subtopology_eq_discrete_topology_eq:
lp15@69144
   658
   "subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
lp15@69144
   659
  using discrete_topology_unique_derived_set [of U "subtopology X U"]
lp15@69144
   660
  by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)
lp15@69144
   661
lp15@69144
   662
lemma subtopology_eq_discrete_topology:
lp15@69144
   663
   "S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
lp15@69144
   664
        \<Longrightarrow> subtopology X S = discrete_topology S"
lp15@69144
   665
  by (simp add: subtopology_eq_discrete_topology_eq)
lp15@69144
   666
lp15@69144
   667
lemma subtopology_eq_discrete_topology_gen:
lp15@69144
   668
   "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
lp15@69144
   669
  by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
lp15@69144
   670
lp15@69712
   671
lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
lp15@69712
   672
proof -
lp15@69712
   673
  have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
lp15@69712
   674
    by force
lp15@69712
   675
  then show ?thesis
lp15@69712
   676
    by (simp add: subtopology_def) (simp add: discrete_topology_def)
lp15@69712
   677
qed
lp15@69144
   678
lemma openin_Int_derived_set_of_subset:
lp15@69144
   679
   "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
lp15@69144
   680
  by (auto simp: derived_set_of_def)
lp15@69144
   681
lp15@69144
   682
lemma openin_Int_derived_set_of_eq:
lp15@69144
   683
  "openin X S \<Longrightarrow> S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
lp15@69144
   684
  apply auto
lp15@69144
   685
   apply (meson IntI openin_Int_derived_set_of_subset subsetCE)
lp15@69144
   686
  by (meson derived_set_of_mono inf_sup_ord(2) subset_eq)
lp15@69144
   687
lp15@69144
   688
lp15@69144
   689
subsection\<open> Closure with respect to a topological space\<close>
lp15@69144
   690
lp15@69144
   691
definition closure_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "closure'_of" 80)
lp15@69144
   692
  where "X closure_of S \<equiv> {x \<in> topspace X. \<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y \<in> S. y \<in> T)}"
lp15@69144
   693
lp15@69144
   694
lemma closure_of_restrict: "X closure_of S = X closure_of (topspace X \<inter> S)"
lp15@69144
   695
  unfolding closure_of_def
lp15@69144
   696
  apply safe
lp15@69144
   697
  apply (meson IntI openin_subset subset_iff)
lp15@69144
   698
  by auto
lp15@69144
   699
lp15@69144
   700
lemma in_closure_of:
lp15@69144
   701
   "x \<in> X closure_of S \<longleftrightarrow>
lp15@69144
   702
    x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y. y \<in> S \<and> y \<in> T))"
lp15@69144
   703
  by (auto simp: closure_of_def)
lp15@69144
   704
lp15@69144
   705
lemma closure_of: "X closure_of S = topspace X \<inter> (S \<union> X derived_set_of S)"
lp15@69144
   706
  by (fastforce simp: in_closure_of in_derived_set_of)
lp15@69144
   707
lp15@69144
   708
lemma closure_of_alt: "X closure_of S = topspace X \<inter> S \<union> X derived_set_of S"
lp15@69144
   709
  using derived_set_of_subset_topspace [of X S]
lp15@69144
   710
  unfolding closure_of_def in_derived_set_of
lp15@69144
   711
  by safe (auto simp: in_derived_set_of)
lp15@69144
   712
lp15@69144
   713
lemma derived_set_of_subset_closure_of:
lp15@69144
   714
   "X derived_set_of S \<subseteq> X closure_of S"
lp15@69144
   715
  by (fastforce simp: closure_of_def in_derived_set_of)
lp15@69144
   716
lp15@69144
   717
lemma closure_of_subtopology:
lp15@69144
   718
  "(subtopology X U) closure_of S = U \<inter> (X closure_of (U \<inter> S))"
lp15@69144
   719
  unfolding closure_of_def topspace_subtopology openin_subtopology
lp15@69144
   720
  by safe (metis (full_types) IntI Int_iff inf.commute)+
lp15@69144
   721
lp15@69144
   722
lemma closure_of_empty [simp]: "X closure_of {} = {}"
lp15@69144
   723
  by (simp add: closure_of_alt)
lp15@69144
   724
lp15@69144
   725
lemma closure_of_topspace [simp]: "X closure_of topspace X = topspace X"
lp15@69144
   726
  by (simp add: closure_of)
lp15@69144
   727
lp15@69144
   728
lemma closure_of_UNIV [simp]: "X closure_of UNIV = topspace X"
lp15@69144
   729
  by (simp add: closure_of)
lp15@69144
   730
lp15@69144
   731
lemma closure_of_subset_topspace: "X closure_of S \<subseteq> topspace X"
lp15@69144
   732
  by (simp add: closure_of)
lp15@69144
   733
lp15@69144
   734
lemma closure_of_subset_subtopology: "(subtopology X S) closure_of T \<subseteq> S"
lp15@69144
   735
  by (simp add: closure_of_subtopology)
lp15@69144
   736
lp15@69144
   737
lemma closure_of_mono: "S \<subseteq> T \<Longrightarrow> X closure_of S \<subseteq> X closure_of T"
lp15@69144
   738
  by (fastforce simp add: closure_of_def)
lp15@69144
   739
lp15@69144
   740
lemma closure_of_subtopology_subset:
lp15@69144
   741
   "(subtopology X U) closure_of S \<subseteq> (X closure_of S)"
lp15@69144
   742
  unfolding closure_of_subtopology
lp15@69144
   743
  by clarsimp (meson closure_of_mono contra_subsetD inf.cobounded2)
lp15@69144
   744
lp15@69144
   745
lemma closure_of_subtopology_mono:
lp15@69144
   746
   "T \<subseteq> U \<Longrightarrow> (subtopology X T) closure_of S \<subseteq> (subtopology X U) closure_of S"
lp15@69144
   747
  unfolding closure_of_subtopology
lp15@69144
   748
  by auto (meson closure_of_mono inf_mono subset_iff)
lp15@69144
   749
lp15@69144
   750
lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
lp15@69874
   751
  by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_Un inf_sup_distrib1)
lp15@69144
   752
lp15@69144
   753
lemma closure_of_Union:
lp15@69144
   754
   "finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
lp15@69144
   755
by (induction \<F> rule: finite_induct) auto
lp15@69144
   756
lp15@69144
   757
lemma closure_of_subset: "S \<subseteq> topspace X \<Longrightarrow> S \<subseteq> X closure_of S"
lp15@69144
   758
  by (auto simp: closure_of_def)
lp15@69144
   759
lp15@69144
   760
lemma closure_of_subset_Int: "topspace X \<inter> S \<subseteq> X closure_of S"
lp15@69144
   761
  by (auto simp: closure_of_def)
lp15@69144
   762
lp15@69144
   763
lemma closure_of_subset_eq: "S \<subseteq> topspace X \<and> X closure_of S \<subseteq> S \<longleftrightarrow> closedin X S"
lp15@69144
   764
proof (cases "S \<subseteq> topspace X")
lp15@69144
   765
  case True
lp15@69144
   766
  then have "\<forall>x. x \<in> topspace X \<and> (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<in>S. y \<in> T)) \<longrightarrow> x \<in> S
lp15@69144
   767
             \<Longrightarrow> openin X (topspace X - S)"
lp15@69144
   768
    apply (subst openin_subopen, safe)
lp15@69144
   769
    by (metis DiffI subset_eq openin_subset [of X])
lp15@69144
   770
  then show ?thesis
lp15@69144
   771
    by (auto simp: closedin_def closure_of_def)
lp15@69144
   772
next
lp15@69144
   773
  case False
lp15@69144
   774
  then show ?thesis
lp15@69144
   775
    by (simp add: closedin_def)
lp15@69144
   776
qed
lp15@69144
   777
lp15@69144
   778
lemma closure_of_eq: "X closure_of S = S \<longleftrightarrow> closedin X S"
lp15@69144
   779
proof (cases "S \<subseteq> topspace X")
lp15@69144
   780
  case True
lp15@69144
   781
  then show ?thesis
lp15@69144
   782
    by (metis closure_of_subset closure_of_subset_eq set_eq_subset)
lp15@69144
   783
next
lp15@69144
   784
  case False
lp15@69144
   785
  then show ?thesis
lp15@69144
   786
    using closure_of closure_of_subset_eq by fastforce
lp15@69144
   787
qed
lp15@69144
   788
lp15@69144
   789
lemma closedin_contains_derived_set:
lp15@69144
   790
   "closedin X S \<longleftrightarrow> X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X"
lp15@69144
   791
proof (intro iffI conjI)
lp15@69144
   792
  show "closedin X S \<Longrightarrow> X derived_set_of S \<subseteq> S"
lp15@69144
   793
    using closure_of_eq derived_set_of_subset_closure_of by fastforce
lp15@69144
   794
  show "closedin X S \<Longrightarrow> S \<subseteq> topspace X"
lp15@69144
   795
    using closedin_subset by blast
lp15@69144
   796
  show "X derived_set_of S \<subseteq> S \<and> S \<subseteq> topspace X \<Longrightarrow> closedin X S"
lp15@69144
   797
    by (metis closure_of closure_of_eq inf.absorb_iff2 sup.orderE)
lp15@69144
   798
qed
lp15@69144
   799
lp15@69144
   800
lemma derived_set_subset_gen:
lp15@69144
   801
   "X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X (topspace X \<inter> S)"
lp15@69144
   802
  by (simp add: closedin_contains_derived_set derived_set_of_restrict derived_set_of_subset_topspace)
lp15@69144
   803
lp15@69144
   804
lemma derived_set_subset: "S \<subseteq> topspace X \<Longrightarrow> (X derived_set_of S \<subseteq> S \<longleftrightarrow> closedin X S)"
lp15@69144
   805
  by (simp add: closedin_contains_derived_set)
lp15@69144
   806
lp15@69144
   807
lemma closedin_derived_set:
lp15@69144
   808
     "closedin (subtopology X T) S \<longleftrightarrow>
lp15@69144
   809
      S \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> S)"
lp15@69144
   810
  by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)
lp15@69144
   811
lp15@69144
   812
lemma closedin_Int_closure_of:
lp15@69144
   813
     "closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
lp15@69144
   814
  by (metis Int_left_absorb closure_of_eq closure_of_subtopology)
lp15@69144
   815
lp15@69144
   816
lemma closure_of_closedin: "closedin X S \<Longrightarrow> X closure_of S = S"
lp15@69144
   817
  by (simp add: closure_of_eq)
lp15@69144
   818
lp15@69144
   819
lemma closure_of_eq_diff: "X closure_of S = topspace X - \<Union>{T. openin X T \<and> disjnt S T}"
lp15@69144
   820
  by (auto simp: closure_of_def disjnt_iff)
lp15@69144
   821
lp15@69144
   822
lemma closedin_closure_of [simp]: "closedin X (X closure_of S)"
lp15@69144
   823
  unfolding closure_of_eq_diff by blast
lp15@69144
   824
lp15@69144
   825
lemma closure_of_closure_of [simp]: "X closure_of (X closure_of S) = X closure_of S"
lp15@69144
   826
  by (simp add: closure_of_eq)
lp15@69144
   827
lp15@69144
   828
lemma closure_of_hull:
lp15@69144
   829
  assumes "S \<subseteq> topspace X" shows "X closure_of S = (closedin X) hull S"
lp15@69144
   830
proof (rule hull_unique [THEN sym])
lp15@69144
   831
  show "S \<subseteq> X closure_of S"
lp15@69144
   832
    by (simp add: closure_of_subset assms)
lp15@69144
   833
next
lp15@69144
   834
  show "closedin X (X closure_of S)"
lp15@69144
   835
    by simp
lp15@69144
   836
  show "\<And>T. \<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> X closure_of S \<subseteq> T"
lp15@69144
   837
    by (metis closure_of_eq closure_of_mono)
lp15@69144
   838
qed
lp15@69144
   839
lp15@69144
   840
lemma closure_of_minimal:
lp15@69144
   841
   "\<lbrakk>S \<subseteq> T; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T"
lp15@69144
   842
  by (metis closure_of_eq closure_of_mono)
lp15@69144
   843
lp15@69144
   844
lemma closure_of_minimal_eq:
lp15@69144
   845
   "\<lbrakk>S \<subseteq> topspace X; closedin X T\<rbrakk> \<Longrightarrow> (X closure_of S) \<subseteq> T \<longleftrightarrow> S \<subseteq> T"
lp15@69144
   846
  by (meson closure_of_minimal closure_of_subset subset_trans)
lp15@69144
   847
lp15@69144
   848
lemma closure_of_unique:
lp15@69144
   849
   "\<lbrakk>S \<subseteq> T; closedin X T;
lp15@69144
   850
     \<And>T'. \<lbrakk>S \<subseteq> T'; closedin X T'\<rbrakk> \<Longrightarrow> T \<subseteq> T'\<rbrakk>
lp15@69144
   851
    \<Longrightarrow> X closure_of S = T"
lp15@69144
   852
  by (meson closedin_closure_of closedin_subset closure_of_minimal closure_of_subset eq_iff order.trans)
lp15@69144
   853
lp15@69144
   854
lemma closure_of_eq_empty_gen: "X closure_of S = {} \<longleftrightarrow> disjnt (topspace X) S"
lp15@69144
   855
  unfolding disjnt_def closure_of_restrict [where S=S]
lp15@69144
   856
  using closure_of by fastforce
lp15@69144
   857
lp15@69144
   858
lemma closure_of_eq_empty: "S \<subseteq> topspace X \<Longrightarrow> X closure_of S = {} \<longleftrightarrow> S = {}"
lp15@69144
   859
  using closure_of_subset by fastforce
lp15@69144
   860
lp15@69144
   861
lemma openin_Int_closure_of_subset:
lp15@69144
   862
  assumes "openin X S"
lp15@69144
   863
  shows "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
lp15@69144
   864
proof -
lp15@69144
   865
  have "S \<inter> X derived_set_of T = S \<inter> X derived_set_of (S \<inter> T)"
lp15@69144
   866
    by (meson assms openin_Int_derived_set_of_eq)
lp15@69144
   867
  moreover have "S \<inter> (S \<inter> T) = S \<inter> T"
lp15@69144
   868
    by fastforce
lp15@69144
   869
  ultimately show ?thesis
lp15@69144
   870
    by (metis closure_of_alt inf.cobounded2 inf_left_commute inf_sup_distrib1)
lp15@69144
   871
qed
lp15@69144
   872
lp15@69144
   873
lemma closure_of_openin_Int_closure_of:
lp15@69144
   874
  assumes "openin X S"
lp15@69144
   875
  shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)"
lp15@69144
   876
proof
lp15@69144
   877
  show "X closure_of (S \<inter> X closure_of T) \<subseteq> X closure_of (S \<inter> T)"
lp15@69144
   878
    by (simp add: assms closure_of_minimal openin_Int_closure_of_subset)
lp15@69144
   879
next
lp15@69144
   880
  show "X closure_of (S \<inter> T) \<subseteq> X closure_of (S \<inter> X closure_of T)"
lp15@69144
   881
    by (metis Int_lower1 Int_subset_iff assms closedin_closure_of closure_of_minimal_eq closure_of_mono inf_le2 le_infI1 openin_subset)
lp15@69144
   882
qed
lp15@69144
   883
lp15@69144
   884
lemma openin_Int_closure_of_eq:
lp15@69144
   885
  "openin X S \<Longrightarrow> S \<inter> X closure_of T = S \<inter> X closure_of (S \<inter> T)"
lp15@69144
   886
  apply (rule equalityI)
lp15@69144
   887
   apply (simp add: openin_Int_closure_of_subset)
lp15@69144
   888
  by (meson closure_of_mono inf.cobounded2 inf_mono subset_refl)
lp15@69144
   889
lp15@69144
   890
lemma openin_Int_closure_of_eq_empty:
lp15@69144
   891
   "openin X S \<Longrightarrow> S \<inter> X closure_of T = {} \<longleftrightarrow> S \<inter> T = {}"
lp15@69144
   892
  apply (subst openin_Int_closure_of_eq, auto)
lp15@69144
   893
  by (meson IntI closure_of_subset_Int disjoint_iff_not_equal openin_subset subset_eq)
lp15@69144
   894
lp15@69144
   895
lemma closure_of_openin_Int_superset:
lp15@69144
   896
   "openin X S \<and> S \<subseteq> X closure_of T
lp15@69144
   897
        \<Longrightarrow> X closure_of (S \<inter> T) = X closure_of S"
lp15@69144
   898
  by (metis closure_of_openin_Int_closure_of inf.orderE)
lp15@69144
   899
lp15@69144
   900
lemma closure_of_openin_subtopology_Int_closure_of:
lp15@69144
   901
  assumes S: "openin (subtopology X U) S" and "T \<subseteq> U"
lp15@69144
   902
  shows "X closure_of (S \<inter> X closure_of T) = X closure_of (S \<inter> T)" (is "?lhs = ?rhs")
lp15@69144
   903
proof
lp15@69144
   904
  obtain S0 where S0: "openin X S0" "S = S0 \<inter> U"
lp15@69144
   905
    using assms by (auto simp: openin_subtopology)
lp15@69144
   906
  show "?lhs \<subseteq> ?rhs"
lp15@69144
   907
  proof -
lp15@69144
   908
    have "S0 \<inter> X closure_of T = S0 \<inter> X closure_of (S0 \<inter> T)"
lp15@69144
   909
      by (meson S0(1) openin_Int_closure_of_eq)
lp15@69144
   910
    moreover have "S0 \<inter> T = S0 \<inter> U \<inter> T"
lp15@69144
   911
      using \<open>T \<subseteq> U\<close> by fastforce
lp15@69144
   912
    ultimately have "S \<inter> X closure_of T \<subseteq> X closure_of (S \<inter> T)"
lp15@69144
   913
      using S0(2) by auto
lp15@69144
   914
    then show ?thesis
lp15@69144
   915
      by (meson closedin_closure_of closure_of_minimal)
lp15@69144
   916
  qed
lp15@69144
   917
next
lp15@69144
   918
  show "?rhs \<subseteq> ?lhs"
lp15@69144
   919
  proof -
lp15@69144
   920
    have "T \<inter> S \<subseteq> T \<union> X derived_set_of T"
lp15@69144
   921
      by force
lp15@69144
   922
    then show ?thesis
lp15@69144
   923
      by (metis Int_subset_iff S closure_of closure_of_mono inf.cobounded2 inf.coboundedI2 inf_commute openin_closedin_eq topspace_subtopology)
lp15@69144
   924
  qed
lp15@69144
   925
qed
lp15@69144
   926
lp15@69144
   927
lemma closure_of_subtopology_open:
lp15@69144
   928
     "openin X U \<or> S \<subseteq> U \<Longrightarrow> (subtopology X U) closure_of S = U \<inter> X closure_of S"
lp15@69144
   929
  by (metis closure_of_subtopology inf_absorb2 openin_Int_closure_of_eq)
lp15@69144
   930
lp15@69144
   931
lemma discrete_topology_closure_of:
lp15@69144
   932
     "(discrete_topology U) closure_of S = U \<inter> S"
lp15@69144
   933
  by (metis closedin_discrete_topology closure_of_restrict closure_of_unique discrete_topology_unique inf_sup_ord(1) order_refl)
lp15@69144
   934
lp15@69144
   935
lp15@69144
   936
text\<open> Interior with respect to a topological space.                             \<close>
lp15@69144
   937
lp15@69144
   938
definition interior_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "interior'_of" 80)
lp15@69144
   939
  where "X interior_of S \<equiv> {x. \<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> S}"
lp15@69144
   940
lp15@69144
   941
lemma interior_of_restrict:
lp15@69144
   942
   "X interior_of S = X interior_of (topspace X \<inter> S)"
lp15@69144
   943
  using openin_subset by (auto simp: interior_of_def)
lp15@69144
   944
lp15@69144
   945
lemma interior_of_eq: "(X interior_of S = S) \<longleftrightarrow> openin X S"
lp15@69144
   946
  unfolding interior_of_def  using openin_subopen by blast
lp15@69144
   947
lp15@69144
   948
lemma interior_of_openin: "openin X S \<Longrightarrow> X interior_of S = S"
lp15@69144
   949
  by (simp add: interior_of_eq)
lp15@69144
   950
lp15@69144
   951
lemma interior_of_empty [simp]: "X interior_of {} = {}"
lp15@69144
   952
  by (simp add: interior_of_eq)
lp15@69144
   953
lp15@69144
   954
lemma interior_of_topspace [simp]: "X interior_of (topspace X) = topspace X"
lp15@69144
   955
  by (simp add: interior_of_eq)
lp15@69144
   956
lp15@69144
   957
lemma openin_interior_of [simp]: "openin X (X interior_of S)"
lp15@69144
   958
  unfolding interior_of_def
lp15@69144
   959
  using openin_subopen by fastforce
lp15@69144
   960
lp15@69144
   961
lemma interior_of_interior_of [simp]:
lp15@69144
   962
   "X interior_of X interior_of S = X interior_of S"
lp15@69144
   963
  by (simp add: interior_of_eq)
lp15@69144
   964
lp15@69144
   965
lemma interior_of_subset: "X interior_of S \<subseteq> S"
lp15@69144
   966
  by (auto simp: interior_of_def)
lp15@69144
   967
lp15@69144
   968
lemma interior_of_subset_closure_of: "X interior_of S \<subseteq> X closure_of S"
lp15@69144
   969
  by (metis closure_of_subset_Int dual_order.trans interior_of_restrict interior_of_subset)
lp15@69144
   970
lp15@69144
   971
lemma subset_interior_of_eq: "S \<subseteq> X interior_of S \<longleftrightarrow> openin X S"
lp15@69144
   972
  by (metis interior_of_eq interior_of_subset subset_antisym)
lp15@69144
   973
lp15@69144
   974
lemma interior_of_mono: "S \<subseteq> T \<Longrightarrow> X interior_of S \<subseteq> X interior_of T"
lp15@69144
   975
  by (auto simp: interior_of_def)
lp15@69144
   976
lp15@69144
   977
lemma interior_of_maximal: "\<lbrakk>T \<subseteq> S; openin X T\<rbrakk> \<Longrightarrow> T \<subseteq> X interior_of S"
lp15@69144
   978
  by (auto simp: interior_of_def)
lp15@69144
   979
lp15@69144
   980
lemma interior_of_maximal_eq: "openin X T \<Longrightarrow> T \<subseteq> X interior_of S \<longleftrightarrow> T \<subseteq> S"
lp15@69144
   981
  by (meson interior_of_maximal interior_of_subset order_trans)
lp15@69144
   982
lp15@69144
   983
lemma interior_of_unique:
lp15@69144
   984
   "\<lbrakk>T \<subseteq> S; openin X T; \<And>T'. \<lbrakk>T' \<subseteq> S; openin X T'\<rbrakk> \<Longrightarrow> T' \<subseteq> T\<rbrakk> \<Longrightarrow> X interior_of S = T"
lp15@69144
   985
  by (simp add: interior_of_maximal_eq interior_of_subset subset_antisym)
lp15@69144
   986
lp15@69144
   987
lemma interior_of_subset_topspace: "X interior_of S \<subseteq> topspace X"
lp15@69144
   988
  by (simp add: openin_subset)
lp15@69144
   989
lp15@69144
   990
lemma interior_of_subset_subtopology: "(subtopology X S) interior_of T \<subseteq> S"
lp15@69144
   991
  by (meson openin_imp_subset openin_interior_of)
lp15@69144
   992
lp15@69144
   993
lemma interior_of_Int: "X interior_of (S \<inter> T) = X interior_of S \<inter> X interior_of T"
lp15@69144
   994
  apply (rule equalityI)
lp15@69144
   995
   apply (simp add: interior_of_mono)
lp15@69144
   996
  apply (auto simp: interior_of_maximal_eq openin_Int interior_of_subset le_infI1 le_infI2)
lp15@69144
   997
  done
lp15@69144
   998
lp15@69144
   999
lemma interior_of_Inter_subset: "X interior_of (\<Inter>\<F>) \<subseteq> (\<Inter>S \<in> \<F>. X interior_of S)"
lp15@69144
  1000
  by (simp add: INT_greatest Inf_lower interior_of_mono)
lp15@69144
  1001
lp15@69144
  1002
lemma union_interior_of_subset:
lp15@69144
  1003
   "X interior_of S \<union> X interior_of T \<subseteq> X interior_of (S \<union> T)"
lp15@69144
  1004
  by (simp add: interior_of_mono)
lp15@69144
  1005
lp15@69144
  1006
lemma interior_of_eq_empty:
lp15@69144
  1007
   "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<subseteq> S \<longrightarrow> T = {})"
lp15@69144
  1008
  by (metis bot.extremum_uniqueI interior_of_maximal interior_of_subset openin_interior_of)
lp15@69144
  1009
lp15@69144
  1010
lemma interior_of_eq_empty_alt:
lp15@69144
  1011
   "X interior_of S = {} \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> T - S \<noteq> {})"
lp15@69144
  1012
  by (auto simp: interior_of_eq_empty)
lp15@69144
  1013
lp15@69144
  1014
lemma interior_of_Union_openin_subsets:
lp15@69144
  1015
   "\<Union>{T. openin X T \<and> T \<subseteq> S} = X interior_of S"
lp15@69144
  1016
  by (rule interior_of_unique [symmetric]) auto
lp15@69144
  1017
lp15@69144
  1018
lemma interior_of_complement:
lp15@69144
  1019
   "X interior_of (topspace X - S) = topspace X - X closure_of S"
lp15@69144
  1020
  by (auto simp: interior_of_def closure_of_def)
lp15@69144
  1021
lp15@69144
  1022
lemma interior_of_closure_of:
lp15@69144
  1023
   "X interior_of S = topspace X - X closure_of (topspace X - S)"
lp15@69144
  1024
  unfolding interior_of_complement [symmetric]
lp15@69144
  1025
  by (metis Diff_Diff_Int interior_of_restrict)
lp15@69144
  1026
lp15@69144
  1027
lemma closure_of_interior_of:
lp15@69144
  1028
   "X closure_of S = topspace X - X interior_of (topspace X - S)"
lp15@69144
  1029
  by (simp add: interior_of_complement Diff_Diff_Int closure_of)
lp15@69144
  1030
lp15@69144
  1031
lemma closure_of_complement: "X closure_of (topspace X - S) = topspace X - X interior_of S"
lp15@69144
  1032
  unfolding interior_of_def closure_of_def
lp15@69144
  1033
  by (blast dest: openin_subset)
lp15@69144
  1034
lp15@69144
  1035
lemma interior_of_eq_empty_complement:
lp15@69144
  1036
  "X interior_of S = {} \<longleftrightarrow> X closure_of (topspace X - S) = topspace X"
lp15@69144
  1037
  using interior_of_subset_topspace [of X S] closure_of_complement by fastforce
lp15@69144
  1038
lp15@69144
  1039
lemma closure_of_eq_topspace:
lp15@69144
  1040
   "X closure_of S = topspace X \<longleftrightarrow> X interior_of (topspace X - S) = {}"
lp15@69144
  1041
  using closure_of_subset_topspace [of X S] interior_of_complement by fastforce
lp15@69144
  1042
lp15@69144
  1043
lemma interior_of_subtopology_subset:
lp15@69144
  1044
     "U \<inter> X interior_of S \<subseteq> (subtopology X U) interior_of S"
lp15@69144
  1045
  by (auto simp: interior_of_def openin_subtopology)
lp15@69144
  1046
lp15@69144
  1047
lemma interior_of_subtopology_subsets:
lp15@69144
  1048
   "T \<subseteq> U \<Longrightarrow> T \<inter> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
lp15@69144
  1049
  by (metis inf.absorb_iff2 interior_of_subtopology_subset subtopology_subtopology)
lp15@69144
  1050
lp15@69144
  1051
lemma interior_of_subtopology_mono:
lp15@69144
  1052
   "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X U) interior_of S \<subseteq> (subtopology X T) interior_of S"
lp15@69144
  1053
  by (metis dual_order.trans inf.orderE inf_commute interior_of_subset interior_of_subtopology_subsets)
lp15@69144
  1054
lp15@69144
  1055
lemma interior_of_subtopology_open:
lp15@69144
  1056
  assumes "openin X U"
lp15@69144
  1057
  shows "(subtopology X U) interior_of S = U \<inter> X interior_of S"
lp15@69144
  1058
proof -
lp15@69144
  1059
  have "\<forall>A. U \<inter> X closure_of (U \<inter> A) = U \<inter> X closure_of A"
lp15@69144
  1060
    using assms openin_Int_closure_of_eq by blast
lp15@69144
  1061
  then have "topspace X \<inter> U - U \<inter> X closure_of (topspace X \<inter> U - S) = U \<inter> (topspace X - X closure_of (topspace X - S))"
lp15@69144
  1062
    by (metis (no_types) Diff_Int_distrib Int_Diff inf_commute)
lp15@69144
  1063
  then show ?thesis
lp15@69144
  1064
    unfolding interior_of_closure_of closure_of_subtopology_open topspace_subtopology
lp15@69144
  1065
    using openin_Int_closure_of_eq [OF assms]
lp15@69144
  1066
    by (metis assms closure_of_subtopology_open)
lp15@69144
  1067
qed
lp15@69144
  1068
lp15@69144
  1069
lemma dense_intersects_open:
lp15@69144
  1070
   "X closure_of S = topspace X \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
lp15@69144
  1071
proof -
lp15@69144
  1072
  have "X closure_of S = topspace X \<longleftrightarrow> (topspace X - X interior_of (topspace X - S) = topspace X)"
lp15@69144
  1073
    by (simp add: closure_of_interior_of)
lp15@69144
  1074
  also have "\<dots> \<longleftrightarrow> X interior_of (topspace X - S) = {}"
lp15@69144
  1075
    by (simp add: closure_of_complement interior_of_eq_empty_complement)
lp15@69144
  1076
  also have "\<dots> \<longleftrightarrow> (\<forall>T. openin X T \<and> T \<noteq> {} \<longrightarrow> S \<inter> T \<noteq> {})"
lp15@69144
  1077
    unfolding interior_of_eq_empty_alt
lp15@69144
  1078
    using openin_subset by fastforce
lp15@69144
  1079
  finally show ?thesis .
lp15@69144
  1080
qed
lp15@69144
  1081
lp15@69144
  1082
lemma interior_of_closedin_union_empty_interior_of:
lp15@69144
  1083
  assumes "closedin X S" and disj: "X interior_of T = {}"
lp15@69144
  1084
  shows "X interior_of (S \<union> T) = X interior_of S"
lp15@69144
  1085
proof -
lp15@69144
  1086
  have "X closure_of (topspace X - T) = topspace X"
lp15@69144
  1087
    by (metis Diff_Diff_Int disj closure_of_eq_topspace closure_of_restrict interior_of_closure_of)
lp15@69144
  1088
  then show ?thesis
lp15@69144
  1089
    unfolding interior_of_closure_of
lp15@69144
  1090
    by (metis Diff_Un Diff_subset assms(1) closedin_def closure_of_openin_Int_superset)
lp15@69144
  1091
qed
lp15@69144
  1092
lp15@69144
  1093
lemma interior_of_union_eq_empty:
lp15@69144
  1094
   "closedin X S
lp15@69144
  1095
        \<Longrightarrow> (X interior_of (S \<union> T) = {} \<longleftrightarrow>
lp15@69144
  1096
             X interior_of S = {} \<and> X interior_of T = {})"
lp15@69144
  1097
  by (metis interior_of_closedin_union_empty_interior_of le_sup_iff subset_empty union_interior_of_subset)
lp15@69144
  1098
lp15@69144
  1099
lemma discrete_topology_interior_of [simp]:
lp15@69144
  1100
    "(discrete_topology U) interior_of S = U \<inter> S"
lp15@69144
  1101
  by (simp add: interior_of_restrict [of _ S] interior_of_eq)
lp15@69144
  1102
lp15@69144
  1103
lp15@69144
  1104
subsection \<open>Frontier with respect to topological space \<close>
lp15@69144
  1105
lp15@69144
  1106
definition frontier_of :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixr "frontier'_of" 80)
lp15@69144
  1107
  where "X frontier_of S \<equiv> X closure_of S - X interior_of S"
lp15@69144
  1108
lp15@69144
  1109
lemma frontier_of_closures:
lp15@69144
  1110
     "X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
lp15@69144
  1111
  by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)
lp15@69144
  1112
lp15@69144
  1113
lp15@69144
  1114
lemma interior_of_union_frontier_of [simp]:
lp15@69144
  1115
     "X interior_of S \<union> X frontier_of S = X closure_of S"
lp15@69144
  1116
  by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)
lp15@69144
  1117
lp15@69144
  1118
lemma frontier_of_restrict: "X frontier_of S = X frontier_of (topspace X \<inter> S)"
lp15@69144
  1119
  by (metis closure_of_restrict frontier_of_def interior_of_restrict)
lp15@69144
  1120
lp15@69144
  1121
lemma closedin_frontier_of: "closedin X (X frontier_of S)"
lp15@69144
  1122
  by (simp add: closedin_Int frontier_of_closures)
lp15@69144
  1123
lp15@69144
  1124
lemma frontier_of_subset_topspace: "X frontier_of S \<subseteq> topspace X"
lp15@69144
  1125
  by (simp add: closedin_frontier_of closedin_subset)
lp15@69144
  1126
lp15@69144
  1127
lemma frontier_of_subset_subtopology: "(subtopology X S) frontier_of T \<subseteq> S"
lp15@69144
  1128
  by (metis (no_types) closedin_derived_set closedin_frontier_of)
lp15@69144
  1129
lp15@69144
  1130
lemma frontier_of_subtopology_subset:
lp15@69144
  1131
  "U \<inter> (subtopology X U) frontier_of S \<subseteq> (X frontier_of S)"
lp15@69144
  1132
proof -
lp15@69144
  1133
  have "U \<inter> X interior_of S - subtopology X U interior_of S = {}"
lp15@69144
  1134
    by (simp add: interior_of_subtopology_subset)
lp15@69144
  1135
  moreover have "X closure_of S \<inter> subtopology X U closure_of S = subtopology X U closure_of S"
lp15@69144
  1136
    by (meson closure_of_subtopology_subset inf.absorb_iff2)
lp15@69144
  1137
  ultimately show ?thesis
lp15@69144
  1138
    unfolding frontier_of_def
lp15@69144
  1139
    by blast
lp15@69144
  1140
qed
lp15@69144
  1141
lp15@69144
  1142
lemma frontier_of_subtopology_mono:
lp15@69144
  1143
   "\<lbrakk>S \<subseteq> T; T \<subseteq> U\<rbrakk> \<Longrightarrow> (subtopology X T) frontier_of S \<subseteq> (subtopology X U) frontier_of S"
lp15@69144
  1144
    by (simp add: frontier_of_def Diff_mono closure_of_subtopology_mono interior_of_subtopology_mono)
lp15@69144
  1145
lp15@69144
  1146
lemma clopenin_eq_frontier_of:
lp15@69144
  1147
   "closedin X S \<and> openin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> X frontier_of S = {}"
lp15@69144
  1148
proof (cases "S \<subseteq> topspace X")
lp15@69144
  1149
  case True
lp15@69144
  1150
  then show ?thesis
lp15@69144
  1151
    by (metis Diff_eq_empty_iff closure_of_eq closure_of_subset_eq frontier_of_def interior_of_eq interior_of_subset interior_of_union_frontier_of sup_bot_right)
lp15@69144
  1152
next
lp15@69144
  1153
  case False
lp15@69144
  1154
  then show ?thesis
lp15@69144
  1155
    by (simp add: frontier_of_closures openin_closedin_eq)
lp15@69144
  1156
qed
lp15@69144
  1157
lp15@69144
  1158
lemma frontier_of_eq_empty:
lp15@69144
  1159
     "S \<subseteq> topspace X \<Longrightarrow> (X frontier_of S = {} \<longleftrightarrow> closedin X S \<and> openin X S)"
lp15@69144
  1160
  by (simp add: clopenin_eq_frontier_of)
lp15@69144
  1161
lp15@69144
  1162
lemma frontier_of_openin:
lp15@69144
  1163
     "openin X S \<Longrightarrow> X frontier_of S = X closure_of S - S"
lp15@69144
  1164
  by (metis (no_types) frontier_of_def interior_of_eq)
lp15@69144
  1165
lp15@69144
  1166
lemma frontier_of_openin_straddle_Int:
lp15@69144
  1167
  assumes "openin X U" "U \<inter> X frontier_of S \<noteq> {}"
lp15@69144
  1168
  shows "U \<inter> S \<noteq> {}" "U - S \<noteq> {}"
lp15@69144
  1169
proof -
lp15@69144
  1170
  have "U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}"
lp15@69144
  1171
    using assms by (simp add: frontier_of_closures)
lp15@69144
  1172
  then show "U \<inter> S \<noteq> {}"
lp15@69144
  1173
    using assms openin_Int_closure_of_eq_empty by fastforce
lp15@69144
  1174
  show "U - S \<noteq> {}"
lp15@69144
  1175
  proof -
lp15@69144
  1176
    have "\<exists>A. X closure_of (A - S) \<inter> U \<noteq> {}"
lp15@69144
  1177
      using \<open>U \<inter> (X closure_of S \<inter> X closure_of (topspace X - S)) \<noteq> {}\<close> by blast
lp15@69144
  1178
    then have "\<not> U \<subseteq> S"
lp15@69144
  1179
      by (metis Diff_disjoint Diff_eq_empty_iff Int_Diff assms(1) inf_commute openin_Int_closure_of_eq_empty)
lp15@69144
  1180
    then show ?thesis
lp15@69144
  1181
      by blast
lp15@69144
  1182
  qed
lp15@69144
  1183
qed
lp15@69144
  1184
lp15@69144
  1185
lemma frontier_of_subset_closedin: "closedin X S \<Longrightarrow> (X frontier_of S) \<subseteq> S"
lp15@69144
  1186
  using closure_of_eq frontier_of_def by fastforce
lp15@69144
  1187
lp15@69144
  1188
lemma frontier_of_empty [simp]: "X frontier_of {} = {}"
lp15@69144
  1189
  by (simp add: frontier_of_def)
lp15@69144
  1190
lp15@69144
  1191
lemma frontier_of_topspace [simp]: "X frontier_of topspace X = {}"
lp15@69144
  1192
  by (simp add: frontier_of_def)
lp15@69144
  1193
lp15@69144
  1194
lemma frontier_of_subset_eq:
lp15@69144
  1195
  assumes "S \<subseteq> topspace X"
lp15@69144
  1196
  shows "(X frontier_of S) \<subseteq> S \<longleftrightarrow> closedin X S"
lp15@69144
  1197
proof
lp15@69144
  1198
  show "X frontier_of S \<subseteq> S \<Longrightarrow> closedin X S"
lp15@69144
  1199
    by (metis assms closure_of_subset_eq interior_of_subset interior_of_union_frontier_of le_sup_iff)
lp15@69144
  1200
  show "closedin X S \<Longrightarrow> X frontier_of S \<subseteq> S"
lp15@69144
  1201
    by (simp add: frontier_of_subset_closedin)
lp15@69144
  1202
qed
lp15@69144
  1203
lp15@69144
  1204
lemma frontier_of_complement: "X frontier_of (topspace X - S) = X frontier_of S"
lp15@69144
  1205
  by (metis Diff_Diff_Int closure_of_restrict frontier_of_closures inf_commute)
lp15@69144
  1206
lp15@69144
  1207
lemma frontier_of_disjoint_eq:
lp15@69144
  1208
  assumes "S \<subseteq> topspace X"
lp15@69144
  1209
  shows "((X frontier_of S) \<inter> S = {} \<longleftrightarrow> openin X S)"
lp15@69144
  1210
proof
lp15@69144
  1211
  assume "X frontier_of S \<inter> S = {}"
lp15@69144
  1212
  then have "closedin X (topspace X - S)"
lp15@69144
  1213
    using assms closure_of_subset frontier_of_def interior_of_eq interior_of_subset by fastforce
lp15@69144
  1214
  then show "openin X S"
lp15@69144
  1215
    using assms by (simp add: openin_closedin)
lp15@69144
  1216
next
lp15@69144
  1217
  show "openin X S \<Longrightarrow> X frontier_of S \<inter> S = {}"
lp15@69144
  1218
    by (simp add: Diff_Diff_Int closedin_def frontier_of_openin inf.absorb_iff2 inf_commute)
lp15@69144
  1219
qed
lp15@69144
  1220
lp15@69144
  1221
lemma frontier_of_disjoint_eq_alt:
lp15@69144
  1222
  "S \<subseteq> (topspace X - X frontier_of S) \<longleftrightarrow> openin X S"
lp15@69144
  1223
proof (cases "S \<subseteq> topspace X")
lp15@69144
  1224
  case True
lp15@69144
  1225
  show ?thesis
lp15@69144
  1226
    using True frontier_of_disjoint_eq by auto
lp15@69144
  1227
next
lp15@69144
  1228
  case False
lp15@69144
  1229
  then show ?thesis
lp15@69144
  1230
    by (meson Diff_subset openin_subset subset_trans)
lp15@69144
  1231
qed
lp15@69144
  1232
lp15@69144
  1233
lemma frontier_of_Int:
lp15@69144
  1234
     "X frontier_of (S \<inter> T) =
lp15@69144
  1235
      X closure_of (S \<inter> T) \<inter> (X frontier_of S \<union> X frontier_of T)"
lp15@69144
  1236
proof -
lp15@69144
  1237
  have *: "U \<subseteq> S \<and> U \<subseteq> T \<Longrightarrow> U \<inter> (S \<inter> A \<union> T \<inter> B) = U \<inter> (A \<union> B)" for U S T A B :: "'a set"
lp15@69144
  1238
    by blast
lp15@69144
  1239
  show ?thesis
lp15@69144
  1240
    by (simp add: frontier_of_closures closure_of_mono Diff_Int * flip: closure_of_Un)
lp15@69144
  1241
qed
lp15@69144
  1242
lp15@69144
  1243
lemma frontier_of_Int_subset: "X frontier_of (S \<inter> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
lp15@69144
  1244
  by (simp add: frontier_of_Int)
lp15@69144
  1245
lp15@69144
  1246
lemma frontier_of_Int_closedin:
lp15@69144
  1247
  "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> X frontier_of(S \<inter> T) = X frontier_of S \<inter> T \<union> S \<inter> X frontier_of T"
lp15@69144
  1248
  apply (simp add: frontier_of_Int closedin_Int closure_of_closedin)
lp15@69144
  1249
  using frontier_of_subset_closedin by blast
lp15@69144
  1250
lp15@69144
  1251
lemma frontier_of_Un_subset: "X frontier_of(S \<union> T) \<subseteq> X frontier_of S \<union> X frontier_of T"
lp15@69144
  1252
  by (metis Diff_Un frontier_of_Int_subset frontier_of_complement)
lp15@69144
  1253
lp15@69144
  1254
lemma frontier_of_Union_subset:
lp15@69144
  1255
   "finite \<F> \<Longrightarrow> X frontier_of (\<Union>\<F>) \<subseteq> (\<Union>T \<in> \<F>. X frontier_of T)"
lp15@69144
  1256
proof (induction \<F> rule: finite_induct)
lp15@69144
  1257
  case (insert A \<F>)
lp15@69144
  1258
  then show ?case
lp15@69144
  1259
    using frontier_of_Un_subset by fastforce
lp15@69144
  1260
qed simp
lp15@69144
  1261
lp15@69144
  1262
lemma frontier_of_frontier_of_subset:
lp15@69144
  1263
     "X frontier_of (X frontier_of S) \<subseteq> X frontier_of S"
lp15@69144
  1264
  by (simp add: closedin_frontier_of frontier_of_subset_closedin)
lp15@69144
  1265
lp15@69144
  1266
lemma frontier_of_subtopology_open:
lp15@69144
  1267
     "openin X U \<Longrightarrow> (subtopology X U) frontier_of S = U \<inter> X frontier_of S"
lp15@69144
  1268
  by (simp add: Diff_Int_distrib closure_of_subtopology_open frontier_of_def interior_of_subtopology_open)
lp15@69144
  1269
lp15@69144
  1270
lemma discrete_topology_frontier_of [simp]:
lp15@69144
  1271
     "(discrete_topology U) frontier_of S = {}"
lp15@69144
  1272
  by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
lp15@69144
  1273
lp15@69144
  1274
lp15@69918
  1275
subsection\<open>Locally finite collections\<close>
lp15@69918
  1276
lp15@69918
  1277
definition locally_finite_in
lp15@69918
  1278
  where
lp15@69918
  1279
 "locally_finite_in X \<A> \<longleftrightarrow>
lp15@69918
  1280
        (\<Union>\<A> \<subseteq> topspace X) \<and>
lp15@69918
  1281
        (\<forall>x \<in> topspace X. \<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}})"
lp15@69918
  1282
lp15@69918
  1283
lemma finite_imp_locally_finite_in:
lp15@69918
  1284
   "\<lbrakk>finite \<A>; \<Union>\<A> \<subseteq> topspace X\<rbrakk> \<Longrightarrow> locally_finite_in X \<A>"
lp15@69918
  1285
  by (auto simp: locally_finite_in_def)
lp15@69918
  1286
lp15@69918
  1287
lemma locally_finite_in_subset:
lp15@69918
  1288
  assumes "locally_finite_in X \<A>" "\<B> \<subseteq> \<A>"
lp15@69918
  1289
  shows "locally_finite_in X \<B>"
lp15@69918
  1290
proof -
lp15@69918
  1291
  have "finite {U \<in> \<A>. U \<inter> V \<noteq> {}} \<Longrightarrow> finite {U \<in> \<B>. U \<inter> V \<noteq> {}}" for V
lp15@69918
  1292
    apply (erule rev_finite_subset) using \<open>\<B> \<subseteq> \<A>\<close> by blast
lp15@69918
  1293
  then show ?thesis
lp15@69918
  1294
  using assms unfolding locally_finite_in_def by (fastforce simp add:)
lp15@69918
  1295
qed
lp15@69918
  1296
lp15@69918
  1297
lemma locally_finite_in_refinement:
lp15@69918
  1298
  assumes \<A>: "locally_finite_in X \<A>" and f: "\<And>S. S \<in> \<A> \<Longrightarrow> f S \<subseteq> S"
lp15@69918
  1299
  shows "locally_finite_in X (f ` \<A>)"
lp15@69918
  1300
proof -
lp15@69918
  1301
  show ?thesis
lp15@69918
  1302
    unfolding locally_finite_in_def
lp15@69918
  1303
  proof safe
lp15@69918
  1304
    fix x
lp15@69918
  1305
    assume "x \<in> topspace X"
lp15@69918
  1306
    then obtain V where "openin X V" "x \<in> V" "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1307
      using \<A> unfolding locally_finite_in_def by blast
lp15@69918
  1308
    moreover have "{U \<in> \<A>. f U \<inter> V \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}" for V
lp15@69918
  1309
      using f by blast
lp15@69918
  1310
    ultimately have "finite {U \<in> \<A>. f U \<inter> V \<noteq> {}}"
lp15@69918
  1311
      using finite_subset by blast
lp15@69918
  1312
    moreover have "f ` {U \<in> \<A>. f U \<inter> V \<noteq> {}} = {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1313
      by blast
lp15@69918
  1314
    ultimately have "finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1315
      by (metis (no_types, lifting) finite_imageI)
lp15@69918
  1316
    then show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> f ` \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1317
      using \<open>openin X V\<close> \<open>x \<in> V\<close> by blast
lp15@69918
  1318
  next
lp15@69918
  1319
    show "\<And>x xa. \<lbrakk>xa \<in> \<A>; x \<in> f xa\<rbrakk> \<Longrightarrow> x \<in> topspace X"
lp15@69918
  1320
      by (meson Sup_upper \<A> f locally_finite_in_def subset_iff)
lp15@69918
  1321
  qed
lp15@69918
  1322
qed
lp15@69918
  1323
lp15@69918
  1324
lemma locally_finite_in_subtopology:
lp15@69918
  1325
  assumes \<A>: "locally_finite_in X \<A>" "\<Union>\<A> \<subseteq> S"
lp15@69918
  1326
  shows "locally_finite_in (subtopology X S) \<A>"
lp15@69918
  1327
  unfolding locally_finite_in_def
lp15@69918
  1328
proof safe
lp15@69918
  1329
  fix x
lp15@69918
  1330
  assume x: "x \<in> topspace (subtopology X S)"
lp15@69918
  1331
  then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1332
    using \<A> unfolding locally_finite_in_def topspace_subtopology by blast
lp15@69918
  1333
  show "\<exists>V. openin (subtopology X S) V \<and> x \<in> V \<and> finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1334
  proof (intro exI conjI)
lp15@69918
  1335
    show "openin (subtopology X S) (S \<inter> V)"
lp15@69918
  1336
      by (simp add: \<open>openin X V\<close> openin_subtopology_Int2)
lp15@69918
  1337
    have "{U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}} \<subseteq> {U \<in> \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1338
      by auto
lp15@69918
  1339
    with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
lp15@69918
  1340
      using finite_subset by auto
lp15@69918
  1341
    show "x \<in> S \<inter> V"
lp15@69918
  1342
      using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
lp15@69918
  1343
  qed
lp15@69918
  1344
next
lp15@69918
  1345
  show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
lp15@69918
  1346
    using assms unfolding locally_finite_in_def topspace_subtopology by blast
lp15@69918
  1347
qed
lp15@69918
  1348
lp15@69918
  1349
lp15@69918
  1350
lemma closedin_locally_finite_Union:
lp15@69918
  1351
  assumes clo: "\<And>S. S \<in> \<A> \<Longrightarrow> closedin X S" and \<A>: "locally_finite_in X \<A>"
lp15@69918
  1352
  shows "closedin X (\<Union>\<A>)"
lp15@69918
  1353
  using \<A> unfolding locally_finite_in_def closedin_def
lp15@69918
  1354
proof clarify
lp15@69918
  1355
  show "openin X (topspace X - \<Union>\<A>)"
lp15@69918
  1356
  proof (subst openin_subopen, clarify)
lp15@69918
  1357
    fix x
lp15@69918
  1358
    assume "x \<in> topspace X" and "x \<notin> \<Union>\<A>"
lp15@69918
  1359
    then obtain V where "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1360
      using \<A> unfolding locally_finite_in_def by blast
lp15@69918
  1361
    let ?T = "V - \<Union>{S \<in> \<A>. S \<inter> V \<noteq> {}}"
lp15@69918
  1362
    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> topspace X - \<Union>\<A>"
lp15@69918
  1363
    proof (intro exI conjI)
lp15@69918
  1364
      show "openin X ?T"
lp15@69918
  1365
        by (metis (no_types, lifting) fin \<open>openin X V\<close> clo closedin_Union mem_Collect_eq openin_diff)
lp15@69918
  1366
      show "x \<in> ?T"
lp15@69918
  1367
        using \<open>x \<notin> \<Union>\<A>\<close> \<open>x \<in> V\<close> by auto
lp15@69918
  1368
      show "?T \<subseteq> topspace X - \<Union>\<A>"
lp15@69918
  1369
        using \<open>openin X V\<close> openin_subset by auto
lp15@69918
  1370
    qed
lp15@69918
  1371
  qed
lp15@69918
  1372
qed
lp15@69918
  1373
lp15@69918
  1374
lemma locally_finite_in_closure:
lp15@69918
  1375
  assumes \<A>: "locally_finite_in X \<A>"
lp15@69918
  1376
  shows "locally_finite_in X ((\<lambda>S. X closure_of S) ` \<A>)"
lp15@69918
  1377
  using \<A> unfolding locally_finite_in_def
lp15@69918
  1378
proof (intro conjI; clarsimp)
lp15@69918
  1379
  fix x A
lp15@69918
  1380
  assume "x \<in> X closure_of A"
lp15@69918
  1381
  then show "x \<in> topspace X"
lp15@69918
  1382
    by (meson in_closure_of)
lp15@69918
  1383
next
lp15@69918
  1384
  fix x
lp15@69918
  1385
  assume "x \<in> topspace X" and "\<Union>\<A> \<subseteq> topspace X"
lp15@69918
  1386
  then obtain V where V: "openin X V" "x \<in> V" and fin: "finite {U \<in> \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1387
    using \<A> unfolding locally_finite_in_def by blast
lp15@69918
  1388
  have eq: "{y \<in> f ` \<A>. Q y} = f ` {x. x \<in> \<A> \<and> Q(f x)}" for f Q
lp15@69918
  1389
    by blast
lp15@69918
  1390
  have eq2: "{A \<in> \<A>. X closure_of A \<inter> V \<noteq> {}} = {A \<in> \<A>. A \<inter> V \<noteq> {}}"
lp15@69918
  1391
    using openin_Int_closure_of_eq_empty V  by blast
lp15@69918
  1392
  have "finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1393
    by (simp add: eq eq2 fin)
lp15@69918
  1394
  with V show "\<exists>V. openin X V \<and> x \<in> V \<and> finite {U \<in> (closure_of) X ` \<A>. U \<inter> V \<noteq> {}}"
lp15@69918
  1395
    by blast
lp15@69918
  1396
qed
lp15@69918
  1397
lp15@69918
  1398
lemma closedin_Union_locally_finite_closure:
lp15@69918
  1399
   "locally_finite_in X \<A> \<Longrightarrow> closedin X (\<Union>((\<lambda>S. X closure_of S) ` \<A>))"
lp15@69918
  1400
  by (metis (mono_tags) closedin_closure_of closedin_locally_finite_Union imageE locally_finite_in_closure)
lp15@69918
  1401
lp15@69918
  1402
lemma closure_of_Union_subset: "\<Union>((\<lambda>S. X closure_of S) ` \<A>) \<subseteq> X closure_of (\<Union>\<A>)"
lp15@69918
  1403
  by clarify (meson Union_upper closure_of_mono subsetD)
lp15@69918
  1404
lp15@69918
  1405
lemma closure_of_locally_finite_Union:
lp15@69918
  1406
   "locally_finite_in X \<A> \<Longrightarrow> X closure_of (\<Union>\<A>) = \<Union>((\<lambda>S. X closure_of S) ` \<A>)"
lp15@69918
  1407
  apply (rule closure_of_unique)
lp15@69918
  1408
  apply (simp add: SUP_upper2 Sup_le_iff closure_of_subset locally_finite_in_def)
lp15@69918
  1409
  apply (simp add: closedin_Union_locally_finite_closure)
lp15@69918
  1410
  by (simp add: Sup_le_iff closure_of_minimal)
lp15@69918
  1411
lp15@69918
  1412
lp15@69939
  1413
subsection%important \<open>Continuous maps\<close>
lp15@69939
  1414
lp15@69939
  1415
text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
lp15@69939
  1416
of type classes, as defined below.\<close>
lp15@69144
  1417
lp15@69144
  1418
definition continuous_map where
lp15@69144
  1419
  "continuous_map X Y f \<equiv>
lp15@69144
  1420
     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
lp15@69144
  1421
     (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
lp15@69144
  1422
lp15@69144
  1423
lemma continuous_map:
lp15@69144
  1424
   "continuous_map X Y f \<longleftrightarrow>
lp15@69144
  1425
        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U})"
lp15@69144
  1426
  by (auto simp: continuous_map_def)
lp15@69144
  1427
lp15@69144
  1428
lemma continuous_map_image_subset_topspace:
lp15@69144
  1429
   "continuous_map X Y f \<Longrightarrow> f ` (topspace X) \<subseteq> topspace Y"
lp15@69144
  1430
  by (auto simp: continuous_map_def)
lp15@69144
  1431
lp15@69144
  1432
lemma continuous_map_on_empty: "topspace X = {} \<Longrightarrow> continuous_map X Y f"
lp15@69144
  1433
  by (auto simp: continuous_map_def)
lp15@69144
  1434
lp15@69144
  1435
lemma continuous_map_closedin:
lp15@69144
  1436
   "continuous_map X Y f \<longleftrightarrow>
lp15@69144
  1437
         (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
lp15@69144
  1438
         (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
lp15@69144
  1439
proof -
lp15@69144
  1440
  have "(\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}) =
lp15@69144
  1441
        (\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C})"
lp15@69144
  1442
    if "\<And>x. x \<in> topspace X \<Longrightarrow> f x \<in> topspace Y"
lp15@69144
  1443
  proof -
lp15@69144
  1444
    have eq: "{x \<in> topspace X. f x \<in> topspace Y \<and> f x \<notin> C} = (topspace X - {x \<in> topspace X. f x \<in> C})" for C
lp15@69144
  1445
      using that by blast
lp15@69144
  1446
    show ?thesis
lp15@69144
  1447
    proof (intro iffI allI impI)
lp15@69144
  1448
      fix C
lp15@69144
  1449
      assume "\<forall>U. openin Y U \<longrightarrow> openin X {x \<in> topspace X. f x \<in> U}" and "closedin Y C"
lp15@69144
  1450
      then have "openin X {x \<in> topspace X. f x \<in> topspace Y - C}" by blast
lp15@69144
  1451
      then show "closedin X {x \<in> topspace X. f x \<in> C}"
lp15@69144
  1452
        by (auto simp add: closedin_def eq)
lp15@69144
  1453
    next
lp15@69144
  1454
      fix U
lp15@69144
  1455
      assume "\<forall>C. closedin Y C \<longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}" and "openin Y U"
lp15@69144
  1456
      then have "closedin X {x \<in> topspace X. f x \<in> topspace Y - U}" by blast
lp15@69144
  1457
      then show "openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  1458
        by (auto simp add: openin_closedin_eq eq)
lp15@69144
  1459
    qed
lp15@69144
  1460
  qed
lp15@69144
  1461
  then show ?thesis
lp15@69144
  1462
    by (auto simp: continuous_map_def)
lp15@69144
  1463
qed
lp15@69144
  1464
lp15@69144
  1465
lemma openin_continuous_map_preimage:
lp15@69144
  1466
   "\<lbrakk>continuous_map X Y f; openin Y U\<rbrakk> \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  1467
  by (simp add: continuous_map_def)
lp15@69144
  1468
lp15@69144
  1469
lemma closedin_continuous_map_preimage:
lp15@69144
  1470
   "\<lbrakk>continuous_map X Y f; closedin Y C\<rbrakk> \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> C}"
lp15@69144
  1471
  by (simp add: continuous_map_closedin)
lp15@69144
  1472
lp15@69144
  1473
lemma openin_continuous_map_preimage_gen:
lp15@69144
  1474
  assumes "continuous_map X Y f" "openin X U" "openin Y V"
lp15@69144
  1475
  shows "openin X {x \<in> U. f x \<in> V}"
lp15@69144
  1476
proof -
lp15@69144
  1477
  have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
lp15@69144
  1478
    using assms(2) openin_closedin_eq by fastforce
lp15@69144
  1479
  show ?thesis
lp15@69144
  1480
    unfolding eq
lp15@69144
  1481
    using assms openin_continuous_map_preimage by fastforce
lp15@69144
  1482
qed
lp15@69144
  1483
lp15@69144
  1484
lemma closedin_continuous_map_preimage_gen:
lp15@69144
  1485
  assumes "continuous_map X Y f" "closedin X U" "closedin Y V"
lp15@69144
  1486
  shows "closedin X {x \<in> U. f x \<in> V}"
lp15@69144
  1487
proof -
lp15@69144
  1488
  have eq: "{x \<in> U. f x \<in> V} = U \<inter> {x \<in> topspace X. f x \<in> V}"
lp15@69144
  1489
    using assms(2) closedin_def by fastforce
lp15@69144
  1490
  show ?thesis
lp15@69144
  1491
    unfolding eq
lp15@69144
  1492
    using assms closedin_continuous_map_preimage by fastforce
lp15@69144
  1493
qed
lp15@69144
  1494
lp15@69144
  1495
lemma continuous_map_image_closure_subset:
lp15@69144
  1496
  assumes "continuous_map X Y f"
lp15@69144
  1497
  shows "f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
lp15@69144
  1498
proof -
lp15@69144
  1499
  have *: "f ` (topspace X) \<subseteq> topspace Y"
lp15@69144
  1500
    by (meson assms continuous_map)
lp15@69144
  1501
  have "X closure_of T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of (f ` T)}" if "T \<subseteq> topspace X" for T
lp15@69144
  1502
  proof (rule closure_of_minimal)
lp15@69144
  1503
    show "T \<subseteq> {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
lp15@69144
  1504
      using closure_of_subset * that  by (fastforce simp: in_closure_of)
lp15@69144
  1505
  next
lp15@69144
  1506
    show "closedin X {x \<in> X closure_of T. f x \<in> Y closure_of f ` T}"
lp15@69144
  1507
      using assms closedin_continuous_map_preimage_gen by fastforce
lp15@69144
  1508
  qed
lp15@69144
  1509
  then have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (f ` (topspace X \<inter> S))"
lp15@69144
  1510
    by blast
lp15@69144
  1511
  also have "\<dots> \<subseteq> Y closure_of (topspace Y \<inter> f ` S)"
lp15@69144
  1512
    using * by (blast intro!: closure_of_mono)
lp15@69144
  1513
  finally have "f ` (X closure_of (topspace X \<inter> S)) \<subseteq> Y closure_of (topspace Y \<inter> f ` S)" .
lp15@69144
  1514
  then show ?thesis
lp15@69144
  1515
    by (metis closure_of_restrict)
lp15@69144
  1516
qed
lp15@69144
  1517
lp15@69144
  1518
lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
lp15@69144
  1519
       (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
lp15@69144
  1520
  using continuous_map_image_closure_subset by blast
lp15@69144
  1521
lp15@69144
  1522
lemma continuous_map_subset_aux2:
lp15@69144
  1523
  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
lp15@69144
  1524
  shows "continuous_map X Y f"
lp15@69144
  1525
  unfolding continuous_map_closedin
lp15@69144
  1526
proof (intro conjI ballI allI impI)
lp15@69144
  1527
  fix x
lp15@69144
  1528
  assume "x \<in> topspace X"
lp15@69144
  1529
  then show "f x \<in> topspace Y"
lp15@69144
  1530
    using assms closure_of_subset_topspace by fastforce
lp15@69144
  1531
next
lp15@69144
  1532
  fix C
lp15@69144
  1533
  assume "closedin Y C"
lp15@69144
  1534
  then show "closedin X {x \<in> topspace X. f x \<in> C}"
lp15@69144
  1535
  proof (clarsimp simp flip: closure_of_subset_eq, intro conjI)
lp15@69144
  1536
    fix x
lp15@69144
  1537
    assume x: "x \<in> X closure_of {x \<in> topspace X. f x \<in> C}"
lp15@69144
  1538
      and "C \<subseteq> topspace Y" and "Y closure_of C \<subseteq> C"
lp15@69144
  1539
    show "x \<in> topspace X"
lp15@69144
  1540
      by (meson x in_closure_of)
lp15@69144
  1541
    have "{a \<in> topspace X. f a \<in> C} \<subseteq> topspace X"
lp15@69144
  1542
      by simp
lp15@69144
  1543
    moreover have "Y closure_of f ` {a \<in> topspace X. f a \<in> C} \<subseteq> C"
lp15@69144
  1544
      by (simp add: \<open>closedin Y C\<close> closure_of_minimal image_subset_iff)
lp15@69144
  1545
    ultimately have "f ` (X closure_of {a \<in> topspace X. f a \<in> C}) \<subseteq> C"
lp15@69144
  1546
      using assms by blast
lp15@69144
  1547
    then show "f x \<in> C"
lp15@69144
  1548
      using x by auto
lp15@69144
  1549
  qed
lp15@69144
  1550
qed
lp15@69144
  1551
lp15@69144
  1552
lemma continuous_map_eq_image_closure_subset:
lp15@69144
  1553
     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
lp15@69144
  1554
  using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
lp15@69144
  1555
lp15@69144
  1556
lemma continuous_map_eq_image_closure_subset_alt:
lp15@69144
  1557
     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
lp15@69144
  1558
  using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
lp15@69144
  1559
lp15@69144
  1560
lemma continuous_map_eq_image_closure_subset_gen:
lp15@69144
  1561
     "continuous_map X Y f \<longleftrightarrow>
lp15@69144
  1562
        f ` (topspace X) \<subseteq> topspace Y \<and>
lp15@69144
  1563
        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
lp15@69144
  1564
  using continuous_map_subset_aux1 continuous_map_subset_aux2 continuous_map_image_subset_topspace by metis
lp15@69144
  1565
lp15@69144
  1566
lemma continuous_map_closure_preimage_subset:
lp15@69144
  1567
   "continuous_map X Y f
lp15@69144
  1568
        \<Longrightarrow> X closure_of {x \<in> topspace X. f x \<in> T}
lp15@69144
  1569
            \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
lp15@69144
  1570
  unfolding continuous_map_closedin
lp15@69144
  1571
  by (rule closure_of_minimal) (use in_closure_of in \<open>fastforce+\<close>)
lp15@69144
  1572
lp15@69144
  1573
lp15@69144
  1574
lemma continuous_map_frontier_frontier_preimage_subset:
lp15@69144
  1575
  assumes "continuous_map X Y f"
lp15@69144
  1576
  shows "X frontier_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y frontier_of T}"
lp15@69144
  1577
proof -
lp15@69144
  1578
  have eq: "topspace X - {x \<in> topspace X. f x \<in> T} = {x \<in> topspace X. f x \<in> topspace Y - T}"
lp15@69144
  1579
    using assms unfolding continuous_map_def by blast
lp15@69144
  1580
  have "X closure_of {x \<in> topspace X. f x \<in> T} \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of T}"
lp15@69144
  1581
    by (simp add: assms continuous_map_closure_preimage_subset)
lp15@69144
  1582
  moreover
lp15@69144
  1583
  have "X closure_of (topspace X - {x \<in> topspace X. f x \<in> T}) \<subseteq> {x \<in> topspace X. f x \<in> Y closure_of (topspace Y - T)}"
lp15@69144
  1584
    using continuous_map_closure_preimage_subset [OF assms] eq by presburger
lp15@69144
  1585
  ultimately show ?thesis
lp15@69144
  1586
    by (auto simp: frontier_of_closures)
lp15@69144
  1587
qed
lp15@69144
  1588
lp15@69144
  1589
lemma topology_finer_continuous_id:
lp15@69144
  1590
  "topspace X = topspace Y \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> continuous_map Y X id)"
lp15@69144
  1591
  unfolding continuous_map_def
lp15@69144
  1592
  apply auto
lp15@69144
  1593
  using openin_subopen openin_subset apply fastforce
lp15@69144
  1594
  using openin_subopen topspace_def by fastforce
lp15@69144
  1595
lp15@69144
  1596
lemma continuous_map_const [simp]:
lp15@69144
  1597
   "continuous_map X Y (\<lambda>x. C) \<longleftrightarrow> topspace X = {} \<or> C \<in> topspace Y"
lp15@69144
  1598
proof (cases "topspace X = {}")
lp15@69144
  1599
  case False
lp15@69144
  1600
  show ?thesis
lp15@69144
  1601
  proof (cases "C \<in> topspace Y")
lp15@69144
  1602
    case True
lp15@69144
  1603
    with openin_subopen show ?thesis
lp15@69144
  1604
      by (auto simp: continuous_map_def)
lp15@69144
  1605
  next
lp15@69144
  1606
    case False
lp15@69144
  1607
    then show ?thesis
lp15@69144
  1608
      unfolding continuous_map_def by fastforce
lp15@69144
  1609
  qed
lp15@69144
  1610
qed (auto simp: continuous_map_on_empty)
lp15@69144
  1611
lp15@69144
  1612
lemma continuous_map_compose:
lp15@69144
  1613
  assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g"
lp15@69144
  1614
  shows "continuous_map X X'' (g \<circ> f)"
lp15@69144
  1615
  unfolding continuous_map_def
lp15@69144
  1616
proof (intro conjI ballI allI impI)
lp15@69144
  1617
  fix x
lp15@69144
  1618
  assume "x \<in> topspace X"
lp15@69144
  1619
  then show "(g \<circ> f) x \<in> topspace X''"
lp15@69144
  1620
    using assms unfolding continuous_map_def by force
lp15@69144
  1621
next
lp15@69144
  1622
  fix U
lp15@69144
  1623
  assume "openin X'' U"
lp15@69144
  1624
  have eq: "{x \<in> topspace X. (g \<circ> f) x \<in> U} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U}}"
lp15@69144
  1625
    by auto (meson f continuous_map_def)
lp15@69144
  1626
  show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U}"
lp15@69144
  1627
    unfolding eq
lp15@69144
  1628
    using assms unfolding continuous_map_def
lp15@69144
  1629
    using \<open>openin X'' U\<close> by blast
lp15@69144
  1630
qed
lp15@69144
  1631
lp15@69144
  1632
lemma continuous_map_eq:
lp15@69144
  1633
  assumes "continuous_map X X' f" and "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x" shows "continuous_map X X' g"
lp15@69144
  1634
proof -
lp15@69144
  1635
  have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
lp15@69144
  1636
    using assms by auto
lp15@69144
  1637
  show ?thesis
lp15@69144
  1638
    using assms by (simp add: continuous_map_def eq)
lp15@69144
  1639
qed
lp15@69144
  1640
lp15@69144
  1641
lemma restrict_continuous_map [simp]:
lp15@69144
  1642
     "topspace X \<subseteq> S \<Longrightarrow> continuous_map X X' (restrict f S) \<longleftrightarrow> continuous_map X X' f"
lp15@69144
  1643
  by (auto simp: elim!: continuous_map_eq)
lp15@69144
  1644
lp15@69144
  1645
lemma continuous_map_in_subtopology:
lp15@69144
  1646
  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
lp15@69144
  1647
  (is "?lhs = ?rhs")
lp15@69144
  1648
proof
lp15@69144
  1649
  assume L: ?lhs
lp15@69144
  1650
  show ?rhs
lp15@69144
  1651
  proof -
lp15@69144
  1652
    have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
lp15@69144
  1653
      by (meson L continuous_map_image_closure_subset)
lp15@69144
  1654
    then show ?thesis
lp15@69144
  1655
      by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset dual_order.trans)
lp15@69144
  1656
  qed
lp15@69144
  1657
next
lp15@69144
  1658
  assume R: ?rhs
lp15@69144
  1659
  then have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. f x \<in> U \<and> f x \<in> S}" for U
lp15@69144
  1660
    by auto
lp15@69144
  1661
  show ?lhs
lp15@69144
  1662
    using R
lp15@69144
  1663
    unfolding continuous_map
lp15@69144
  1664
    by (auto simp: topspace_subtopology openin_subtopology eq)
lp15@69144
  1665
qed
lp15@69144
  1666
lp15@69144
  1667
lp15@69144
  1668
lemma continuous_map_from_subtopology:
lp15@69144
  1669
     "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
lp15@69144
  1670
  by (auto simp: continuous_map topspace_subtopology openin_subtopology)
lp15@69144
  1671
lp15@69144
  1672
lemma continuous_map_into_fulltopology:
lp15@69144
  1673
   "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
lp15@69144
  1674
  by (auto simp: continuous_map_in_subtopology)
lp15@69144
  1675
lp15@69144
  1676
lemma continuous_map_into_subtopology:
lp15@69144
  1677
   "\<lbrakk>continuous_map X X' f; f ` topspace X \<subseteq> T\<rbrakk> \<Longrightarrow> continuous_map X (subtopology X' T) f"
lp15@69144
  1678
  by (auto simp: continuous_map_in_subtopology)
lp15@69144
  1679
lp15@69144
  1680
lemma continuous_map_from_subtopology_mono:
lp15@69144
  1681
     "\<lbrakk>continuous_map (subtopology X T) X' f; S \<subseteq> T\<rbrakk>
lp15@69144
  1682
      \<Longrightarrow> continuous_map (subtopology X S) X' f"
lp15@69144
  1683
  by (metis inf.absorb_iff2 continuous_map_from_subtopology subtopology_subtopology)
lp15@69144
  1684
lp15@69144
  1685
lemma continuous_map_from_discrete_topology [simp]:
lp15@69144
  1686
  "continuous_map (discrete_topology U) X f \<longleftrightarrow> f ` U \<subseteq> topspace X"
lp15@69144
  1687
  by (auto simp: continuous_map_def)
lp15@69144
  1688
lp15@69922
  1689
lemma continuous_map_iff_continuous [simp]: "continuous_map (subtopology euclidean S) euclidean g = continuous_on S g"
lp15@69922
  1690
  by (fastforce simp add: continuous_map openin_subtopology continuous_on_open_invariant)
lp15@69922
  1691
lp15@69922
  1692
lemma continuous_map_iff_continuous2 [simp]: "continuous_map euclidean euclidean g = continuous_on UNIV g"
lp15@69922
  1693
  by (metis continuous_map_iff_continuous subtopology_UNIV)
lp15@69874
  1694
lp15@69874
  1695
lemma continuous_map_openin_preimage_eq:
lp15@69874
  1696
   "continuous_map X Y f \<longleftrightarrow>
lp15@69874
  1697
        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
lp15@69874
  1698
  by (auto simp: continuous_map_def vimage_def Int_def)
lp15@69874
  1699
lp15@69874
  1700
lemma continuous_map_closedin_preimage_eq:
lp15@69874
  1701
   "continuous_map X Y f \<longleftrightarrow>
lp15@69874
  1702
        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
lp15@69874
  1703
  by (auto simp: continuous_map_closedin vimage_def Int_def)
lp15@69874
  1704
lp15@69874
  1705
lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt"
lp15@69874
  1706
  by (simp add: continuous_at_imp_continuous_on isCont_real_sqrt)
lp15@69874
  1707
lp15@69874
  1708
lemma continuous_map_sqrt [continuous_intros]:
lp15@69874
  1709
   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
lp15@69874
  1710
  by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)
lp15@69874
  1711
lp15@69710
  1712
lemma continuous_map_id [simp]: "continuous_map X X id"
lp15@69710
  1713
  unfolding continuous_map_def  using openin_subopen topspace_def by fastforce
lp15@69710
  1714
lp15@69710
  1715
declare continuous_map_id [unfolded id_def, simp]
lp15@69710
  1716
lp15@69710
  1717
lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id"
lp15@69710
  1718
  by (simp add: continuous_map_from_subtopology)
lp15@69710
  1719
lp15@69710
  1720
declare continuous_map_id_subt [unfolded id_def, simp]
lp15@69710
  1721
lp15@69144
  1722
lp15@69939
  1723
lemma%important continuous_map_alt:
lp15@69939
  1724
   "continuous_map T1 T2 f 
lp15@69939
  1725
    = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
lp15@69939
  1726
  by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
lp15@69939
  1727
lp15@69939
  1728
lemma continuous_map_open [intro]:
lp15@69939
  1729
  "continuous_map T1 T2 f \<Longrightarrow> openin T2 U \<Longrightarrow> openin T1 (f-`U \<inter> topspace(T1))"
lp15@69939
  1730
  unfolding continuous_map_alt by auto
lp15@69939
  1731
lp15@69939
  1732
lemma continuous_map_preimage_topspace [intro]:
lp15@69939
  1733
  assumes "continuous_map T1 T2 f"
lp15@69939
  1734
  shows "f-`(topspace T2) \<inter> topspace T1 = topspace T1"
lp15@69939
  1735
using assms unfolding continuous_map_def by auto
lp15@69939
  1736
lp15@69939
  1737
lp15@69939
  1738
lp15@69144
  1739
subsection\<open>Open and closed maps (not a priori assumed continuous)\<close>
lp15@69144
  1740
lp15@69144
  1741
definition open_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
lp15@69144
  1742
  where "open_map X1 X2 f \<equiv> \<forall>U. openin X1 U \<longrightarrow> openin X2 (f ` U)"
lp15@69144
  1743
lp15@69144
  1744
definition closed_map :: "'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
lp15@69144
  1745
  where "closed_map X1 X2 f \<equiv> \<forall>U. closedin X1 U \<longrightarrow> closedin X2 (f ` U)"
lp15@69144
  1746
lp15@69144
  1747
lemma open_map_imp_subset_topspace:
lp15@69144
  1748
     "open_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
lp15@69144
  1749
  unfolding open_map_def by (simp add: openin_subset)
lp15@69144
  1750
lp15@69144
  1751
lemma open_map_imp_subset:
lp15@69144
  1752
    "\<lbrakk>open_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
lp15@69144
  1753
  by (meson order_trans open_map_imp_subset_topspace subset_image_iff)
lp15@69144
  1754
lp15@69144
  1755
lemma topology_finer_open_id:
lp15@69144
  1756
     "(\<forall>S. openin X S \<longrightarrow> openin X' S) \<longleftrightarrow> open_map X X' id"
lp15@69144
  1757
  unfolding open_map_def by auto
lp15@69144
  1758
lp15@69144
  1759
lemma open_map_id: "open_map X X id"
lp15@69144
  1760
  unfolding open_map_def by auto
lp15@69144
  1761
lp15@69144
  1762
lemma open_map_eq:
lp15@69144
  1763
     "\<lbrakk>open_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> open_map X X' g"
lp15@69144
  1764
  unfolding open_map_def
lp15@69144
  1765
  by (metis image_cong openin_subset subset_iff)
lp15@69144
  1766
lp15@69144
  1767
lemma open_map_inclusion_eq:
lp15@69144
  1768
  "open_map (subtopology X S) X id \<longleftrightarrow> openin X (topspace X \<inter> S)"
lp15@69144
  1769
proof -
lp15@69144
  1770
  have *: "openin X (T \<inter> S)" if "openin X (S \<inter> topspace X)" "openin X T" for T
lp15@69144
  1771
  proof -
lp15@69144
  1772
    have "T \<subseteq> topspace X"
lp15@69144
  1773
      using that by (simp add: openin_subset)
lp15@69144
  1774
    with that show "openin X (T \<inter> S)"
lp15@69144
  1775
      by (metis inf.absorb1 inf.left_commute inf_commute openin_Int)
lp15@69144
  1776
  qed
lp15@69144
  1777
  show ?thesis
lp15@69144
  1778
    by (fastforce simp add: open_map_def Int_commute openin_subtopology_alt intro: *)
lp15@69144
  1779
qed
lp15@69144
  1780
lp15@69144
  1781
lemma open_map_inclusion:
lp15@69144
  1782
     "openin X S \<Longrightarrow> open_map (subtopology X S) X id"
lp15@69144
  1783
  by (simp add: open_map_inclusion_eq openin_Int)
lp15@69144
  1784
lp15@69144
  1785
lemma open_map_compose:
lp15@69144
  1786
     "\<lbrakk>open_map X X' f; open_map X' X'' g\<rbrakk> \<Longrightarrow> open_map X X'' (g \<circ> f)"
lp15@69144
  1787
  by (metis (no_types, lifting) image_comp open_map_def)
lp15@69144
  1788
lp15@69144
  1789
lemma closed_map_imp_subset_topspace:
lp15@69144
  1790
     "closed_map X1 X2 f \<Longrightarrow> f ` (topspace X1) \<subseteq> topspace X2"
lp15@69144
  1791
  by (simp add: closed_map_def closedin_subset)
lp15@69144
  1792
lp15@69144
  1793
lemma closed_map_imp_subset:
lp15@69144
  1794
     "\<lbrakk>closed_map X1 X2 f; S \<subseteq> topspace X1\<rbrakk> \<Longrightarrow> f ` S \<subseteq> topspace X2"
lp15@69144
  1795
  using closed_map_imp_subset_topspace by blast
lp15@69144
  1796
lp15@69144
  1797
lemma topology_finer_closed_id:
lp15@69144
  1798
    "(\<forall>S. closedin X S \<longrightarrow> closedin X' S) \<longleftrightarrow> closed_map X X' id"
lp15@69144
  1799
  by (simp add: closed_map_def)
lp15@69144
  1800
lp15@69144
  1801
lemma closed_map_id: "closed_map X X id"
lp15@69144
  1802
  by (simp add: closed_map_def)
lp15@69144
  1803
lp15@69144
  1804
lemma closed_map_eq:
lp15@69144
  1805
   "\<lbrakk>closed_map X X' f; \<And>x. x \<in> topspace X \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> closed_map X X' g"
lp15@69144
  1806
  unfolding closed_map_def
lp15@69144
  1807
  by (metis image_cong closedin_subset subset_iff)
lp15@69144
  1808
lp15@69144
  1809
lemma closed_map_compose:
lp15@69144
  1810
    "\<lbrakk>closed_map X X' f; closed_map X' X'' g\<rbrakk> \<Longrightarrow> closed_map X X'' (g \<circ> f)"
lp15@69144
  1811
  by (metis (no_types, lifting) closed_map_def image_comp)
lp15@69144
  1812
lp15@69144
  1813
lemma closed_map_inclusion_eq:
lp15@69144
  1814
   "closed_map (subtopology X S) X id \<longleftrightarrow>
lp15@69144
  1815
        closedin X (topspace X \<inter> S)"
lp15@69144
  1816
proof -
lp15@69144
  1817
  have *: "closedin X (T \<inter> S)" if "closedin X (S \<inter> topspace X)" "closedin X T" for T
lp15@69144
  1818
  proof -
lp15@69144
  1819
    have "T \<subseteq> topspace X"
lp15@69144
  1820
      using that by (simp add: closedin_subset)
lp15@69144
  1821
    with that show "closedin X (T \<inter> S)"
lp15@69144
  1822
      by (metis inf.absorb1 inf.left_commute inf_commute closedin_Int)
lp15@69144
  1823
  qed
lp15@69144
  1824
  show ?thesis
lp15@69144
  1825
    by (fastforce simp add: closed_map_def Int_commute closedin_subtopology_alt intro: *)
lp15@69144
  1826
qed
lp15@69144
  1827
lp15@69144
  1828
lemma closed_map_inclusion: "closedin X S \<Longrightarrow> closed_map (subtopology X S) X id"
lp15@69144
  1829
  by (simp add: closed_map_inclusion_eq closedin_Int)
lp15@69144
  1830
lp15@69144
  1831
lemma open_map_into_subtopology:
lp15@69144
  1832
    "\<lbrakk>open_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> open_map X (subtopology X' S) f"
lp15@69144
  1833
  unfolding open_map_def openin_subtopology
lp15@69144
  1834
  using openin_subset by fastforce
lp15@69144
  1835
lp15@69144
  1836
lemma closed_map_into_subtopology:
lp15@69144
  1837
    "\<lbrakk>closed_map X X' f; f ` topspace X \<subseteq> S\<rbrakk> \<Longrightarrow> closed_map X (subtopology X' S) f"
lp15@69144
  1838
  unfolding closed_map_def closedin_subtopology
lp15@69144
  1839
  using closedin_subset by fastforce
lp15@69144
  1840
lp15@69144
  1841
lemma open_map_into_discrete_topology:
lp15@69144
  1842
    "open_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
lp15@69144
  1843
  unfolding open_map_def openin_discrete_topology using openin_subset by blast
lp15@69144
  1844
lp15@69144
  1845
lemma closed_map_into_discrete_topology:
lp15@69144
  1846
    "closed_map X (discrete_topology U) f \<longleftrightarrow> f ` (topspace X) \<subseteq> U"
lp15@69144
  1847
  unfolding closed_map_def closedin_discrete_topology using closedin_subset by blast
lp15@69144
  1848
lp15@69144
  1849
lemma bijective_open_imp_closed_map:
lp15@69144
  1850
     "\<lbrakk>open_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> closed_map X X' f"
lp15@69144
  1851
  unfolding open_map_def closed_map_def closedin_def
lp15@69144
  1852
  by auto (metis Diff_subset inj_on_image_set_diff)
lp15@69144
  1853
lp15@69144
  1854
lemma bijective_closed_imp_open_map:
lp15@69144
  1855
     "\<lbrakk>closed_map X X' f; f ` (topspace X) = topspace X'; inj_on f (topspace X)\<rbrakk> \<Longrightarrow> open_map X X' f"
lp15@69144
  1856
  unfolding closed_map_def open_map_def openin_closedin_eq
lp15@69144
  1857
  by auto (metis Diff_subset inj_on_image_set_diff)
lp15@69144
  1858
lp15@69144
  1859
lemma open_map_from_subtopology:
lp15@69144
  1860
     "\<lbrakk>open_map X X' f; openin X U\<rbrakk> \<Longrightarrow> open_map (subtopology X U) X' f"
lp15@69144
  1861
  unfolding open_map_def openin_subtopology_alt by blast
lp15@69144
  1862
lp15@69144
  1863
lemma closed_map_from_subtopology:
lp15@69144
  1864
     "\<lbrakk>closed_map X X' f; closedin X U\<rbrakk> \<Longrightarrow> closed_map (subtopology X U) X' f"
lp15@69144
  1865
  unfolding closed_map_def closedin_subtopology_alt by blast
lp15@69144
  1866
lp15@69144
  1867
lemma open_map_restriction:
lp15@69144
  1868
     "\<lbrakk>open_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
lp15@69144
  1869
      \<Longrightarrow> open_map (subtopology X U) (subtopology X' V) f"
lp15@69144
  1870
  unfolding open_map_def openin_subtopology_alt
lp15@69144
  1871
  apply clarify
lp15@69144
  1872
  apply (rename_tac T)
lp15@69144
  1873
  apply (rule_tac x="f ` T" in image_eqI)
lp15@69939
  1874
  using openin_closedin_eq by fastforce+
lp15@69144
  1875
lp15@69144
  1876
lemma closed_map_restriction:
lp15@69144
  1877
     "\<lbrakk>closed_map X X' f; {x. x \<in> topspace X \<and> f x \<in> V} = U\<rbrakk>
lp15@69144
  1878
      \<Longrightarrow> closed_map (subtopology X U) (subtopology X' V) f"
lp15@69144
  1879
  unfolding closed_map_def closedin_subtopology_alt
lp15@69144
  1880
  apply clarify
lp15@69144
  1881
  apply (rename_tac T)
lp15@69144
  1882
  apply (rule_tac x="f ` T" in image_eqI)
lp15@69939
  1883
  using closedin_def by fastforce+
lp15@69144
  1884
lp15@69144
  1885
subsection\<open>Quotient maps\<close>
lp15@69144
  1886
                                      
lp15@69144
  1887
definition quotient_map where
lp15@69144
  1888
 "quotient_map X X' f \<longleftrightarrow>
lp15@69144
  1889
        f ` (topspace X) = topspace X' \<and>
lp15@69144
  1890
        (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (openin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> openin X' U))"
lp15@69144
  1891
lp15@69144
  1892
lemma quotient_map_eq:
lp15@69144
  1893
  assumes "quotient_map X X' f" "\<And>x. x \<in> topspace X \<Longrightarrow> f x = g x"
lp15@69144
  1894
  shows "quotient_map X X' g"
lp15@69144
  1895
proof -
lp15@69144
  1896
  have eq: "{x \<in> topspace X. f x \<in> U} = {x \<in> topspace X. g x \<in> U}" for U
lp15@69144
  1897
    using assms by auto
lp15@69144
  1898
  show ?thesis
lp15@69144
  1899
  using assms
lp15@69144
  1900
  unfolding quotient_map_def
lp15@69144
  1901
  by (metis (mono_tags, lifting) eq image_cong)
lp15@69144
  1902
qed
lp15@69144
  1903
lp15@69144
  1904
lemma quotient_map_compose:
lp15@69144
  1905
  assumes f: "quotient_map X X' f" and g: "quotient_map X' X'' g"
lp15@69144
  1906
  shows "quotient_map X X'' (g \<circ> f)"
lp15@69144
  1907
  unfolding quotient_map_def
lp15@69144
  1908
proof (intro conjI allI impI)
lp15@69144
  1909
  show "(g \<circ> f) ` topspace X = topspace X''"
haftmann@69661
  1910
    using assms by (simp only: image_comp [symmetric]) (simp add: quotient_map_def)
lp15@69144
  1911
next
lp15@69144
  1912
  fix U''
lp15@69144
  1913
  assume "U'' \<subseteq> topspace X''"
lp15@69144
  1914
  define U' where "U' \<equiv> {y \<in> topspace X'. g y \<in> U''}"
lp15@69144
  1915
  have "U' \<subseteq> topspace X'"
lp15@69144
  1916
    by (auto simp add: U'_def)
lp15@69144
  1917
  then have U': "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
lp15@69144
  1918
    using assms unfolding quotient_map_def by simp
lp15@69144
  1919
  have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''} = {x \<in> topspace X. (g \<circ> f) x \<in> U''}"
lp15@69144
  1920
    using f quotient_map_def by fastforce
lp15@69144
  1921
  have "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X {x \<in> topspace X. f x \<in> U'}"
lp15@69144
  1922
    using assms  by (simp add: quotient_map_def U'_def eq)
lp15@69144
  1923
  also have "\<dots> = openin X'' U''"
lp15@69144
  1924
    using U'_def \<open>U'' \<subseteq> topspace X''\<close> U' g quotient_map_def by fastforce
lp15@69144
  1925
  finally show "openin X {x \<in> topspace X. (g \<circ> f) x \<in> U''} = openin X'' U''" .
lp15@69144
  1926
qed
lp15@69144
  1927
lp15@69144
  1928
lemma quotient_map_from_composition:
lp15@69144
  1929
  assumes f: "continuous_map X X' f" and g: "continuous_map X' X'' g" and gf: "quotient_map X X'' (g \<circ> f)"
lp15@69144
  1930
  shows  "quotient_map X' X'' g"
lp15@69144
  1931
  unfolding quotient_map_def
lp15@69144
  1932
proof (intro conjI allI impI)
lp15@69144
  1933
  show "g ` topspace X' = topspace X''"
lp15@69144
  1934
    using assms unfolding continuous_map_def quotient_map_def by fastforce
lp15@69144
  1935
next
lp15@69144
  1936
  fix U'' :: "'c set"
lp15@69144
  1937
  assume U'': "U'' \<subseteq> topspace X''"
lp15@69144
  1938
  have eq: "{x \<in> topspace X. g (f x) \<in> U''} = {x \<in> topspace X. f x \<in> {y. y \<in> topspace X' \<and> g y \<in> U''}}"
lp15@69144
  1939
    using continuous_map_def f by fastforce
lp15@69144
  1940
  show "openin X' {x \<in> topspace X'. g x \<in> U''} = openin X'' U''"
lp15@69144
  1941
    using assms unfolding continuous_map_def quotient_map_def
lp15@69144
  1942
    by (metis (mono_tags, lifting) Collect_cong U'' comp_apply eq)
lp15@69144
  1943
qed
lp15@69144
  1944
lp15@69144
  1945
lemma quotient_imp_continuous_map:
lp15@69144
  1946
    "quotient_map X X' f \<Longrightarrow> continuous_map X X' f"
lp15@69144
  1947
  by (simp add: continuous_map openin_subset quotient_map_def)
lp15@69144
  1948
lp15@69144
  1949
lemma quotient_imp_surjective_map:
lp15@69144
  1950
    "quotient_map X X' f \<Longrightarrow> f ` (topspace X) = topspace X'"
lp15@69144
  1951
  by (simp add: quotient_map_def)
lp15@69144
  1952
lp15@69144
  1953
lemma quotient_map_closedin:
lp15@69144
  1954
  "quotient_map X X' f \<longleftrightarrow>
lp15@69144
  1955
        f ` (topspace X) = topspace X' \<and>
lp15@69144
  1956
        (\<forall>U. U \<subseteq> topspace X' \<longrightarrow> (closedin X {x. x \<in> topspace X \<and> f x \<in> U} \<longleftrightarrow> closedin X' U))"
lp15@69144
  1957
proof -
lp15@69144
  1958
  have eq: "(topspace X - {x \<in> topspace X. f x \<in> U'}) = {x \<in> topspace X. f x \<in> topspace X' \<and> f x \<notin> U'}"
lp15@69144
  1959
    if "f ` topspace X = topspace X'" "U' \<subseteq> topspace X'" for U'
lp15@69144
  1960
      using that by auto
lp15@69144
  1961
  have "(\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U) =
lp15@69144
  1962
          (\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U)"
lp15@69144
  1963
    if "f ` topspace X = topspace X'"
lp15@69144
  1964
  proof (rule iffI; intro allI impI subsetI)
lp15@69144
  1965
    fix U'
lp15@69144
  1966
    assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
lp15@69144
  1967
      and U': "U' \<subseteq> topspace X'"
lp15@69144
  1968
    show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
nipkow@69286
  1969
      using U'  by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
lp15@69144
  1970
  next
lp15@69144
  1971
    fix U' :: "'b set"
lp15@69144
  1972
    assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
lp15@69144
  1973
      and U': "U' \<subseteq> topspace X'"
lp15@69144
  1974
    show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
nipkow@69286
  1975
      using U'  by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
lp15@69144
  1976
  qed
lp15@69144
  1977
  then show ?thesis
lp15@69144
  1978
    unfolding quotient_map_def by force
lp15@69144
  1979
qed
lp15@69144
  1980
lp15@69144
  1981
lemma continuous_open_imp_quotient_map:
lp15@69144
  1982
  assumes "continuous_map X X' f" and om: "open_map X X' f" and feq: "f ` (topspace X) = topspace X'"
lp15@69144
  1983
  shows "quotient_map X X' f"
lp15@69144
  1984
proof -
lp15@69144
  1985
  { fix U
lp15@69144
  1986
    assume U: "U \<subseteq> topspace X'" and "openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  1987
    then have ope: "openin X' (f ` {x \<in> topspace X. f x \<in> U})"
lp15@69144
  1988
      using om unfolding open_map_def by blast
lp15@69144
  1989
    then have "openin X' U"
lp15@69144
  1990
      using U feq by (subst openin_subopen) force
lp15@69144
  1991
  }
lp15@69144
  1992
  moreover have "openin X {x \<in> topspace X. f x \<in> U}" if "U \<subseteq> topspace X'" and "openin X' U" for U
lp15@69144
  1993
    using that assms unfolding continuous_map_def by blast
lp15@69144
  1994
  ultimately show ?thesis
lp15@69144
  1995
    unfolding quotient_map_def using assms by blast
lp15@69144
  1996
qed
lp15@69144
  1997
lp15@69144
  1998
lemma continuous_closed_imp_quotient_map:
lp15@69144
  1999
  assumes "continuous_map X X' f" and om: "closed_map X X' f" and feq: "f ` (topspace X) = topspace X'"
lp15@69144
  2000
  shows "quotient_map X X' f"
lp15@69144
  2001
proof -
lp15@69144
  2002
  have "f ` {x \<in> topspace X. f x \<in> U} = U" if "U \<subseteq> topspace X'" for U
lp15@69144
  2003
    using that feq by auto
lp15@69144
  2004
  with assms show ?thesis
lp15@69144
  2005
    unfolding quotient_map_closedin closed_map_def continuous_map_closedin by auto
lp15@69144
  2006
qed
lp15@69144
  2007
lp15@69144
  2008
lemma continuous_open_quotient_map:
lp15@69144
  2009
   "\<lbrakk>continuous_map X X' f; open_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
lp15@69144
  2010
  by (meson continuous_open_imp_quotient_map quotient_map_def)
lp15@69144
  2011
lp15@69144
  2012
lemma continuous_closed_quotient_map:
lp15@69144
  2013
     "\<lbrakk>continuous_map X X' f; closed_map X X' f\<rbrakk> \<Longrightarrow> quotient_map X X' f \<longleftrightarrow> f ` (topspace X) = topspace X'"
lp15@69144
  2014
  by (meson continuous_closed_imp_quotient_map quotient_map_def)
lp15@69144
  2015
lp15@69144
  2016
lemma injective_quotient_map:
lp15@69144
  2017
  assumes "inj_on f (topspace X)"
lp15@69144
  2018
  shows "quotient_map X X' f \<longleftrightarrow>
lp15@69144
  2019
         continuous_map X X' f \<and> open_map X X' f \<and> closed_map X X' f \<and> f ` (topspace X) = topspace X'"
lp15@69144
  2020
         (is "?lhs = ?rhs")
lp15@69144
  2021
proof
lp15@69144
  2022
  assume L: ?lhs
lp15@69144
  2023
  have "open_map X X' f"
lp15@69144
  2024
  proof (clarsimp simp add: open_map_def)
lp15@69144
  2025
    fix U
lp15@69144
  2026
    assume "openin X U"
lp15@69144
  2027
    then have "U \<subseteq> topspace X"
lp15@69144
  2028
      by (simp add: openin_subset)
lp15@69144
  2029
    moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
lp15@69144
  2030
      using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
lp15@69144
  2031
    ultimately show "openin X' (f ` U)"
lp15@69144
  2032
      using L unfolding quotient_map_def
lp15@69144
  2033
      by (metis (no_types, lifting) Collect_cong \<open>openin X U\<close> image_mono)
lp15@69144
  2034
  qed
lp15@69144
  2035
  moreover have "closed_map X X' f"
lp15@69144
  2036
  proof (clarsimp simp add: closed_map_def)
lp15@69144
  2037
    fix U
lp15@69144
  2038
    assume "closedin X U"
lp15@69144
  2039
    then have "U \<subseteq> topspace X"
lp15@69144
  2040
      by (simp add: closedin_subset)
lp15@69144
  2041
    moreover have "{x \<in> topspace X. f x \<in> f ` U} = U"
lp15@69144
  2042
      using \<open>U \<subseteq> topspace X\<close> assms inj_onD by fastforce
lp15@69144
  2043
    ultimately show "closedin X' (f ` U)"
lp15@69144
  2044
      using L unfolding quotient_map_closedin
lp15@69144
  2045
      by (metis (no_types, lifting) Collect_cong \<open>closedin X U\<close> image_mono)
lp15@69144
  2046
  qed
lp15@69144
  2047
  ultimately show ?rhs
lp15@69144
  2048
    using L by (simp add: quotient_imp_continuous_map quotient_imp_surjective_map)
lp15@69144
  2049
next
lp15@69144
  2050
  assume ?rhs
lp15@69144
  2051
  then show ?lhs
lp15@69144
  2052
    by (simp add: continuous_closed_imp_quotient_map)
lp15@69144
  2053
qed
lp15@69144
  2054
lp15@69144
  2055
lemma continuous_compose_quotient_map:
lp15@69144
  2056
  assumes f: "quotient_map X X' f" and g: "continuous_map X X'' (g \<circ> f)"
lp15@69144
  2057
  shows "continuous_map X' X'' g"
lp15@69144
  2058
  unfolding quotient_map_def continuous_map_def
lp15@69144
  2059
proof (intro conjI ballI allI impI)
lp15@69144
  2060
  show "\<And>x'. x' \<in> topspace X' \<Longrightarrow> g x' \<in> topspace X''"
lp15@69144
  2061
    using assms unfolding quotient_map_def
lp15@69144
  2062
    by (metis (no_types, hide_lams) continuous_map_image_subset_topspace image_comp image_subset_iff)
lp15@69144
  2063
next
lp15@69144
  2064
  fix U'' :: "'c set"
lp15@69144
  2065
  assume U'': "openin X'' U''"
lp15@69144
  2066
  have "f ` topspace X = topspace X'"
lp15@69144
  2067
    by (simp add: f quotient_imp_surjective_map)
lp15@69144
  2068
  then have eq: "{x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U} = {x \<in> topspace X. g (f x) \<in> U}" for U
lp15@69144
  2069
    by auto
lp15@69144
  2070
  have "openin X {x \<in> topspace X. f x \<in> topspace X' \<and> g (f x) \<in> U''}"
lp15@69144
  2071
    unfolding eq using U'' g openin_continuous_map_preimage by fastforce
lp15@69144
  2072
  then have *: "openin X {x \<in> topspace X. f x \<in> {x \<in> topspace X'. g x \<in> U''}}"
lp15@69144
  2073
    by auto
lp15@69144
  2074
  show "openin X' {x \<in> topspace X'. g x \<in> U''}"
lp15@69144
  2075
    using f unfolding quotient_map_def
lp15@69144
  2076
    by (metis (no_types) Collect_subset *)
lp15@69144
  2077
qed
lp15@69144
  2078
lp15@69144
  2079
lemma continuous_compose_quotient_map_eq:
lp15@69144
  2080
   "quotient_map X X' f \<Longrightarrow> continuous_map X X'' (g \<circ> f) \<longleftrightarrow> continuous_map X' X'' g"
lp15@69144
  2081
  using continuous_compose_quotient_map continuous_map_compose quotient_imp_continuous_map by blast
lp15@69144
  2082
lp15@69144
  2083
lemma quotient_map_compose_eq:
lp15@69144
  2084
   "quotient_map X X' f \<Longrightarrow> quotient_map X X'' (g \<circ> f) \<longleftrightarrow> quotient_map X' X'' g"
lp15@69144
  2085
  apply safe
lp15@69144
  2086
  apply (meson continuous_compose_quotient_map_eq quotient_imp_continuous_map quotient_map_from_composition)
lp15@69144
  2087
  by (simp add: quotient_map_compose)
lp15@69144
  2088
lp15@69144
  2089
lemma quotient_map_restriction:
lp15@69144
  2090
  assumes quo: "quotient_map X Y f" and U: "{x \<in> topspace X. f x \<in> V} = U" and disj: "openin Y V \<or> closedin Y V"
lp15@69144
  2091
 shows "quotient_map (subtopology X U) (subtopology Y V) f"
lp15@69144
  2092
  using disj
lp15@69144
  2093
proof
lp15@69144
  2094
  assume V: "openin Y V"
lp15@69144
  2095
  with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
lp15@69144
  2096
    by (auto simp: openin_subset)
lp15@69144
  2097
  have fim: "f ` topspace X = topspace Y"
lp15@69144
  2098
     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U} = openin Y U"
lp15@69144
  2099
    using quo unfolding quotient_map_def by auto
lp15@69144
  2100
  have "openin X U"
lp15@69144
  2101
    using U V Y sub(2) by blast
lp15@69144
  2102
  show ?thesis
lp15@69144
  2103
    unfolding quotient_map_def
lp15@69144
  2104
  proof (intro conjI allI impI)
lp15@69144
  2105
    show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
lp15@69144
  2106
      using sub U fim by (auto simp: topspace_subtopology)
lp15@69144
  2107
  next
lp15@69144
  2108
    fix Y' :: "'b set"
lp15@69144
  2109
    assume "Y' \<subseteq> topspace (subtopology Y V)"
lp15@69144
  2110
    then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
lp15@69144
  2111
      by (simp_all add: topspace_subtopology)
lp15@69144
  2112
    then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
lp15@69144
  2113
      using U by blast
lp15@69144
  2114
    then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
lp15@69144
  2115
      using U V Y \<open>openin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
lp15@69144
  2116
      by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
lp15@69144
  2117
  qed
lp15@69144
  2118
next
lp15@69144
  2119
  assume V: "closedin Y V"
lp15@69144
  2120
  with U have sub: "U \<subseteq> topspace X" "V \<subseteq> topspace Y"
lp15@69144
  2121
    by (auto simp: closedin_subset)
lp15@69144
  2122
  have fim: "f ` topspace X = topspace Y"
lp15@69144
  2123
     and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> closedin X {x \<in> topspace X. f x \<in> U} = closedin Y U"
lp15@69144
  2124
    using quo unfolding quotient_map_closedin by auto
lp15@69144
  2125
  have "closedin X U"
lp15@69144
  2126
    using U V Y sub(2) by blast
lp15@69144
  2127
  show ?thesis
lp15@69144
  2128
    unfolding quotient_map_closedin
lp15@69144
  2129
  proof (intro conjI allI impI)
lp15@69144
  2130
    show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
lp15@69144
  2131
      using sub U fim by (auto simp: topspace_subtopology)
lp15@69144
  2132
  next
lp15@69144
  2133
    fix Y' :: "'b set"
lp15@69144
  2134
    assume "Y' \<subseteq> topspace (subtopology Y V)"
lp15@69144
  2135
    then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
lp15@69144
  2136
      by (simp_all add: topspace_subtopology)
lp15@69144
  2137
    then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
lp15@69144
  2138
      using U by blast
lp15@69144
  2139
    then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
lp15@69144
  2140
      using U V Y \<open>closedin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
lp15@69144
  2141
      by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
lp15@69144
  2142
  qed
lp15@69144
  2143
qed
lp15@69144
  2144
lp15@69144
  2145
lemma quotient_map_saturated_open:
lp15@69144
  2146
     "quotient_map X Y f \<longleftrightarrow>
lp15@69144
  2147
        continuous_map X Y f \<and> f ` (topspace X) = topspace Y \<and>
lp15@69144
  2148
        (\<forall>U. openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U \<longrightarrow> openin Y (f ` U))"
lp15@69144
  2149
     (is "?lhs = ?rhs")
lp15@69144
  2150
proof
lp15@69144
  2151
  assume L: ?lhs
lp15@69144
  2152
  then have fim: "f ` topspace X = topspace Y"
lp15@69144
  2153
    and Y: "\<And>U. U \<subseteq> topspace Y \<Longrightarrow> openin Y U = openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  2154
    unfolding quotient_map_def by auto
lp15@69144
  2155
  show ?rhs
lp15@69144
  2156
  proof (intro conjI allI impI)
lp15@69144
  2157
    show "continuous_map X Y f"
lp15@69144
  2158
      by (simp add: L quotient_imp_continuous_map)
lp15@69144
  2159
    show "f ` topspace X = topspace Y"
lp15@69144
  2160
      by (simp add: fim)
lp15@69144
  2161
  next
lp15@69144
  2162
    fix U :: "'a set"
lp15@69144
  2163
    assume U: "openin X U \<and> {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U"
lp15@69144
  2164
    then have sub:  "f ` U \<subseteq> topspace Y" and eq: "{x \<in> topspace X. f x \<in> f ` U} = U"
lp15@69144
  2165
      using fim openin_subset by fastforce+
lp15@69144
  2166
    show "openin Y (f ` U)"
lp15@69144
  2167
      by (simp add: sub Y eq U)
lp15@69144
  2168
  qed
lp15@69144
  2169
next
lp15@69144
  2170
  assume ?rhs
lp15@69144
  2171
  then have YX: "\<And>U. openin Y U \<Longrightarrow> openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  2172
       and fim: "f ` topspace X = topspace Y"
lp15@69144
  2173
       and XY: "\<And>U. \<lbrakk>openin X U; {x \<in> topspace X. f x \<in> f ` U} \<subseteq> U\<rbrakk> \<Longrightarrow> openin Y (f ` U)"
lp15@69144
  2174
    by (auto simp: quotient_map_def continuous_map_def)
lp15@69144
  2175
  show ?lhs
lp15@69144
  2176
  proof (simp add: quotient_map_def fim, intro allI impI iffI)
lp15@69144
  2177
    fix U :: "'b set"
lp15@69144
  2178
    assume "U \<subseteq> topspace Y" and X: "openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  2179
    have feq: "f ` {x \<in> topspace X. f x \<in> U} = U"
lp15@69144
  2180
      using \<open>U \<subseteq> topspace Y\<close> fim by auto
lp15@69144
  2181
    show "openin Y U"
lp15@69144
  2182
      using XY [OF X] by (simp add: feq)
lp15@69144
  2183
  next
lp15@69144
  2184
    fix U :: "'b set"
lp15@69144
  2185
    assume "U \<subseteq> topspace Y" and Y: "openin Y U"
lp15@69144
  2186
    show "openin X {x \<in> topspace X. f x \<in> U}"
lp15@69144
  2187
      by (metis YX [OF Y])
lp15@69144
  2188
  qed
lp15@69144
  2189
qed
lp15@69144
  2190
lp15@69144
  2191
subsection\<open> Separated Sets\<close>
lp15@69144
  2192
lp15@69144
  2193
definition separatedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
lp15@69144
  2194
  where "separatedin X S T \<equiv>
lp15@69144
  2195
           S \<subseteq> topspace X \<and> T \<subseteq> topspace X \<and>
lp15@69144
  2196
           S \<inter> X closure_of T = {} \<and> T \<inter> X closure_of S = {}"
lp15@69144
  2197
lp15@69144
  2198
lemma separatedin_empty [simp]:
lp15@69144
  2199
     "separatedin X S {} \<longleftrightarrow> S \<subseteq> topspace X"
lp15@69144
  2200
     "separatedin X {} S \<longleftrightarrow> S \<subseteq> topspace X"
lp15@69144
  2201
  by (simp_all add: separatedin_def)
lp15@69144
  2202
lp15@69144
  2203
lemma separatedin_refl [simp]:
lp15@69144
  2204
     "separatedin X S S \<longleftrightarrow> S = {}"
lp15@69144
  2205
proof -
lp15@69144
  2206
  have "\<And>x. \<lbrakk>separatedin X S S; x \<in> S\<rbrakk> \<Longrightarrow> False"
lp15@69144
  2207
    by (metis all_not_in_conv closure_of_subset inf.orderE separatedin_def)
lp15@69144
  2208
  then show ?thesis
lp15@69144
  2209
    by auto
lp15@69144
  2210
qed
lp15@69144
  2211
lp15@69144
  2212
lemma separatedin_sym:
lp15@69144
  2213
     "separatedin X S T \<longleftrightarrow> separatedin X T S"
lp15@69144
  2214
  by (auto simp: separatedin_def)
lp15@69144
  2215
lp15@69144
  2216
lemma separatedin_imp_disjoint:
lp15@69144
  2217
     "separatedin X S T \<Longrightarrow> disjnt S T"
lp15@69144
  2218
  by (meson closure_of_subset disjnt_def disjnt_subset2 separatedin_def)
lp15@69144
  2219
lp15@69144
  2220
lemma separatedin_mono:
lp15@69144
  2221
   "\<lbrakk>separatedin X S T; S' \<subseteq> S; T' \<subseteq> T\<rbrakk> \<Longrightarrow> separatedin X S' T'"
lp15@69144
  2222
  unfolding separatedin_def
lp15@69144
  2223
  using closure_of_mono by blast
lp15@69144
  2224
lp15@69144
  2225
lemma separatedin_open_sets:
lp15@69144
  2226
     "\<lbrakk>openin X S; openin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
lp15@69144
  2227
  unfolding disjnt_def separatedin_def
lp15@69144
  2228
  by (auto simp: openin_Int_closure_of_eq_empty openin_subset)
lp15@69144
  2229
lp15@69144
  2230
lemma separatedin_closed_sets:
lp15@69144
  2231
     "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X S T \<longleftrightarrow> disjnt S T"
lp15@69144
  2232
  by (metis closedin_def closure_of_eq disjnt_def inf_commute separatedin_def)
lp15@69144
  2233
lp15@69144
  2234
lemma separatedin_subtopology:
lp15@69144
  2235
     "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
lp15@69144
  2236
  apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
lp15@69144
  2237
  apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
lp15@69144
  2238
  done
lp15@69144
  2239
lp15@69144
  2240
lemma separatedin_discrete_topology:
lp15@69144
  2241
     "separatedin (discrete_topology U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> disjnt S T"
lp15@69144
  2242
  by (metis openin_discrete_topology separatedin_def separatedin_open_sets topspace_discrete_topology)
lp15@69144
  2243
lp15@69144
  2244
lemma separated_eq_distinguishable:
lp15@69144
  2245
   "separatedin X {x} {y} \<longleftrightarrow>
lp15@69144
  2246
        x \<in> topspace X \<and> y \<in> topspace X \<and>
lp15@69144
  2247
        (\<exists>U. openin X U \<and> x \<in> U \<and> (y \<notin> U)) \<and>
lp15@69144
  2248
        (\<exists>v. openin X v \<and> y \<in> v \<and> (x \<notin> v))"
lp15@69144
  2249
  by (force simp: separatedin_def closure_of_def)
lp15@69144
  2250
lp15@69144
  2251
lemma separatedin_Un [simp]:
lp15@69144
  2252
   "separatedin X S (T \<union> U) \<longleftrightarrow> separatedin X S T \<and> separatedin X S U"
lp15@69144
  2253
   "separatedin X (S \<union> T) U \<longleftrightarrow> separatedin X S U \<and> separatedin X T U"
lp15@69144
  2254