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