src/HOL/Analysis/Abstract_Topology_2.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69939 812ce526da33
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
immler@69616
     1
(*  Author:     L C Paulson, University of Cambridge
immler@69616
     2
    Author:     Amine Chaieb, University of Cambridge
immler@69616
     3
    Author:     Robert Himmelmann, TU Muenchen
immler@69616
     4
    Author:     Brian Huffman, Portland State University
immler@69616
     5
*)
immler@69616
     6
immler@69616
     7
section \<open>Abstract Topology 2\<close>
immler@69616
     8
immler@69616
     9
theory Abstract_Topology_2
immler@69616
    10
  imports
immler@69616
    11
    Elementary_Topology
immler@69616
    12
    Abstract_Topology
immler@69616
    13
    "HOL-Library.Indicator_Function"
immler@69616
    14
begin
immler@69616
    15
immler@69616
    16
text \<open>Combination of Elementary and Abstract Topology\<close>
immler@69616
    17
immler@69616
    18
(* FIXME: move elsewhere *)
immler@69616
    19
immler@69616
    20
lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
immler@69616
    21
  apply auto
immler@69616
    22
  apply (rule_tac x="d/2" in exI)
immler@69616
    23
  apply auto
immler@69616
    24
  done
immler@69616
    25
immler@69616
    26
lemma approachable_lt_le2:  \<comment> \<open>like the above, but pushes aside an extra formula\<close>
immler@69616
    27
    "(\<exists>(d::real) > 0. \<forall>x. Q x \<longrightarrow> f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> Q x \<longrightarrow> P x)"
immler@69616
    28
  apply auto
immler@69616
    29
  apply (rule_tac x="d/2" in exI, auto)
immler@69616
    30
  done
immler@69616
    31
immler@69616
    32
lemma triangle_lemma:
immler@69616
    33
  fixes x y z :: real
immler@69616
    34
  assumes x: "0 \<le> x"
immler@69616
    35
    and y: "0 \<le> y"
immler@69616
    36
    and z: "0 \<le> z"
immler@69616
    37
    and xy: "x\<^sup>2 \<le> y\<^sup>2 + z\<^sup>2"
immler@69616
    38
  shows "x \<le> y + z"
immler@69616
    39
proof -
immler@69616
    40
  have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
immler@69616
    41
    using z y by simp
immler@69616
    42
  with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
immler@69616
    43
    by (simp add: power2_eq_square field_simps)
immler@69616
    44
  from y z have yz: "y + z \<ge> 0"
immler@69616
    45
    by arith
immler@69616
    46
  from power2_le_imp_le[OF th yz] show ?thesis .
immler@69616
    47
qed
immler@69616
    48
immler@69616
    49
lemma isCont_indicator:
immler@69616
    50
  fixes x :: "'a::t2_space"
immler@69616
    51
  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
immler@69616
    52
proof auto
immler@69616
    53
  fix x
immler@69616
    54
  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
immler@69616
    55
  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
immler@69616
    56
    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
immler@69616
    57
  show False
immler@69616
    58
  proof (cases "x \<in> A")
immler@69616
    59
    assume x: "x \<in> A"
immler@69616
    60
    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
immler@69616
    61
    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
immler@69616
    62
      using 1 open_greaterThanLessThan by blast
immler@69616
    63
    then guess U .. note U = this
immler@69616
    64
    hence "\<forall>y\<in>U. indicator A y > (0::real)"
immler@69616
    65
      unfolding greaterThanLessThan_def by auto
immler@69616
    66
    hence "U \<subseteq> A" using indicator_eq_0_iff by force
immler@69616
    67
    hence "x \<in> interior A" using U interiorI by auto
immler@69616
    68
    thus ?thesis using fr unfolding frontier_def by simp
immler@69616
    69
  next
immler@69616
    70
    assume x: "x \<notin> A"
immler@69616
    71
    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
immler@69616
    72
    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
immler@69616
    73
      using 1 open_greaterThanLessThan by blast
immler@69616
    74
    then guess U .. note U = this
immler@69616
    75
    hence "\<forall>y\<in>U. indicator A y < (1::real)"
immler@69616
    76
      unfolding greaterThanLessThan_def by auto
immler@69616
    77
    hence "U \<subseteq> -A" by auto
immler@69616
    78
    hence "x \<in> interior (-A)" using U interiorI by auto
immler@69616
    79
    thus ?thesis using fr interior_complement unfolding frontier_def by auto
immler@69616
    80
  qed
immler@69616
    81
next
immler@69616
    82
  assume nfr: "x \<notin> frontier A"
immler@69616
    83
  hence "x \<in> interior A \<or> x \<in> interior (-A)"
immler@69616
    84
    by (auto simp: frontier_def closure_interior)
immler@69616
    85
  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
immler@69616
    86
  proof
immler@69616
    87
    assume int: "x \<in> interior A"
immler@69616
    88
    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
immler@69616
    89
    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
immler@69616
    90
    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
immler@69616
    91
    thus ?thesis using U continuous_on_eq_continuous_at by auto
immler@69616
    92
  next
immler@69616
    93
    assume ext: "x \<in> interior (-A)"
immler@69616
    94
    then obtain U where U: "open U" "x \<in> U" "U \<subseteq> -A" unfolding interior_def by auto
immler@69616
    95
    then have "continuous_on U (indicator A)"
immler@69616
    96
      using continuous_on_topological by (auto simp: subset_iff)
immler@69616
    97
    thus ?thesis using U continuous_on_eq_continuous_at by auto
immler@69616
    98
  qed
immler@69616
    99
qed
immler@69616
   100
immler@69616
   101
lemma closedin_limpt:
lp15@69922
   102
  "closedin (top_of_set T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
immler@69616
   103
  apply (simp add: closedin_closed, safe)
immler@69616
   104
   apply (simp add: closed_limpt islimpt_subset)
immler@69616
   105
  apply (rule_tac x="closure S" in exI, simp)
immler@69616
   106
  apply (force simp: closure_def)
immler@69616
   107
  done
immler@69616
   108
lp15@69922
   109
lemma closedin_closed_eq: "closed S \<Longrightarrow> closedin (top_of_set S) T \<longleftrightarrow> closed T \<and> T \<subseteq> S"
immler@69616
   110
  by (meson closedin_limpt closed_subset closedin_closed_trans)
immler@69616
   111
immler@69616
   112
lemma connected_closed_set:
immler@69616
   113
   "closed S
immler@69616
   114
    \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
immler@69616
   115
  unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
immler@69616
   116
immler@69616
   117
text \<open>If a connnected set is written as the union of two nonempty closed sets, then these sets
immler@69616
   118
have to intersect.\<close>
immler@69616
   119
immler@69616
   120
lemma connected_as_closed_union:
immler@69616
   121
  assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
immler@69616
   122
  shows "A \<inter> B \<noteq> {}"
immler@69616
   123
by (metis assms closed_Un connected_closed_set)
immler@69616
   124
immler@69616
   125
lemma closedin_subset_trans:
lp15@69922
   126
  "closedin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
lp15@69922
   127
    closedin (top_of_set T) S"
immler@69616
   128
  by (meson closedin_limpt subset_iff)
immler@69616
   129
immler@69616
   130
lemma openin_subset_trans:
lp15@69922
   131
  "openin (top_of_set U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
lp15@69922
   132
    openin (top_of_set T) S"
immler@69616
   133
  by (auto simp: openin_open)
immler@69616
   134
immler@69616
   135
lemma closedin_compact:
lp15@69922
   136
   "\<lbrakk>compact S; closedin (top_of_set S) T\<rbrakk> \<Longrightarrow> compact T"
immler@69616
   137
by (metis closedin_closed compact_Int_closed)
immler@69616
   138
immler@69616
   139
lemma closedin_compact_eq:
immler@69616
   140
  fixes S :: "'a::t2_space set"
immler@69616
   141
  shows
immler@69616
   142
   "compact S
lp15@69922
   143
         \<Longrightarrow> (closedin (top_of_set S) T \<longleftrightarrow>
immler@69616
   144
              compact T \<and> T \<subseteq> S)"
immler@69616
   145
by (metis closedin_imp_subset closedin_compact closed_subset compact_imp_closed)
immler@69616
   146
immler@69616
   147
immler@69616
   148
subsection \<open>Closure\<close>
immler@69616
   149
lp15@69922
   150
lemma euclidean_closure_of [simp]: "euclidean closure_of S = closure S"
lp15@69922
   151
  by (auto simp: closure_of_def closure_def islimpt_def)
lp15@69922
   152
immler@69616
   153
lemma closure_openin_Int_closure:
lp15@69922
   154
  assumes ope: "openin (top_of_set U) S" and "T \<subseteq> U"
immler@69616
   155
  shows "closure(S \<inter> closure T) = closure(S \<inter> T)"
immler@69616
   156
proof
immler@69616
   157
  obtain V where "open V" and S: "S = U \<inter> V"
immler@69616
   158
    using ope using openin_open by metis
immler@69616
   159
  show "closure (S \<inter> closure T) \<subseteq> closure (S \<inter> T)"
immler@69616
   160
    proof (clarsimp simp: S)
immler@69616
   161
      fix x
immler@69616
   162
      assume  "x \<in> closure (U \<inter> V \<inter> closure T)"
immler@69616
   163
      then have "V \<inter> closure T \<subseteq> A \<Longrightarrow> x \<in> closure A" for A
immler@69616
   164
          by (metis closure_mono subsetD inf.coboundedI2 inf_assoc)
immler@69616
   165
      then have "x \<in> closure (T \<inter> V)"
immler@69616
   166
         by (metis \<open>open V\<close> closure_closure inf_commute open_Int_closure_subset)
immler@69616
   167
      then show "x \<in> closure (U \<inter> V \<inter> T)"
immler@69616
   168
        by (metis \<open>T \<subseteq> U\<close> inf.absorb_iff2 inf_assoc inf_commute)
immler@69616
   169
    qed
immler@69616
   170
next
immler@69616
   171
  show "closure (S \<inter> T) \<subseteq> closure (S \<inter> closure T)"
immler@69616
   172
    by (meson Int_mono closure_mono closure_subset order_refl)
immler@69616
   173
qed
immler@69616
   174
immler@69616
   175
corollary infinite_openin:
immler@69616
   176
  fixes S :: "'a :: t1_space set"
lp15@69922
   177
  shows "\<lbrakk>openin (top_of_set U) S; x \<in> S; x islimpt U\<rbrakk> \<Longrightarrow> infinite S"
immler@69616
   178
  by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute)
immler@69616
   179
immler@69622
   180
lemma closure_Int_ballI:
lp15@69922
   181
  assumes "\<And>U. \<lbrakk>openin (top_of_set S) U; U \<noteq> {}\<rbrakk> \<Longrightarrow> T \<inter> U \<noteq> {}"
immler@69622
   182
  shows "S \<subseteq> closure T"
immler@69622
   183
proof (clarsimp simp: closure_iff_nhds_not_empty)
immler@69622
   184
  fix x and A and V
immler@69622
   185
  assume "x \<in> S" "V \<subseteq> A" "open V" "x \<in> V" "T \<inter> A = {}"
lp15@69922
   186
  then have "openin (top_of_set S) (A \<inter> V \<inter> S)"
immler@69622
   187
    by (auto simp: openin_open intro!: exI[where x="V"])
immler@69622
   188
  moreover have "A \<inter> V \<inter> S \<noteq> {}" using \<open>x \<in> V\<close> \<open>V \<subseteq> A\<close> \<open>x \<in> S\<close>
immler@69622
   189
    by auto
immler@69622
   190
  ultimately have "T \<inter> (A \<inter> V \<inter> S) \<noteq> {}"
immler@69622
   191
    by (rule assms)
immler@69622
   192
  with \<open>T \<inter> A = {}\<close> show False by auto
immler@69622
   193
qed
immler@69622
   194
immler@69622
   195
immler@69616
   196
subsection \<open>Frontier\<close>
immler@69616
   197
lp15@69922
   198
lemma euclidean_interior_of [simp]: "euclidean interior_of S = interior S"
lp15@69922
   199
  by (auto simp: interior_of_def interior_def)
lp15@69922
   200
lp15@69922
   201
lemma euclidean_frontier_of [simp]: "euclidean frontier_of S = frontier S"
lp15@69922
   202
  by (auto simp: frontier_of_def frontier_def)
lp15@69922
   203
immler@69616
   204
lemma connected_Int_frontier:
immler@69616
   205
     "\<lbrakk>connected s; s \<inter> t \<noteq> {}; s - t \<noteq> {}\<rbrakk> \<Longrightarrow> (s \<inter> frontier t \<noteq> {})"
immler@69616
   206
  apply (simp add: frontier_interiors connected_openin, safe)
immler@69616
   207
  apply (drule_tac x="s \<inter> interior t" in spec, safe)
immler@69616
   208
   apply (drule_tac [2] x="s \<inter> interior (-t)" in spec)
immler@69616
   209
   apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD])
immler@69616
   210
  done
immler@69616
   211
immler@69616
   212
subsection \<open>Compactness\<close>
immler@69616
   213
immler@69616
   214
lemma openin_delete:
immler@69616
   215
  fixes a :: "'a :: t1_space"
lp15@69922
   216
  shows "openin (top_of_set u) s
lp15@69922
   217
         \<Longrightarrow> openin (top_of_set u) (s - {a})"
immler@69616
   218
by (metis Int_Diff open_delete openin_open)
immler@69616
   219
immler@69616
   220
lemma compact_eq_openin_cover:
immler@69616
   221
  "compact S \<longleftrightarrow>
lp15@69922
   222
    (\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
immler@69616
   223
      (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
immler@69616
   224
proof safe
immler@69616
   225
  fix C
lp15@69922
   226
  assume "compact S" and "\<forall>c\<in>C. openin (top_of_set S) c" and "S \<subseteq> \<Union>C"
immler@69616
   227
  then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
immler@69616
   228
    unfolding openin_open by force+
immler@69616
   229
  with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
immler@69616
   230
    by (meson compactE)
immler@69616
   231
  then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
immler@69616
   232
    by auto
immler@69616
   233
  then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
immler@69616
   234
next
lp15@69922
   235
  assume 1: "\<forall>C. (\<forall>c\<in>C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>C \<longrightarrow>
immler@69616
   236
        (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D)"
immler@69616
   237
  show "compact S"
immler@69616
   238
  proof (rule compactI)
immler@69616
   239
    fix C
immler@69616
   240
    let ?C = "image (\<lambda>T. S \<inter> T) C"
immler@69616
   241
    assume "\<forall>t\<in>C. open t" and "S \<subseteq> \<Union>C"
lp15@69922
   242
    then have "(\<forall>c\<in>?C. openin (top_of_set S) c) \<and> S \<subseteq> \<Union>?C"
immler@69616
   243
      unfolding openin_open by auto
immler@69616
   244
    with 1 obtain D where "D \<subseteq> ?C" and "finite D" and "S \<subseteq> \<Union>D"
immler@69616
   245
      by metis
immler@69616
   246
    let ?D = "inv_into C (\<lambda>T. S \<inter> T) ` D"
immler@69616
   247
    have "?D \<subseteq> C \<and> finite ?D \<and> S \<subseteq> \<Union>?D"
immler@69616
   248
    proof (intro conjI)
immler@69616
   249
      from \<open>D \<subseteq> ?C\<close> show "?D \<subseteq> C"
immler@69616
   250
        by (fast intro: inv_into_into)
immler@69616
   251
      from \<open>finite D\<close> show "finite ?D"
immler@69616
   252
        by (rule finite_imageI)
immler@69616
   253
      from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
immler@69616
   254
        apply (rule subset_trans, clarsimp)
immler@69616
   255
        apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
immler@69616
   256
        apply (erule rev_bexI, fast)
immler@69616
   257
        done
immler@69616
   258
    qed
immler@69616
   259
    then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
immler@69616
   260
  qed
immler@69616
   261
qed
immler@69616
   262
immler@69616
   263
immler@69616
   264
subsection \<open>Continuity\<close>
immler@69616
   265
immler@69616
   266
lemma interior_image_subset:
immler@69616
   267
  assumes "inj f" "\<And>x. continuous (at x) f"
immler@69616
   268
  shows "interior (f ` S) \<subseteq> f ` (interior S)"
immler@69616
   269
proof
immler@69616
   270
  fix x assume "x \<in> interior (f ` S)"
immler@69616
   271
  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` S" ..
immler@69616
   272
  then have "x \<in> f ` S" by auto
immler@69616
   273
  then obtain y where y: "y \<in> S" "x = f y" by auto
immler@69616
   274
  have "open (f -` T)"
immler@69616
   275
    using assms \<open>open T\<close> by (simp add: continuous_at_imp_continuous_on open_vimage)
immler@69616
   276
  moreover have "y \<in> vimage f T"
immler@69616
   277
    using \<open>x = f y\<close> \<open>x \<in> T\<close> by simp
immler@69616
   278
  moreover have "vimage f T \<subseteq> S"
immler@69616
   279
    using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
immler@69616
   280
  ultimately have "y \<in> interior S" ..
immler@69616
   281
  with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
immler@69616
   282
qed
immler@69616
   283
immler@69616
   284
subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
immler@69616
   285
immler@69616
   286
lemma continuous_closedin_preimage_constant:
immler@69616
   287
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
lp15@69922
   288
  shows "continuous_on S f \<Longrightarrow> closedin (top_of_set S) {x \<in> S. f x = a}"
immler@69616
   289
  using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
immler@69616
   290
immler@69616
   291
lemma continuous_closed_preimage_constant:
immler@69616
   292
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
immler@69616
   293
  shows "continuous_on S f \<Longrightarrow> closed S \<Longrightarrow> closed {x \<in> S. f x = a}"
immler@69616
   294
  using continuous_closed_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)
immler@69616
   295
immler@69616
   296
lemma continuous_constant_on_closure:
immler@69616
   297
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
immler@69616
   298
  assumes "continuous_on (closure S) f"
immler@69616
   299
      and "\<And>x. x \<in> S \<Longrightarrow> f x = a"
immler@69616
   300
      and "x \<in> closure S"
immler@69616
   301
  shows "f x = a"
immler@69616
   302
    using continuous_closed_preimage_constant[of "closure S" f a]
immler@69616
   303
      assms closure_minimal[of S "{x \<in> closure S. f x = a}"] closure_subset
immler@69616
   304
    unfolding subset_eq
immler@69616
   305
    by auto
immler@69616
   306
immler@69616
   307
lemma image_closure_subset:
immler@69616
   308
  assumes contf: "continuous_on (closure S) f"
immler@69616
   309
    and "closed T"
immler@69616
   310
    and "(f ` S) \<subseteq> T"
immler@69616
   311
  shows "f ` (closure S) \<subseteq> T"
immler@69616
   312
proof -
immler@69616
   313
  have "S \<subseteq> {x \<in> closure S. f x \<in> T}"
immler@69616
   314
    using assms(3) closure_subset by auto
immler@69616
   315
  moreover have "closed (closure S \<inter> f -` T)"
immler@69616
   316
    using continuous_closed_preimage[OF contf] \<open>closed T\<close> by auto
immler@69616
   317
  ultimately have "closure S = (closure S \<inter> f -` T)"
immler@69616
   318
    using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
immler@69616
   319
  then show ?thesis by auto
immler@69616
   320
qed
immler@69616
   321
immler@69616
   322
subsection%unimportant \<open>A function constant on a set\<close>
immler@69616
   323
immler@69616
   324
definition constant_on  (infixl "(constant'_on)" 50)
immler@69616
   325
  where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
immler@69616
   326
immler@69616
   327
lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"
immler@69616
   328
  unfolding constant_on_def by blast
immler@69616
   329
immler@69616
   330
lemma injective_not_constant:
immler@69616
   331
  fixes S :: "'a::{perfect_space} set"
immler@69616
   332
  shows "\<lbrakk>open S; inj_on f S; f constant_on S\<rbrakk> \<Longrightarrow> S = {}"
immler@69616
   333
unfolding constant_on_def
immler@69616
   334
by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
immler@69616
   335
immler@69616
   336
lemma constant_on_closureI:
immler@69616
   337
  fixes f :: "_ \<Rightarrow> 'b::t1_space"
immler@69616
   338
  assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
immler@69616
   339
    shows "f constant_on (closure S)"
immler@69616
   340
using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
immler@69616
   341
by metis
immler@69616
   342
immler@69616
   343
immler@69616
   344
subsection%unimportant \<open>Continuity relative to a union.\<close>
immler@69616
   345
immler@69616
   346
lemma continuous_on_Un_local:
lp15@69922
   347
    "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
immler@69616
   348
      continuous_on s f; continuous_on t f\<rbrakk>
immler@69616
   349
     \<Longrightarrow> continuous_on (s \<union> t) f"
immler@69616
   350
  unfolding continuous_on closedin_limpt
immler@69616
   351
  by (metis Lim_trivial_limit Lim_within_union Un_iff trivial_limit_within)
immler@69616
   352
immler@69616
   353
lemma continuous_on_cases_local:
lp15@69922
   354
     "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
immler@69616
   355
       continuous_on s f; continuous_on t g;
immler@69616
   356
       \<And>x. \<lbrakk>x \<in> s \<and> \<not>P x \<or> x \<in> t \<and> P x\<rbrakk> \<Longrightarrow> f x = g x\<rbrakk>
immler@69616
   357
      \<Longrightarrow> continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
immler@69616
   358
  by (rule continuous_on_Un_local) (auto intro: continuous_on_eq)
immler@69616
   359
immler@69616
   360
lemma continuous_on_cases_le:
immler@69616
   361
  fixes h :: "'a :: topological_space \<Rightarrow> real"
immler@69616
   362
  assumes "continuous_on {t \<in> s. h t \<le> a} f"
immler@69616
   363
      and "continuous_on {t \<in> s. a \<le> h t} g"
immler@69616
   364
      and h: "continuous_on s h"
immler@69616
   365
      and "\<And>t. \<lbrakk>t \<in> s; h t = a\<rbrakk> \<Longrightarrow> f t = g t"
immler@69616
   366
    shows "continuous_on s (\<lambda>t. if h t \<le> a then f(t) else g(t))"
immler@69616
   367
proof -
immler@69616
   368
  have s: "s = (s \<inter> h -` atMost a) \<union> (s \<inter> h -` atLeast a)"
immler@69616
   369
    by force
lp15@69922
   370
  have 1: "closedin (top_of_set s) (s \<inter> h -` atMost a)"
immler@69616
   371
    by (rule continuous_closedin_preimage [OF h closed_atMost])
lp15@69922
   372
  have 2: "closedin (top_of_set s) (s \<inter> h -` atLeast a)"
immler@69616
   373
    by (rule continuous_closedin_preimage [OF h closed_atLeast])
immler@69616
   374
  have eq: "s \<inter> h -` {..a} = {t \<in> s. h t \<le> a}" "s \<inter> h -` {a..} = {t \<in> s. a \<le> h t}"
immler@69616
   375
    by auto
immler@69616
   376
  show ?thesis
immler@69616
   377
    apply (rule continuous_on_subset [of s, OF _ order_refl])
immler@69616
   378
    apply (subst s)
immler@69616
   379
    apply (rule continuous_on_cases_local)
immler@69616
   380
    using 1 2 s assms apply (auto simp: eq)
immler@69616
   381
    done
immler@69616
   382
qed
immler@69616
   383
immler@69616
   384
lemma continuous_on_cases_1:
immler@69616
   385
  fixes s :: "real set"
immler@69616
   386
  assumes "continuous_on {t \<in> s. t \<le> a} f"
immler@69616
   387
      and "continuous_on {t \<in> s. a \<le> t} g"
immler@69616
   388
      and "a \<in> s \<Longrightarrow> f a = g a"
immler@69616
   389
    shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
immler@69616
   390
using assms
immler@69616
   391
by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
immler@69616
   392
immler@69616
   393
immler@69616
   394
subsection%unimportant\<open>Inverse function property for open/closed maps\<close>
immler@69616
   395
immler@69616
   396
lemma continuous_on_inverse_open_map:
immler@69616
   397
  assumes contf: "continuous_on S f"
immler@69616
   398
    and imf: "f ` S = T"
immler@69616
   399
    and injf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
lp15@69922
   400
    and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
immler@69616
   401
  shows "continuous_on T g"
immler@69616
   402
proof -
immler@69616
   403
  from imf injf have gTS: "g ` T = S"
immler@69616
   404
    by force
immler@69616
   405
  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
immler@69616
   406
    by force
immler@69616
   407
  show ?thesis
immler@69616
   408
    by (simp add: continuous_on_open [of T g] gTS) (metis openin_imp_subset fU oo)
immler@69616
   409
qed
immler@69616
   410
immler@69616
   411
lemma continuous_on_inverse_closed_map:
immler@69616
   412
  assumes contf: "continuous_on S f"
immler@69616
   413
    and imf: "f ` S = T"
immler@69616
   414
    and injf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
lp15@69922
   415
    and oo: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)"
immler@69616
   416
  shows "continuous_on T g"
immler@69616
   417
proof -
immler@69616
   418
  from imf injf have gTS: "g ` T = S"
immler@69616
   419
    by force
immler@69616
   420
  from imf injf have fU: "U \<subseteq> S \<Longrightarrow> (f ` U) = T \<inter> g -` U" for U
immler@69616
   421
    by force
immler@69616
   422
  show ?thesis
immler@69616
   423
    by (simp add: continuous_on_closed [of T g] gTS) (metis closedin_imp_subset fU oo)
immler@69616
   424
qed
immler@69616
   425
immler@69616
   426
lemma homeomorphism_injective_open_map:
immler@69616
   427
  assumes contf: "continuous_on S f"
immler@69616
   428
    and imf: "f ` S = T"
immler@69616
   429
    and injf: "inj_on f S"
lp15@69922
   430
    and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
immler@69616
   431
  obtains g where "homeomorphism S T f g"
immler@69616
   432
proof
immler@69616
   433
  have "continuous_on T (inv_into S f)"
immler@69616
   434
    by (metis contf continuous_on_inverse_open_map imf injf inv_into_f_f oo)
immler@69616
   435
  with imf injf contf show "homeomorphism S T f (inv_into S f)"
immler@69616
   436
    by (auto simp: homeomorphism_def)
immler@69616
   437
qed
immler@69616
   438
immler@69616
   439
lemma homeomorphism_injective_closed_map:
immler@69616
   440
  assumes contf: "continuous_on S f"
immler@69616
   441
    and imf: "f ` S = T"
immler@69616
   442
    and injf: "inj_on f S"
lp15@69922
   443
    and oo: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)"
immler@69616
   444
  obtains g where "homeomorphism S T f g"
immler@69616
   445
proof
immler@69616
   446
  have "continuous_on T (inv_into S f)"
immler@69616
   447
    by (metis contf continuous_on_inverse_closed_map imf injf inv_into_f_f oo)
immler@69616
   448
  with imf injf contf show "homeomorphism S T f (inv_into S f)"
immler@69616
   449
    by (auto simp: homeomorphism_def)
immler@69616
   450
qed
immler@69616
   451
immler@69616
   452
lemma homeomorphism_imp_open_map:
immler@69616
   453
  assumes hom: "homeomorphism S T f g"
lp15@69922
   454
    and oo: "openin (top_of_set S) U"
lp15@69922
   455
  shows "openin (top_of_set T) (f ` U)"
immler@69616
   456
proof -
immler@69616
   457
  from hom oo have [simp]: "f ` U = T \<inter> g -` U"
immler@69616
   458
    using openin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
immler@69616
   459
  from hom have "continuous_on T g"
immler@69616
   460
    unfolding homeomorphism_def by blast
immler@69616
   461
  moreover have "g ` T = S"
immler@69616
   462
    by (metis hom homeomorphism_def)
immler@69616
   463
  ultimately show ?thesis
immler@69616
   464
    by (simp add: continuous_on_open oo)
immler@69616
   465
qed
immler@69616
   466
immler@69616
   467
lemma homeomorphism_imp_closed_map:
immler@69616
   468
  assumes hom: "homeomorphism S T f g"
lp15@69922
   469
    and oo: "closedin (top_of_set S) U"
lp15@69922
   470
  shows "closedin (top_of_set T) (f ` U)"
immler@69616
   471
proof -
immler@69616
   472
  from hom oo have [simp]: "f ` U = T \<inter> g -` U"
immler@69616
   473
    using closedin_subset by (fastforce simp: homeomorphism_def rev_image_eqI)
immler@69616
   474
  from hom have "continuous_on T g"
immler@69616
   475
    unfolding homeomorphism_def by blast
immler@69616
   476
  moreover have "g ` T = S"
immler@69616
   477
    by (metis hom homeomorphism_def)
immler@69616
   478
  ultimately show ?thesis
immler@69616
   479
    by (simp add: continuous_on_closed oo)
immler@69616
   480
qed
immler@69616
   481
immler@69616
   482
subsection%unimportant \<open>Seperability\<close>
immler@69616
   483
immler@69616
   484
lemma subset_second_countable:
immler@69616
   485
  obtains \<B> :: "'a:: second_countable_topology set set"
immler@69616
   486
    where "countable \<B>"
immler@69616
   487
          "{} \<notin> \<B>"
lp15@69922
   488
          "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C"
lp15@69922
   489
          "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
immler@69616
   490
proof -
immler@69616
   491
  obtain \<B> :: "'a set set"
immler@69616
   492
    where "countable \<B>"
lp15@69922
   493
      and opeB: "\<And>C. C \<in> \<B> \<Longrightarrow> openin(top_of_set S) C"
lp15@69922
   494
      and \<B>:    "\<And>T. openin(top_of_set S) T \<Longrightarrow> \<exists>\<U>. \<U> \<subseteq> \<B> \<and> T = \<Union>\<U>"
immler@69616
   495
  proof -
immler@69616
   496
    obtain \<C> :: "'a set set"
immler@69616
   497
      where "countable \<C>" and ope: "\<And>C. C \<in> \<C> \<Longrightarrow> open C"
immler@69616
   498
        and \<C>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<C> \<and> S = \<Union>U"
immler@69616
   499
      by (metis univ_second_countable that)
immler@69616
   500
    show ?thesis
immler@69616
   501
    proof
immler@69616
   502
      show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
immler@69616
   503
        by (simp add: \<open>countable \<C>\<close>)
lp15@69922
   504
      show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (top_of_set S) C"
immler@69616
   505
        using ope by auto
lp15@69922
   506
      show "\<And>T. openin (top_of_set S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
immler@69616
   507
        by (metis \<C> image_mono inf_Sup openin_open)
immler@69616
   508
    qed
immler@69616
   509
  qed
immler@69616
   510
  show ?thesis
immler@69616
   511
  proof
immler@69616
   512
    show "countable (\<B> - {{}})"
immler@69616
   513
      using \<open>countable \<B>\<close> by blast
lp15@69922
   514
    show "\<And>C. \<lbrakk>C \<in> \<B> - {{}}\<rbrakk> \<Longrightarrow> openin (top_of_set S) C"
lp15@69922
   515
      by (simp add: \<open>\<And>C. C \<in> \<B> \<Longrightarrow> openin (top_of_set S) C\<close>)
lp15@69922
   516
    show "\<exists>\<U>\<subseteq>\<B> - {{}}. T = \<Union>\<U>" if "openin (top_of_set S) T" for T
immler@69616
   517
      using \<B> [OF that]
immler@69616
   518
      apply clarify
immler@69616
   519
      apply (rule_tac x="\<U> - {{}}" in exI, auto)
immler@69616
   520
        done
immler@69616
   521
  qed auto
immler@69616
   522
qed
immler@69616
   523
immler@69616
   524
lemma Lindelof_openin:
immler@69616
   525
  fixes \<F> :: "'a::second_countable_topology set set"
lp15@69922
   526
  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> openin (top_of_set U) S"
immler@69616
   527
  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
immler@69616
   528
proof -
immler@69616
   529
  have "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>T. open T \<and> S = U \<inter> T"
immler@69616
   530
    using assms by (simp add: openin_open)
immler@69616
   531
  then obtain tf where tf: "\<And>S. S \<in> \<F> \<Longrightarrow> open (tf S) \<and> (S = U \<inter> tf S)"
immler@69616
   532
    by metis
immler@69616
   533
  have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
immler@69616
   534
    using tf by fastforce
immler@69616
   535
  obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
immler@69616
   536
    using tf by (force intro: Lindelof [of "tf ` \<F>"])
immler@69616
   537
  then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
immler@69616
   538
    by (clarsimp simp add: countable_subset_image)
immler@69616
   539
  then show ?thesis ..
immler@69616
   540
qed
immler@69616
   541
immler@69616
   542
immler@69616
   543
subsection%unimportant\<open>Closed Maps\<close>
immler@69616
   544
immler@69616
   545
lemma continuous_imp_closed_map:
immler@69616
   546
  fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
lp15@69922
   547
  assumes "closedin (top_of_set S) U"
immler@69616
   548
          "continuous_on S f" "f ` S = T" "compact S"
lp15@69922
   549
    shows "closedin (top_of_set T) (f ` U)"
immler@69616
   550
  by (metis assms closedin_compact_eq compact_continuous_image continuous_on_subset subset_image_iff)
immler@69616
   551
immler@69616
   552
lemma closed_map_restrict:
lp15@69922
   553
  assumes cloU: "closedin (top_of_set (S \<inter> f -` T')) U"
lp15@69922
   554
    and cc: "\<And>U. closedin (top_of_set S) U \<Longrightarrow> closedin (top_of_set T) (f ` U)"
immler@69616
   555
    and "T' \<subseteq> T"
lp15@69922
   556
  shows "closedin (top_of_set T') (f ` U)"
immler@69616
   557
proof -
immler@69616
   558
  obtain V where "closed V" "U = S \<inter> f -` T' \<inter> V"
immler@69616
   559
    using cloU by (auto simp: closedin_closed)
immler@69616
   560
  with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
immler@69616
   561
    by (fastforce simp add: closedin_closed)
immler@69616
   562
qed
immler@69616
   563
immler@69616
   564
subsection%unimportant\<open>Open Maps\<close>
immler@69616
   565
immler@69616
   566
lemma open_map_restrict:
lp15@69922
   567
  assumes opeU: "openin (top_of_set (S \<inter> f -` T')) U"
lp15@69922
   568
    and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
immler@69616
   569
    and "T' \<subseteq> T"
lp15@69922
   570
  shows "openin (top_of_set T') (f ` U)"
immler@69616
   571
proof -
immler@69616
   572
  obtain V where "open V" "U = S \<inter> f -` T' \<inter> V"
immler@69616
   573
    using opeU by (auto simp: openin_open)
immler@69616
   574
  with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
immler@69616
   575
    by (fastforce simp add: openin_open)
immler@69616
   576
qed
immler@69616
   577
immler@69616
   578
immler@69616
   579
subsection%unimportant\<open>Quotient maps\<close>
immler@69616
   580
immler@69616
   581
lemma quotient_map_imp_continuous_open:
immler@69616
   582
  assumes T: "f ` S \<subseteq> T"
immler@69616
   583
      and ope: "\<And>U. U \<subseteq> T
lp15@69922
   584
              \<Longrightarrow> (openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@69922
   585
                   openin (top_of_set T) U)"
immler@69616
   586
    shows "continuous_on S f"
immler@69616
   587
proof -
immler@69616
   588
  have [simp]: "S \<inter> f -` f ` S = S" by auto
immler@69616
   589
  show ?thesis
immler@69616
   590
    using ope [OF T]
immler@69616
   591
    apply (simp add: continuous_on_open)
immler@69616
   592
    by (meson ope openin_imp_subset openin_trans)
immler@69616
   593
qed
immler@69616
   594
immler@69616
   595
lemma quotient_map_imp_continuous_closed:
immler@69616
   596
  assumes T: "f ` S \<subseteq> T"
immler@69616
   597
      and ope: "\<And>U. U \<subseteq> T
lp15@69922
   598
                  \<Longrightarrow> (closedin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@69922
   599
                       closedin (top_of_set T) U)"
immler@69616
   600
    shows "continuous_on S f"
immler@69616
   601
proof -
immler@69616
   602
  have [simp]: "S \<inter> f -` f ` S = S" by auto
immler@69616
   603
  show ?thesis
immler@69616
   604
    using ope [OF T]
immler@69616
   605
    apply (simp add: continuous_on_closed)
immler@69616
   606
    by (metis (no_types, lifting) ope closedin_imp_subset closedin_trans)
immler@69616
   607
qed
immler@69616
   608
immler@69616
   609
lemma open_map_imp_quotient_map:
immler@69616
   610
  assumes contf: "continuous_on S f"
immler@69616
   611
      and T: "T \<subseteq> f ` S"
lp15@69922
   612
      and ope: "\<And>T. openin (top_of_set S) T
lp15@69922
   613
                   \<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)"
lp15@69922
   614
    shows "openin (top_of_set S) (S \<inter> f -` T) =
lp15@69922
   615
           openin (top_of_set (f ` S)) T"
immler@69616
   616
proof -
immler@69616
   617
  have "T = f ` (S \<inter> f -` T)"
immler@69616
   618
    using T by blast
immler@69616
   619
  then show ?thesis
immler@69616
   620
    using "ope" contf continuous_on_open by metis
immler@69616
   621
qed
immler@69616
   622
immler@69616
   623
lemma closed_map_imp_quotient_map:
immler@69616
   624
  assumes contf: "continuous_on S f"
immler@69616
   625
      and T: "T \<subseteq> f ` S"
lp15@69922
   626
      and ope: "\<And>T. closedin (top_of_set S) T
lp15@69922
   627
              \<Longrightarrow> closedin (top_of_set (f ` S)) (f ` T)"
lp15@69922
   628
    shows "openin (top_of_set S) (S \<inter> f -` T) \<longleftrightarrow>
lp15@69922
   629
           openin (top_of_set (f ` S)) T"
immler@69616
   630
          (is "?lhs = ?rhs")
immler@69616
   631
proof
immler@69616
   632
  assume ?lhs
lp15@69922
   633
  then have *: "closedin (top_of_set S) (S - (S \<inter> f -` T))"
immler@69616
   634
    using closedin_diff by fastforce
immler@69616
   635
  have [simp]: "(f ` S - f ` (S - (S \<inter> f -` T))) = T"
immler@69616
   636
    using T by blast
immler@69616
   637
  show ?rhs
immler@69616
   638
    using ope [OF *, unfolded closedin_def] by auto
immler@69616
   639
next
immler@69616
   640
  assume ?rhs
immler@69616
   641
  with contf show ?lhs
immler@69616
   642
    by (auto simp: continuous_on_open)
immler@69616
   643
qed
immler@69616
   644
immler@69616
   645
lemma continuous_right_inverse_imp_quotient_map:
immler@69616
   646
  assumes contf: "continuous_on S f" and imf: "f ` S \<subseteq> T"
immler@69616
   647
      and contg: "continuous_on T g" and img: "g ` T \<subseteq> S"
immler@69616
   648
      and fg [simp]: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
immler@69616
   649
      and U: "U \<subseteq> T"
lp15@69922
   650
    shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@69922
   651
           openin (top_of_set T) U"
immler@69616
   652
          (is "?lhs = ?rhs")
immler@69616
   653
proof -
lp15@69922
   654
  have f: "\<And>Z. openin (top_of_set (f ` S)) Z \<Longrightarrow>
lp15@69922
   655
                openin (top_of_set S) (S \<inter> f -` Z)"
lp15@69922
   656
  and  g: "\<And>Z. openin (top_of_set (g ` T)) Z \<Longrightarrow>
lp15@69922
   657
                openin (top_of_set T) (T \<inter> g -` Z)"
immler@69616
   658
    using contf contg by (auto simp: continuous_on_open)
immler@69616
   659
  show ?thesis
immler@69616
   660
  proof
immler@69616
   661
    have "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = {x \<in> T. f (g x) \<in> U}"
immler@69616
   662
      using imf img by blast
immler@69616
   663
    also have "... = U"
immler@69616
   664
      using U by auto
immler@69616
   665
    finally have eq: "T \<inter> g -` (g ` T \<inter> (S \<inter> f -` U)) = U" .
immler@69616
   666
    assume ?lhs
lp15@69922
   667
    then have *: "openin (top_of_set (g ` T)) (g ` T \<inter> (S \<inter> f -` U))"
immler@69616
   668
      by (meson img openin_Int openin_subtopology_Int_subset openin_subtopology_self)
immler@69616
   669
    show ?rhs
immler@69616
   670
      using g [OF *] eq by auto
immler@69616
   671
  next
immler@69616
   672
    assume rhs: ?rhs
immler@69616
   673
    show ?lhs
immler@69616
   674
      by (metis f fg image_eqI image_subset_iff imf img openin_subopen openin_subtopology_self openin_trans rhs)
immler@69616
   675
  qed
immler@69616
   676
qed
immler@69616
   677
immler@69616
   678
lemma continuous_left_inverse_imp_quotient_map:
immler@69616
   679
  assumes "continuous_on S f"
immler@69616
   680
      and "continuous_on (f ` S) g"
immler@69616
   681
      and  "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
immler@69616
   682
      and "U \<subseteq> f ` S"
lp15@69922
   683
    shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@69922
   684
           openin (top_of_set (f ` S)) U"
immler@69616
   685
apply (rule continuous_right_inverse_imp_quotient_map)
immler@69616
   686
using assms apply force+
immler@69616
   687
done
immler@69616
   688
immler@69616
   689
lemma continuous_imp_quotient_map:
immler@69616
   690
  fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
immler@69616
   691
  assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
lp15@69922
   692
    shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
lp15@69922
   693
           openin (top_of_set T) U"
immler@69616
   694
  by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
immler@69616
   695
lp15@69922
   696
subsection%unimportant\<open>Pasting lemmas for functions, for of casewise definitions\<close>
immler@69616
   697
lp15@69922
   698
subsubsection\<open>on open sets\<close>
immler@69616
   699
immler@69616
   700
lemma pasting_lemma:
lp15@69922
   701
  assumes ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)"
lp15@69922
   702
      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
lp15@69922
   703
      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
lp15@69922
   704
      and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
lp15@69922
   705
    shows "continuous_map X Y g"
lp15@69922
   706
  unfolding continuous_map_openin_preimage_eq
lp15@69922
   707
proof (intro conjI allI impI)
lp15@69922
   708
  show "g ` topspace X \<subseteq> topspace Y"
lp15@69922
   709
    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
lp15@69922
   710
next
lp15@69922
   711
  fix U
lp15@69922
   712
  assume Y: "openin Y U"
lp15@69922
   713
  have T: "T i \<subseteq> topspace X" if "i \<in> I" for i
lp15@69922
   714
    using ope by (simp add: openin_subset that)
lp15@69922
   715
  have *: "topspace X \<inter> g -` U = (\<Union>i \<in> I. T i \<inter> f i -` U)"
lp15@69922
   716
    using f g T by fastforce
lp15@69922
   717
  have "\<And>i. i \<in> I \<Longrightarrow> openin X (T i \<inter> f i -` U)"
lp15@69922
   718
    using cont unfolding continuous_map_openin_preimage_eq
lp15@69922
   719
    by (metis Y T inf.commute inf_absorb1 ope topspace_subtopology openin_trans_full)
lp15@69922
   720
  then show "openin X (topspace X \<inter> g -` U)"
lp15@69922
   721
    by (auto simp: *)
immler@69616
   722
qed
immler@69616
   723
immler@69616
   724
lemma pasting_lemma_exists:
lp15@69922
   725
  assumes X: "topspace X \<subseteq> (\<Union>i \<in> I. T i)"
lp15@69922
   726
      and ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)"
lp15@69922
   727
      and cont: "\<And>i. i \<in> I \<Longrightarrow> continuous_map (subtopology X (T i)) Y (f i)"
lp15@69922
   728
      and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
lp15@69922
   729
    obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
immler@69616
   730
proof
lp15@69922
   731
  let ?h = "\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x"
lp15@69922
   732
  show "continuous_map X Y ?h"
lp15@69922
   733
    apply (rule pasting_lemma [OF ope cont])
immler@69616
   734
     apply (blast intro: f)+
lp15@69922
   735
    by (metis (no_types, lifting) UN_E X subsetD someI_ex)
lp15@69922
   736
  show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x" if "i \<in> I" "x \<in> topspace X \<inter> T i" for i x
lp15@69922
   737
    by (metis (no_types, lifting) IntD2 IntI f someI_ex that)
lp15@69922
   738
qed
lp15@69922
   739
lp15@69922
   740
lemma pasting_lemma_locally_finite:
lp15@69922
   741
  assumes fin: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>V. openin X V \<and> x \<in> V \<and> finite {i \<in> I. T i \<inter> V \<noteq> {}}"
lp15@69922
   742
    and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
lp15@69922
   743
    and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
lp15@69922
   744
    and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
lp15@69922
   745
    and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
lp15@69922
   746
  shows "continuous_map X Y g"
lp15@69922
   747
  unfolding continuous_map_closedin_preimage_eq
lp15@69922
   748
proof (intro conjI allI impI)
lp15@69922
   749
  show "g ` topspace X \<subseteq> topspace Y"
lp15@69922
   750
    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
lp15@69922
   751
next
lp15@69922
   752
  fix U
lp15@69922
   753
  assume Y: "closedin Y U"
lp15@69922
   754
  have T: "T i \<subseteq> topspace X" if "i \<in> I" for i
lp15@69922
   755
    using clo by (simp add: closedin_subset that)
lp15@69922
   756
  have *: "topspace X \<inter> g -` U = (\<Union>i \<in> I. T i \<inter> f i -` U)"
lp15@69922
   757
    using f g T by fastforce
lp15@69922
   758
  have cTf: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i \<inter> f i -` U)"
lp15@69922
   759
    using cont unfolding continuous_map_closedin_preimage_eq topspace_subtopology
lp15@69922
   760
    by (simp add: Int_absorb1 T Y clo closedin_closed_subtopology)
lp15@69922
   761
  have sub: "{Z \<in> (\<lambda>i. T i \<inter> f i -` U) ` I. Z \<inter> V \<noteq> {}}
lp15@69922
   762
           \<subseteq> (\<lambda>i. T i \<inter> f i -` U) ` {i \<in> I. T i \<inter> V \<noteq> {}}" for V
lp15@69922
   763
    by auto
lp15@69922
   764
  have 1: "(\<Union>i\<in>I. T i \<inter> f i -` U) \<subseteq> topspace X"
lp15@69922
   765
    using T by blast
lp15@69922
   766
  then have lf: "locally_finite_in X ((\<lambda>i. T i \<inter> f i -` U) ` I)"
lp15@69922
   767
    unfolding locally_finite_in_def
lp15@69922
   768
    using finite_subset [OF sub] fin by force
lp15@69922
   769
  show "closedin X (topspace X \<inter> g -` U)"
lp15@69922
   770
    apply (subst *)
lp15@69922
   771
    apply (rule closedin_locally_finite_Union)
lp15@69922
   772
     apply (auto intro: cTf lf)
immler@69616
   773
    done
lp15@69922
   774
qed
lp15@69922
   775
lp15@69922
   776
subsubsection\<open>Likewise on closed sets, with a finiteness assumption\<close>
lp15@69922
   777
lp15@69922
   778
lemma pasting_lemma_closed:
lp15@69922
   779
  assumes fin: "finite I"
lp15@69922
   780
    and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
lp15@69922
   781
    and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
lp15@69922
   782
    and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
lp15@69922
   783
    and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
lp15@69922
   784
  shows "continuous_map X Y g"
lp15@69922
   785
  using pasting_lemma_locally_finite [OF _ clo cont f g] fin by auto
lp15@69922
   786
lp15@69922
   787
lemma pasting_lemma_exists_locally_finite:
lp15@69922
   788
  assumes fin: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>V. openin X V \<and> x \<in> V \<and> finite {i \<in> I. T i \<inter> V \<noteq> {}}"
lp15@69922
   789
    and X: "topspace X \<subseteq> \<Union>(T ` I)"
lp15@69922
   790
    and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
lp15@69922
   791
    and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
lp15@69922
   792
    and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
lp15@69922
   793
    and g: "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>j. j \<in> I \<and> x \<in> T j \<and> g x = f j x"
lp15@69922
   794
  obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
lp15@69922
   795
proof
lp15@69922
   796
  show "continuous_map X Y (\<lambda>x. f(@i. i \<in> I \<and> x \<in> T i) x)"
lp15@69922
   797
    apply (rule pasting_lemma_locally_finite [OF fin])
lp15@69922
   798
        apply (blast intro: assms)+
lp15@69922
   799
    by (metis (no_types, lifting) UN_E X set_rev_mp someI_ex)
immler@69616
   800
next
immler@69616
   801
  fix x i
lp15@69922
   802
  assume "i \<in> I" and "x \<in> topspace X \<inter> T i"
lp15@69922
   803
  show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
lp15@69922
   804
    apply (rule someI2_ex)
lp15@69922
   805
    using \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> apply blast
lp15@69922
   806
    by (meson Int_iff \<open>i \<in> I\<close> \<open>x \<in> topspace X \<inter> T i\<close> f)
lp15@69922
   807
qed
lp15@69922
   808
lp15@69922
   809
lemma pasting_lemma_exists_closed:
lp15@69922
   810
  assumes fin: "finite I"
lp15@69922
   811
    and X: "topspace X \<subseteq> \<Union>(T ` I)"
lp15@69922
   812
    and clo: "\<And>i. i \<in> I \<Longrightarrow> closedin X (T i)"
lp15@69922
   813
    and cont:  "\<And>i. i \<in> I \<Longrightarrow> continuous_map(subtopology X (T i)) Y (f i)"
lp15@69922
   814
    and f: "\<And>i j x. \<lbrakk>i \<in> I; j \<in> I; x \<in> topspace X \<inter> T i \<inter> T j\<rbrakk> \<Longrightarrow> f i x = f j x"
lp15@69922
   815
  obtains g where "continuous_map X Y g" "\<And>x i. \<lbrakk>i \<in> I; x \<in> topspace X \<inter> T i\<rbrakk> \<Longrightarrow> g x = f i x"
lp15@69922
   816
proof
lp15@69922
   817
  show "continuous_map X Y (\<lambda>x. f (SOME i. i \<in> I \<and> x \<in> T i) x)"
lp15@69922
   818
    apply (rule pasting_lemma_closed [OF \<open>finite I\<close> clo cont])
lp15@69922
   819
     apply (blast intro: f)+
lp15@69922
   820
    by (metis (mono_tags, lifting) UN_iff X someI_ex subset_iff)
lp15@69922
   821
next
lp15@69922
   822
  fix x i
lp15@69922
   823
  assume "i \<in> I" "x \<in> topspace X \<inter> T i"
immler@69616
   824
  then show "f (SOME i. i \<in> I \<and> x \<in> T i) x = f i x"
immler@69616
   825
    by (metis (no_types, lifting) IntD2 IntI f someI_ex)
immler@69616
   826
qed
immler@69616
   827
lp15@69922
   828
lemma continuous_map_cases:
lp15@69922
   829
  assumes f: "continuous_map (subtopology X (X closure_of {x. P x})) Y f"
lp15@69922
   830
      and g: "continuous_map (subtopology X (X closure_of {x. \<not> P x})) Y g"
lp15@69922
   831
      and fg: "\<And>x. x \<in> X frontier_of {x. P x} \<Longrightarrow> f x = g x"
lp15@69922
   832
  shows "continuous_map X Y (\<lambda>x. if P x then f x else g x)"
lp15@69922
   833
proof (rule pasting_lemma_closed)
lp15@69922
   834
  let ?f = "\<lambda>b. if b then f else g"
lp15@69922
   835
  let ?g = "\<lambda>x. if P x then f x else g x"
lp15@69922
   836
  let ?T = "\<lambda>b. if b then X closure_of {x. P x} else X closure_of {x. ~P x}"
lp15@69922
   837
  show "finite {True,False}" by auto
lp15@69922
   838
  have eq: "topspace X - Collect P = topspace X \<inter> {x. \<not> P x}"
lp15@69922
   839
    by blast
lp15@69922
   840
  show "?f i x = ?f j x"
lp15@69922
   841
    if "i \<in> {True,False}" "j \<in> {True,False}" and x: "x \<in> topspace X \<inter> ?T i \<inter> ?T j" for i j x
lp15@69922
   842
  proof -
lp15@69922
   843
    have "f x = g x"
lp15@69922
   844
      if "i" "\<not> j"
lp15@69922
   845
      apply (rule fg)
lp15@69922
   846
      unfolding frontier_of_closures eq
lp15@69922
   847
      using x that closure_of_restrict by fastforce
lp15@69922
   848
    moreover
lp15@69922
   849
    have "g x = f x"
lp15@69922
   850
      if "x \<in> X closure_of {x. \<not> P x}" "x \<in> X closure_of Collect P" "\<not> i" "j" for x
lp15@69922
   851
        apply (rule fg [symmetric])
lp15@69922
   852
        unfolding frontier_of_closures eq
lp15@69922
   853
        using x that closure_of_restrict by fastforce
lp15@69922
   854
    ultimately show ?thesis
lp15@69922
   855
      using that by (auto simp flip: closure_of_restrict)
lp15@69922
   856
  qed
lp15@69922
   857
  show "\<exists>j. j \<in> {True,False} \<and> x \<in> ?T j \<and> (if P x then f x else g x) = ?f j x"
lp15@69922
   858
    if "x \<in> topspace X" for x
lp15@69922
   859
    apply simp
lp15@69922
   860
    apply safe
lp15@69922
   861
    apply (metis Int_iff closure_of inf_sup_absorb mem_Collect_eq that)
lp15@69922
   862
    by (metis DiffI eq closure_of_subset_Int contra_subsetD mem_Collect_eq that)
lp15@69922
   863
qed (auto simp: f g)
immler@69616
   864
lp15@69922
   865
lemma continuous_map_cases_alt:
lp15@69922
   866
  assumes f: "continuous_map (subtopology X (X closure_of {x \<in> topspace X. P x})) Y f"
lp15@69922
   867
      and g: "continuous_map (subtopology X (X closure_of {x \<in> topspace X. ~P x})) Y g"
lp15@69922
   868
      and fg: "\<And>x. x \<in> X frontier_of {x \<in> topspace X. P x} \<Longrightarrow> f x = g x"
lp15@69922
   869
    shows "continuous_map X Y (\<lambda>x. if P x then f x else g x)"
lp15@69922
   870
  apply (rule continuous_map_cases)
lp15@69922
   871
  using assms
lp15@69922
   872
    apply (simp_all add: Collect_conj_eq closure_of_restrict [symmetric] frontier_of_restrict [symmetric])
lp15@69922
   873
  done
lp15@69922
   874
lp15@69922
   875
lemma continuous_map_cases_function:
lp15@69922
   876
  assumes contp: "continuous_map X Z p"
lp15@69922
   877
    and contf: "continuous_map (subtopology X {x \<in> topspace X. p x \<in> Z closure_of U}) Y f"
lp15@69922
   878
    and contg: "continuous_map (subtopology X {x \<in> topspace X. p x \<in> Z closure_of (topspace Z - U)}) Y g"
lp15@69922
   879
    and fg: "\<And>x. \<lbrakk>x \<in> topspace X; p x \<in> Z frontier_of U\<rbrakk> \<Longrightarrow> f x = g x"
lp15@69922
   880
  shows "continuous_map X Y (\<lambda>x. if p x \<in> U then f x else g x)"
lp15@69922
   881
proof (rule continuous_map_cases_alt)
lp15@69922
   882
  show "continuous_map (subtopology X (X closure_of {x \<in> topspace X. p x \<in> U})) Y f"
lp15@69922
   883
  proof (rule continuous_map_from_subtopology_mono)
lp15@69922
   884
    let ?T = "{x \<in> topspace X. p x \<in> Z closure_of U}"
lp15@69922
   885
    show "continuous_map (subtopology X ?T) Y f"
lp15@69922
   886
      by (simp add: contf)
lp15@69922
   887
    show "X closure_of {x \<in> topspace X. p x \<in> U} \<subseteq> ?T"
lp15@69922
   888
      by (rule continuous_map_closure_preimage_subset [OF contp])
lp15@69922
   889
  qed
lp15@69922
   890
  show "continuous_map (subtopology X (X closure_of {x \<in> topspace X. p x \<notin> U})) Y g"
lp15@69922
   891
  proof (rule continuous_map_from_subtopology_mono)
lp15@69922
   892
    let ?T = "{x \<in> topspace X. p x \<in> Z closure_of (topspace Z - U)}"
lp15@69922
   893
    show "continuous_map (subtopology X ?T) Y g"
lp15@69922
   894
      by (simp add: contg)
lp15@69922
   895
    have "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> X closure_of {x \<in> topspace X. p x \<in> topspace Z - U}"
lp15@69922
   896
      apply (rule closure_of_mono)
lp15@69922
   897
      using continuous_map_closedin contp by fastforce
lp15@69922
   898
    then show "X closure_of {x \<in> topspace X. p x \<notin> U} \<subseteq> ?T"
lp15@69922
   899
      by (rule order_trans [OF _ continuous_map_closure_preimage_subset [OF contp]])
lp15@69922
   900
  qed
lp15@69922
   901
next
lp15@69922
   902
  show "f x = g x" if "x \<in> X frontier_of {x \<in> topspace X. p x \<in> U}" for x
lp15@69922
   903
    using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast
immler@69616
   904
qed
immler@69616
   905
nipkow@69750
   906
subsection \<open>Retractions\<close>
nipkow@69750
   907
nipkow@69750
   908
definition%important retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
nipkow@69750
   909
where "retraction S T r \<longleftrightarrow>
nipkow@69750
   910
  T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
nipkow@69750
   911
nipkow@69750
   912
definition%important retract_of (infixl "retract'_of" 50) where
nipkow@69750
   913
"T retract_of S  \<longleftrightarrow>  (\<exists>r. retraction S T r)"
nipkow@69750
   914
nipkow@69750
   915
lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
nipkow@69750
   916
  unfolding retraction_def by auto
nipkow@69750
   917
nipkow@69750
   918
text \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
nipkow@69750
   919
nipkow@69750
   920
lemma invertible_fixpoint_property:
nipkow@69750
   921
  fixes S :: "'a::topological_space set"
nipkow@69750
   922
    and T :: "'b::topological_space set"
nipkow@69750
   923
  assumes contt: "continuous_on T i"
nipkow@69750
   924
    and "i ` T \<subseteq> S"
nipkow@69750
   925
    and contr: "continuous_on S r"
nipkow@69750
   926
    and "r ` S \<subseteq> T"
nipkow@69750
   927
    and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
nipkow@69750
   928
    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
nipkow@69750
   929
    and contg: "continuous_on T g"
nipkow@69750
   930
    and "g ` T \<subseteq> T"
nipkow@69750
   931
  obtains y where "y \<in> T" and "g y = y"
nipkow@69750
   932
proof -
nipkow@69750
   933
  have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
nipkow@69750
   934
  proof (rule FP)
nipkow@69750
   935
    show "continuous_on S (i \<circ> g \<circ> r)"
nipkow@69750
   936
      by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
nipkow@69750
   937
    show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
nipkow@69750
   938
      using assms(2,4,8) by force
nipkow@69750
   939
  qed
nipkow@69750
   940
  then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
nipkow@69750
   941
  then have *: "g (r x) \<in> T"
nipkow@69750
   942
    using assms(4,8) by auto
nipkow@69750
   943
  have "r ((i \<circ> g \<circ> r) x) = r x"
nipkow@69750
   944
    using x by auto
nipkow@69750
   945
  then show ?thesis
nipkow@69750
   946
    using "*" ri that by auto
nipkow@69750
   947
qed
nipkow@69750
   948
nipkow@69750
   949
lemma homeomorphic_fixpoint_property:
nipkow@69750
   950
  fixes S :: "'a::topological_space set"
nipkow@69750
   951
    and T :: "'b::topological_space set"
nipkow@69750
   952
  assumes "S homeomorphic T"
nipkow@69750
   953
  shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
nipkow@69750
   954
         (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
nipkow@69750
   955
         (is "?lhs = ?rhs")
nipkow@69750
   956
proof -
nipkow@69750
   957
  obtain r i where r:
nipkow@69750
   958
      "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
nipkow@69750
   959
      "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
nipkow@69750
   960
    using assms unfolding homeomorphic_def homeomorphism_def  by blast
nipkow@69750
   961
  show ?thesis
nipkow@69750
   962
  proof
nipkow@69750
   963
    assume ?lhs
nipkow@69750
   964
    with r show ?rhs
nipkow@69750
   965
      by (metis invertible_fixpoint_property[of T i S r] order_refl)
nipkow@69750
   966
  next
nipkow@69750
   967
    assume ?rhs
nipkow@69750
   968
    with r show ?lhs
nipkow@69750
   969
      by (metis invertible_fixpoint_property[of S r T i] order_refl)
nipkow@69750
   970
  qed
nipkow@69750
   971
qed
nipkow@69750
   972
nipkow@69750
   973
lemma retract_fixpoint_property:
nipkow@69750
   974
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
nipkow@69750
   975
    and S :: "'a set"
nipkow@69750
   976
  assumes "T retract_of S"
nipkow@69750
   977
    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
nipkow@69750
   978
    and contg: "continuous_on T g"
nipkow@69750
   979
    and "g ` T \<subseteq> T"
nipkow@69750
   980
  obtains y where "y \<in> T" and "g y = y"
nipkow@69750
   981
proof -
nipkow@69750
   982
  obtain h where "retraction S T h"
nipkow@69750
   983
    using assms(1) unfolding retract_of_def ..
nipkow@69750
   984
  then show ?thesis
nipkow@69750
   985
    unfolding retraction_def
nipkow@69750
   986
    using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
nipkow@69750
   987
    by (metis assms(4) contg image_ident that)
nipkow@69750
   988
qed
nipkow@69750
   989
nipkow@69750
   990
lemma retraction:
nipkow@69750
   991
  "retraction S T r \<longleftrightarrow>
nipkow@69750
   992
    T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
nipkow@69750
   993
  by (force simp: retraction_def)
nipkow@69750
   994
wenzelm@69753
   995
lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
nipkow@69750
   996
  assumes "retraction S T r"
nipkow@69750
   997
  obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
nipkow@69750
   998
proof (rule that)
nipkow@69750
   999
  from retraction [of S T r] assms
nipkow@69750
  1000
  have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x"
nipkow@69750
  1001
    by simp_all
nipkow@69750
  1002
  then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r"
nipkow@69750
  1003
    by simp_all
nipkow@69750
  1004
  from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x
nipkow@69750
  1005
    using that by simp
nipkow@69750
  1006
  with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x
nipkow@69750
  1007
    using that by auto
nipkow@69750
  1008
qed
nipkow@69750
  1009
wenzelm@69753
  1010
lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
nipkow@69750
  1011
  assumes "T retract_of S"
nipkow@69750
  1012
  obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
nipkow@69750
  1013
proof -
nipkow@69750
  1014
  from assms obtain r where "retraction S T r"
nipkow@69750
  1015
    by (auto simp add: retract_of_def)
nipkow@69750
  1016
  with that show thesis
nipkow@69750
  1017
    by (auto elim: retractionE)
nipkow@69750
  1018
qed
nipkow@69750
  1019
nipkow@69750
  1020
lemma retract_of_imp_extensible:
nipkow@69750
  1021
  assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
nipkow@69750
  1022
  obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
nipkow@69750
  1023
proof -
nipkow@69750
  1024
  from \<open>S retract_of T\<close> obtain r where "retraction T S r"
nipkow@69750
  1025
    by (auto simp add: retract_of_def)
nipkow@69750
  1026
  show thesis
nipkow@69750
  1027
    by (rule that [of "f \<circ> r"])
nipkow@69750
  1028
      (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
nipkow@69750
  1029
qed
nipkow@69750
  1030
nipkow@69750
  1031
lemma idempotent_imp_retraction:
nipkow@69750
  1032
  assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
nipkow@69750
  1033
    shows "retraction S (f ` S) f"
nipkow@69750
  1034
by (simp add: assms retraction)
nipkow@69750
  1035
nipkow@69750
  1036
lemma retraction_subset:
nipkow@69750
  1037
  assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
nipkow@69750
  1038
  shows "retraction s' T r"
nipkow@69750
  1039
  unfolding retraction_def
nipkow@69750
  1040
  by (metis assms continuous_on_subset image_mono retraction)
nipkow@69750
  1041
nipkow@69750
  1042
lemma retract_of_subset:
nipkow@69750
  1043
  assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
nipkow@69750
  1044
    shows "T retract_of s'"
nipkow@69750
  1045
by (meson assms retract_of_def retraction_subset)
nipkow@69750
  1046
nipkow@69750
  1047
lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
nipkow@69750
  1048
by (simp add: retraction)
nipkow@69750
  1049
nipkow@69750
  1050
lemma retract_of_refl [iff]: "S retract_of S"
nipkow@69750
  1051
  unfolding retract_of_def retraction_def
nipkow@69750
  1052
  using continuous_on_id by blast
nipkow@69750
  1053
nipkow@69750
  1054
lemma retract_of_imp_subset:
nipkow@69750
  1055
   "S retract_of T \<Longrightarrow> S \<subseteq> T"
nipkow@69750
  1056
by (simp add: retract_of_def retraction_def)
nipkow@69750
  1057
nipkow@69750
  1058
lemma retract_of_empty [simp]:
nipkow@69750
  1059
     "({} retract_of S) \<longleftrightarrow> S = {}"  "(S retract_of {}) \<longleftrightarrow> S = {}"
nipkow@69750
  1060
by (auto simp: retract_of_def retraction_def)
nipkow@69750
  1061
nipkow@69750
  1062
lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
nipkow@69750
  1063
  unfolding retract_of_def retraction_def by force
nipkow@69750
  1064
nipkow@69750
  1065
lemma retraction_comp:
nipkow@69750
  1066
   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
nipkow@69750
  1067
        \<Longrightarrow> retraction S U (g \<circ> f)"
nipkow@69750
  1068
apply (auto simp: retraction_def intro: continuous_on_compose2)
nipkow@69750
  1069
by blast
nipkow@69750
  1070
nipkow@69750
  1071
lemma retract_of_trans [trans]:
nipkow@69750
  1072
  assumes "S retract_of T" and "T retract_of U"
nipkow@69750
  1073
    shows "S retract_of U"
nipkow@69750
  1074
using assms by (auto simp: retract_of_def intro: retraction_comp)
nipkow@69750
  1075
nipkow@69750
  1076
lemma closedin_retract:
nipkow@69750
  1077
  fixes S :: "'a :: t2_space set"
nipkow@69750
  1078
  assumes "S retract_of T"
lp15@69922
  1079
    shows "closedin (top_of_set T) S"
nipkow@69750
  1080
proof -
nipkow@69750
  1081
  obtain r where r: "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
nipkow@69750
  1082
    using assms by (auto simp: retract_of_def retraction_def)
nipkow@69750
  1083
  have "S = {x\<in>T. x = r x}"
nipkow@69750
  1084
    using r by auto
nipkow@69750
  1085
  also have "\<dots> = T \<inter> ((\<lambda>x. (x, r x)) -` ({y. \<exists>x. y = (x, x)}))"
nipkow@69750
  1086
    unfolding vimage_def mem_Times_iff fst_conv snd_conv
nipkow@69750
  1087
    using r
nipkow@69750
  1088
    by auto
nipkow@69750
  1089
  also have "closedin (top_of_set T) \<dots>"
nipkow@69750
  1090
    by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r)
nipkow@69750
  1091
  finally show ?thesis .
nipkow@69750
  1092
qed
nipkow@69750
  1093
lp15@69922
  1094
lemma closedin_self [simp]: "closedin (top_of_set S) S"
nipkow@69750
  1095
  by simp
nipkow@69750
  1096
nipkow@69750
  1097
lemma retract_of_closed:
nipkow@69750
  1098
    fixes S :: "'a :: t2_space set"
nipkow@69750
  1099
    shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
nipkow@69750
  1100
  by (metis closedin_retract closedin_closed_eq)
nipkow@69750
  1101
nipkow@69750
  1102
lemma retract_of_compact:
nipkow@69750
  1103
     "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
nipkow@69750
  1104
  by (metis compact_continuous_image retract_of_def retraction)
nipkow@69750
  1105
nipkow@69750
  1106
lemma retract_of_connected:
nipkow@69750
  1107
    "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
nipkow@69750
  1108
  by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
nipkow@69750
  1109
nipkow@69750
  1110
lemma retraction_imp_quotient_map:
lp15@69922
  1111
  "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
nipkow@69750
  1112
  if retraction: "retraction S T r" and "U \<subseteq> T"
nipkow@69750
  1113
  using retraction apply (rule retractionE)
nipkow@69750
  1114
  apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
nipkow@69750
  1115
  using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
nipkow@69750
  1116
  done
nipkow@69750
  1117
nipkow@69750
  1118
lemma retract_of_Times:
nipkow@69750
  1119
   "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
nipkow@69750
  1120
apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
nipkow@69750
  1121
apply (rename_tac f g)
nipkow@69750
  1122
apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
nipkow@69750
  1123
apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
nipkow@69750
  1124
done
nipkow@69750
  1125
lp15@69922
  1126
subsection\<open>Retractions on a topological space\<close>
lp15@69922
  1127
lp15@69922
  1128
definition retract_of_space :: "'a set \<Rightarrow> 'a topology \<Rightarrow> bool" (infix "retract'_of'_space" 50)
lp15@69922
  1129
  where "S retract_of_space X
lp15@69922
  1130
         \<equiv> S \<subseteq> topspace X \<and> (\<exists>r. continuous_map X (subtopology X S) r \<and> (\<forall>x \<in> S. r x = x))"
lp15@69922
  1131
lp15@69922
  1132
lemma retract_of_space_retraction_maps:
lp15@69922
  1133
   "S retract_of_space X \<longleftrightarrow> S \<subseteq> topspace X \<and> (\<exists>r. retraction_maps X (subtopology X S) r id)"
lp15@69922
  1134
  by (auto simp: retract_of_space_def retraction_maps_def)
lp15@69922
  1135
lp15@69922
  1136
lemma retract_of_space_section_map:
lp15@69922
  1137
   "S retract_of_space X \<longleftrightarrow> S \<subseteq> topspace X \<and> section_map (subtopology X S) X id"
lp15@69922
  1138
  unfolding retract_of_space_def retraction_maps_def section_map_def
lp15@69922
  1139
  by (auto simp: continuous_map_from_subtopology)
lp15@69922
  1140
lp15@69922
  1141
lemma retract_of_space_imp_subset:
lp15@69922
  1142
   "S retract_of_space X \<Longrightarrow> S \<subseteq> topspace X"
lp15@69922
  1143
  by (simp add: retract_of_space_def)
lp15@69922
  1144
lp15@69922
  1145
lemma retract_of_space_topspace:
lp15@69922
  1146
   "topspace X retract_of_space X"
lp15@69922
  1147
  using retract_of_space_def by force
lp15@69922
  1148
lp15@69922
  1149
lemma retract_of_space_empty [simp]:
lp15@69922
  1150
   "{} retract_of_space X \<longleftrightarrow> topspace X = {}"
lp15@69922
  1151
  by (auto simp: continuous_map_def retract_of_space_def)
lp15@69922
  1152
lp15@69922
  1153
lemma retract_of_space_singleton [simp]:
lp15@69922
  1154
  "{a} retract_of_space X \<longleftrightarrow> a \<in> topspace X"
lp15@69922
  1155
proof -
lp15@69922
  1156
  have "continuous_map X (subtopology X {a}) (\<lambda>x. a) \<and> (\<lambda>x. a) a = a" if "a \<in> topspace X"
lp15@69922
  1157
    using that by simp
lp15@69922
  1158
  then show ?thesis
lp15@69922
  1159
    by (force simp: retract_of_space_def)
lp15@69922
  1160
qed
lp15@69922
  1161
lp15@69922
  1162
lemma retract_of_space_clopen:
lp15@69922
  1163
  assumes "openin X S" "closedin X S" "S = {} \<Longrightarrow> topspace X = {}"
lp15@69922
  1164
  shows "S retract_of_space X"
lp15@69922
  1165
proof (cases "S = {}")
lp15@69922
  1166
  case False
lp15@69922
  1167
  then obtain a where "a \<in> S"
lp15@69922
  1168
    by blast
lp15@69922
  1169
  show ?thesis
lp15@69922
  1170
    unfolding retract_of_space_def
lp15@69922
  1171
  proof (intro exI conjI)
lp15@69922
  1172
    show "S \<subseteq> topspace X"
lp15@69922
  1173
      by (simp add: assms closedin_subset)
lp15@69922
  1174
    have "continuous_map X X (\<lambda>x. if x \<in> S then x else a)"
lp15@69922
  1175
    proof (rule continuous_map_cases)
lp15@69922
  1176
      show "continuous_map (subtopology X (X closure_of {x. x \<in> S})) X (\<lambda>x. x)"
lp15@69922
  1177
        by (simp add: continuous_map_from_subtopology)
lp15@69922
  1178
      show "continuous_map (subtopology X (X closure_of {x. x \<notin> S})) X (\<lambda>x. a)"
lp15@69922
  1179
        using \<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close> by force
lp15@69922
  1180
      show "x = a" if "x \<in> X frontier_of {x. x \<in> S}" for x
lp15@69922
  1181
        using assms that clopenin_eq_frontier_of by fastforce
lp15@69922
  1182
    qed
lp15@69922
  1183
    then show "continuous_map X (subtopology X S) (\<lambda>x. if x \<in> S then x else a)"
lp15@69922
  1184
      using \<open>S \<subseteq> topspace X\<close> \<open>a \<in> S\<close>  by (auto simp: continuous_map_in_subtopology)
lp15@69922
  1185
  qed auto
lp15@69922
  1186
qed (use assms in auto)
lp15@69922
  1187
lp15@69922
  1188
lemma retract_of_space_disjoint_union:
lp15@69922
  1189
  assumes "openin X S" "openin X T" and ST: "disjnt S T" "S \<union> T = topspace X" and "S = {} \<Longrightarrow> topspace X = {}"
lp15@69922
  1190
  shows "S retract_of_space X"
lp15@69922
  1191
proof (rule retract_of_space_clopen)
lp15@69922
  1192
  have "S \<inter> T = {}"
lp15@69922
  1193
    by (meson ST disjnt_def)
lp15@69922
  1194
  then have "S = topspace X - T"
lp15@69922
  1195
    using ST by auto
lp15@69922
  1196
  then show "closedin X S"
lp15@69922
  1197
    using \<open>openin X T\<close> by blast
lp15@69922
  1198
qed (auto simp: assms)
lp15@69922
  1199
lp15@69922
  1200
lemma retraction_maps_section_image1:
lp15@69922
  1201
  assumes "retraction_maps X Y r s"
lp15@69922
  1202
  shows "s ` (topspace Y) retract_of_space X"
lp15@69922
  1203
  unfolding retract_of_space_section_map
lp15@69922
  1204
proof
lp15@69922
  1205
  show "s ` topspace Y \<subseteq> topspace X"
lp15@69922
  1206
    using assms continuous_map_image_subset_topspace retraction_maps_def by blast
lp15@69922
  1207
  show "section_map (subtopology X (s ` topspace Y)) X id"
lp15@69922
  1208
    unfolding section_map_def
lp15@69922
  1209
    using assms retraction_maps_to_retract_maps by blast
lp15@69922
  1210
qed
lp15@69922
  1211
lp15@69922
  1212
lemma retraction_maps_section_image2:
lp15@69922
  1213
   "retraction_maps X Y r s
lp15@69922
  1214
        \<Longrightarrow> subtopology X (s ` (topspace Y)) homeomorphic_space Y"
lp15@69922
  1215
  using embedding_map_imp_homeomorphic_space homeomorphic_space_sym section_imp_embedding_map
lp15@69922
  1216
        section_map_def by blast
lp15@69922
  1217
lp15@69922
  1218
subsection\<open>Paths and path-connectedness\<close>
lp15@69922
  1219
lp15@69922
  1220
definition pathin :: "'a topology \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool" where
lp15@69922
  1221
   "pathin X g \<equiv> continuous_map (subtopology euclideanreal {0..1}) X g"
lp15@69922
  1222
lp15@69922
  1223
lemma pathin_compose:
lp15@69922
  1224
     "\<lbrakk>pathin X g; continuous_map X Y f\<rbrakk> \<Longrightarrow> pathin Y (f \<circ> g)"
lp15@69922
  1225
   by (simp add: continuous_map_compose pathin_def)
lp15@69922
  1226
lp15@69922
  1227
lemma pathin_subtopology:
lp15@69922
  1228
     "pathin (subtopology X S) g \<longleftrightarrow> pathin X g \<and> (\<forall>x \<in> {0..1}. g x \<in> S)"
lp15@69922
  1229
  by (auto simp: pathin_def continuous_map_in_subtopology)
lp15@69922
  1230
lp15@69922
  1231
lemma pathin_const:
lp15@69922
  1232
   "pathin X (\<lambda>x. a) \<longleftrightarrow> a \<in> topspace X"
lp15@69922
  1233
  by (simp add: pathin_def)
lp15@69939
  1234
   
lp15@69939
  1235
lemma path_start_in_topspace: "pathin X g \<Longrightarrow> g 0 \<in> topspace X"
lp15@69939
  1236
  by (force simp: pathin_def continuous_map)
lp15@69939
  1237
lp15@69939
  1238
lemma path_finish_in_topspace: "pathin X g \<Longrightarrow> g 1 \<in> topspace X"
lp15@69939
  1239
  by (force simp: pathin_def continuous_map)
lp15@69939
  1240
lp15@69939
  1241
lemma path_image_subset_topspace: "pathin X g \<Longrightarrow> g ` ({0..1}) \<subseteq> topspace X"
lp15@69939
  1242
  by (force simp: pathin_def continuous_map)
lp15@69922
  1243
lp15@69922
  1244
definition path_connected_space :: "'a topology \<Rightarrow> bool"
lp15@69922
  1245
  where "path_connected_space X \<equiv> \<forall>x \<in> topspace X. \<forall> y \<in> topspace X. \<exists>g. pathin X g \<and> g 0 = x \<and> g 1 = y"
lp15@69922
  1246
lp15@69922
  1247
definition path_connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool"
lp15@69922
  1248
  where "path_connectedin X S \<equiv> S \<subseteq> topspace X \<and> path_connected_space(subtopology X S)"
lp15@69922
  1249
lp15@69922
  1250
lemma path_connectedin_absolute [simp]:
lp15@69922
  1251
     "path_connectedin (subtopology X S) S \<longleftrightarrow> path_connectedin X S"
lp15@69922
  1252
  by (simp add: path_connectedin_def subtopology_subtopology topspace_subtopology)
lp15@69922
  1253
lp15@69922
  1254
lemma path_connectedin_subset_topspace:
lp15@69922
  1255
     "path_connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
lp15@69922
  1256
  by (simp add: path_connectedin_def)
lp15@69922
  1257
lp15@69922
  1258
lemma path_connectedin_subtopology:
lp15@69922
  1259
     "path_connectedin (subtopology X S) T \<longleftrightarrow> path_connectedin X T \<and> T \<subseteq> S"
lp15@69922
  1260
  by (auto simp: path_connectedin_def subtopology_subtopology topspace_subtopology inf.absorb2)
lp15@69922
  1261
lp15@69922
  1262
lemma path_connectedin:
lp15@69922
  1263
     "path_connectedin X S \<longleftrightarrow>
lp15@69922
  1264
        S \<subseteq> topspace X \<and>
lp15@69922
  1265
        (\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> S \<and> g 0 = x \<and> g 1 = y)"
lp15@69922
  1266
  unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology
lp15@69922
  1267
  by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 topspace_subtopology)
lp15@69922
  1268
lp15@69922
  1269
lemma path_connectedin_topspace:
lp15@69922
  1270
     "path_connectedin X (topspace X) \<longleftrightarrow> path_connected_space X"
lp15@69922
  1271
  by (simp add: path_connectedin_def)
lp15@69922
  1272
lp15@69922
  1273
lemma path_connected_imp_connected_space:
lp15@69922
  1274
  assumes "path_connected_space X"
lp15@69922
  1275
  shows "connected_space X"
lp15@69922
  1276
proof -
lp15@69922
  1277
  have *: "\<exists>S. connectedin X S \<and> g 0 \<in> S \<and> g 1 \<in> S" if "pathin X g" for g
lp15@69922
  1278
  proof (intro exI conjI)
lp15@69922
  1279
    have "continuous_map (subtopology euclideanreal {0..1}) X g"
lp15@69922
  1280
      using connectedin_absolute that by (simp add: pathin_def)
lp15@69922
  1281
    then show "connectedin X (g ` {0..1})"
lp15@69922
  1282
      by (rule connectedin_continuous_map_image) auto
lp15@69922
  1283
  qed auto
lp15@69922
  1284
  show ?thesis
lp15@69922
  1285
    using assms
lp15@69922
  1286
    by (auto intro: * simp add: path_connected_space_def connected_space_subconnected Ball_def)
lp15@69922
  1287
qed
lp15@69922
  1288
lp15@69922
  1289
lemma path_connectedin_imp_connectedin:
lp15@69922
  1290
     "path_connectedin X S \<Longrightarrow> connectedin X S"
lp15@69922
  1291
  by (simp add: connectedin_def path_connected_imp_connected_space path_connectedin_def)
lp15@69922
  1292
lp15@69922
  1293
lemma path_connected_space_topspace_empty:
lp15@69922
  1294
     "topspace X = {} \<Longrightarrow> path_connected_space X"
lp15@69922
  1295
  by (simp add: path_connected_space_def)
lp15@69922
  1296
lp15@69922
  1297
lemma path_connectedin_empty [simp]: "path_connectedin X {}"
lp15@69922
  1298
  by (simp add: path_connectedin)
lp15@69922
  1299
lp15@69922
  1300
lemma path_connectedin_singleton [simp]: "path_connectedin X {a} \<longleftrightarrow> a \<in> topspace X"
lp15@69922
  1301
proof
lp15@69922
  1302
  show "path_connectedin X {a} \<Longrightarrow> a \<in> topspace X"
lp15@69922
  1303
    by (simp add: path_connectedin)
lp15@69922
  1304
  show "a \<in> topspace X \<Longrightarrow> path_connectedin X {a}"
lp15@69922
  1305
    unfolding path_connectedin
lp15@69922
  1306
    using pathin_const by fastforce
lp15@69922
  1307
qed
lp15@69922
  1308
lp15@69922
  1309
lemma path_connectedin_continuous_map_image:
lp15@69922
  1310
  assumes f: "continuous_map X Y f" and S: "path_connectedin X S"
lp15@69922
  1311
  shows "path_connectedin Y (f ` S)"
lp15@69922
  1312
proof -
lp15@69922
  1313
  have fX: "f ` (topspace X) \<subseteq> topspace Y"
lp15@69922
  1314
    by (metis f continuous_map_image_subset_topspace)
lp15@69922
  1315
  show ?thesis
lp15@69922
  1316
    unfolding path_connectedin
lp15@69922
  1317
  proof (intro conjI ballI; clarify?)
lp15@69922
  1318
    fix x
lp15@69922
  1319
    assume "x \<in> S"
lp15@69922
  1320
    show "f x \<in> topspace Y"
lp15@69922
  1321
      by (meson S fX \<open>x \<in> S\<close> image_subset_iff path_connectedin_subset_topspace set_mp)
lp15@69922
  1322
  next
lp15@69922
  1323
    fix x y
lp15@69922
  1324
    assume "x \<in> S" and "y \<in> S"
lp15@69922
  1325
    then obtain g where g: "pathin X g" "g ` {0..1} \<subseteq> S" "g 0 = x" "g 1 = y"
lp15@69922
  1326
      using S  by (force simp: path_connectedin)
lp15@69922
  1327
    show "\<exists>g. pathin Y g \<and> g ` {0..1} \<subseteq> f ` S \<and> g 0 = f x \<and> g 1 = f y"
lp15@69922
  1328
    proof (intro exI conjI)
lp15@69922
  1329
      show "pathin Y (f \<circ> g)"
lp15@69922
  1330
        using \<open>pathin X g\<close> f pathin_compose by auto
lp15@69922
  1331
    qed (use g in auto)
lp15@69922
  1332
  qed
lp15@69922
  1333
qed
lp15@69922
  1334
lp15@69939
  1335
lemma path_connectedin_discrete_topology:
lp15@69939
  1336
  "path_connectedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U \<and> (\<exists>a. S \<subseteq> {a})"
lp15@69939
  1337
  apply safe
lp15@69939
  1338
  using path_connectedin_subset_topspace apply fastforce
lp15@69939
  1339
   apply (meson connectedin_discrete_topology path_connectedin_imp_connectedin)
lp15@69939
  1340
  using subset_singletonD by fastforce
lp15@69939
  1341
lp15@69939
  1342
lemma path_connected_space_discrete_topology:
lp15@69939
  1343
   "path_connected_space (discrete_topology U) \<longleftrightarrow> (\<exists>a. U \<subseteq> {a})"
lp15@69939
  1344
  by (metis path_connectedin_discrete_topology path_connectedin_topspace path_connected_space_topspace_empty
lp15@69939
  1345
            subset_singletonD topspace_discrete_topology)
lp15@69939
  1346
lp15@69939
  1347
lp15@69922
  1348
lemma homeomorphic_path_connected_space_imp:
lp15@69922
  1349
     "\<lbrakk>path_connected_space X; X homeomorphic_space Y\<rbrakk> \<Longrightarrow> path_connected_space Y"
lp15@69922
  1350
  unfolding homeomorphic_space_def homeomorphic_maps_def
lp15@69922
  1351
  by (metis (no_types, hide_lams) continuous_map_closedin continuous_map_image_subset_topspace imageI order_class.order.antisym path_connectedin_continuous_map_image path_connectedin_topspace subsetI)
lp15@69922
  1352
lp15@69922
  1353
lemma homeomorphic_path_connected_space:
lp15@69922
  1354
   "X homeomorphic_space Y \<Longrightarrow> path_connected_space X \<longleftrightarrow> path_connected_space Y"
lp15@69922
  1355
  by (meson homeomorphic_path_connected_space_imp homeomorphic_space_sym)
lp15@69922
  1356
lp15@69922
  1357
lemma homeomorphic_map_path_connectedness:
lp15@69922
  1358
  assumes "homeomorphic_map X Y f" "U \<subseteq> topspace X"
lp15@69922
  1359
  shows "path_connectedin Y (f ` U) \<longleftrightarrow> path_connectedin X U"
lp15@69922
  1360
  unfolding path_connectedin_def
lp15@69922
  1361
proof (intro conj_cong homeomorphic_path_connected_space)
lp15@69922
  1362
  show "(f ` U \<subseteq> topspace Y) = (U \<subseteq> topspace X)"
lp15@69922
  1363
    using assms homeomorphic_imp_surjective_map by blast
lp15@69922
  1364
next
lp15@69922
  1365
  assume "U \<subseteq> topspace X"
lp15@69922
  1366
  show "subtopology Y (f ` U) homeomorphic_space subtopology X U"
lp15@69922
  1367
    using assms unfolding homeomorphic_eq_everything_map
lp15@69922
  1368
    by (metis (no_types, hide_lams) assms homeomorphic_map_subtopologies homeomorphic_space homeomorphic_space_sym image_mono inf.absorb_iff2)
lp15@69922
  1369
qed
lp15@69922
  1370
lp15@69922
  1371
lemma homeomorphic_map_path_connectedness_eq:
lp15@69922
  1372
   "homeomorphic_map X Y f \<Longrightarrow> path_connectedin X U \<longleftrightarrow> U \<subseteq> topspace X \<and> path_connectedin Y (f ` U)"
lp15@69922
  1373
  by (meson homeomorphic_map_path_connectedness path_connectedin_def)
lp15@69922
  1374
lp15@69922
  1375
subsection\<open>Connected components\<close>
lp15@69922
  1376
lp15@69922
  1377
definition connected_component_of :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
lp15@69922
  1378
  where "connected_component_of X x y \<equiv>
lp15@69922
  1379
        \<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> T"
lp15@69922
  1380
lp15@69922
  1381
abbreviation connected_component_of_set
lp15@69922
  1382
  where "connected_component_of_set X x \<equiv> Collect (connected_component_of X x)"
lp15@69922
  1383
lp15@69922
  1384
definition connected_components_of :: "'a topology \<Rightarrow> ('a set) set"
lp15@69922
  1385
  where "connected_components_of X \<equiv> connected_component_of_set X ` topspace X"
lp15@69922
  1386
lp15@69922
  1387
lemma connected_component_in_topspace:
lp15@69922
  1388
   "connected_component_of X x y \<Longrightarrow> x \<in> topspace X \<and> y \<in> topspace X"
lp15@69922
  1389
  by (meson connected_component_of_def connectedin_subset_topspace in_mono)
lp15@69922
  1390
lp15@69922
  1391
lemma connected_component_of_refl:
lp15@69922
  1392
   "connected_component_of X x x \<longleftrightarrow> x \<in> topspace X"
lp15@69922
  1393
  by (meson connected_component_in_topspace connected_component_of_def connectedin_sing insertI1)
lp15@69922
  1394
lp15@69922
  1395
lemma connected_component_of_sym:
lp15@69922
  1396
   "connected_component_of X x y \<longleftrightarrow> connected_component_of X y x"
lp15@69922
  1397
  by (meson connected_component_of_def)
lp15@69922
  1398
lp15@69922
  1399
lemma connected_component_of_trans:
lp15@69922
  1400
   "\<lbrakk>connected_component_of X x y; connected_component_of X y z\<rbrakk>
lp15@69922
  1401
        \<Longrightarrow> connected_component_of X x z"
lp15@69922
  1402
  unfolding connected_component_of_def
lp15@69922
  1403
  using connectedin_Un by fastforce
lp15@69922
  1404
lp15@69922
  1405
lemma connected_component_of_mono:
lp15@69922
  1406
   "\<lbrakk>connected_component_of (subtopology X S) x y; S \<subseteq> T\<rbrakk>
lp15@69922
  1407
        \<Longrightarrow> connected_component_of (subtopology X T) x y"
lp15@69922
  1408
  by (metis connected_component_of_def connectedin_subtopology inf.absorb_iff2 subtopology_subtopology)
lp15@69922
  1409
lp15@69922
  1410
lemma connected_component_of_set:
lp15@69922
  1411
   "connected_component_of_set X x = {y. \<exists>T. connectedin X T \<and> x \<in> T \<and> y \<in> T}"
lp15@69922
  1412
  by (meson connected_component_of_def)
lp15@69922
  1413
lp15@69922
  1414
lemma connected_component_of_subset_topspace:
lp15@69922
  1415
   "connected_component_of_set X x \<subseteq> topspace X"
lp15@69922
  1416
  using connected_component_in_topspace by force
lp15@69922
  1417
lp15@69922
  1418
lemma connected_component_of_eq_empty:
lp15@69922
  1419
   "connected_component_of_set X x = {} \<longleftrightarrow> (x \<notin> topspace X)"
lp15@69922
  1420
  using connected_component_in_topspace connected_component_of_refl by fastforce
lp15@69922
  1421
lp15@69922
  1422
lemma connected_space_iff_connected_component:
lp15@69922
  1423
   "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. connected_component_of X x y)"
lp15@69922
  1424
  by (simp add: connected_component_of_def connected_space_subconnected)
lp15@69922
  1425
lp15@69922
  1426
lemma connected_space_imp_connected_component_of:
lp15@69922
  1427
   "\<lbrakk>connected_space X; a \<in> topspace X; b \<in> topspace X\<rbrakk>
lp15@69922
  1428
    \<Longrightarrow> connected_component_of X a b"
lp15@69922
  1429
  by (simp add: connected_space_iff_connected_component)
lp15@69922
  1430
lp15@69922
  1431
lemma connected_space_connected_component_set:
lp15@69922
  1432
   "connected_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. connected_component_of_set X x = topspace X)"
lp15@69922
  1433
  using connected_component_of_subset_topspace connected_space_iff_connected_component by fastforce
lp15@69922
  1434
lp15@69922
  1435
lemma connected_component_of_maximal:
lp15@69922
  1436
   "\<lbrakk>connectedin X S; x \<in> S\<rbrakk> \<Longrightarrow> S \<subseteq> connected_component_of_set X x"
lp15@69922
  1437
  by (meson Ball_Collect connected_component_of_def)
lp15@69922
  1438
lp15@69922
  1439
lemma connected_component_of_equiv:
lp15@69922
  1440
   "connected_component_of X x y \<longleftrightarrow>
lp15@69922
  1441
    x \<in> topspace X \<and> y \<in> topspace X \<and> connected_component_of X x = connected_component_of X y"
lp15@69922
  1442
  apply (simp add: connected_component_in_topspace fun_eq_iff)
lp15@69922
  1443
  by (meson connected_component_of_refl connected_component_of_sym connected_component_of_trans)
lp15@69922
  1444
lp15@69922
  1445
lemma connected_component_of_disjoint:
lp15@69922
  1446
   "disjnt (connected_component_of_set X x) (connected_component_of_set X y)
lp15@69922
  1447
    \<longleftrightarrow> ~(connected_component_of X x y)"
lp15@69922
  1448
  using connected_component_of_equiv unfolding disjnt_iff by force
lp15@69922
  1449
lp15@69922
  1450
lemma connected_component_of_eq:
lp15@69922
  1451
   "connected_component_of X x = connected_component_of X y \<longleftrightarrow>
lp15@69922
  1452
        (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
lp15@69922
  1453
        x \<in> topspace X \<and> y \<in> topspace X \<and>
lp15@69922
  1454
        connected_component_of X x y"
lp15@69922
  1455
  by (metis Collect_empty_eq_bot connected_component_of_eq_empty connected_component_of_equiv)
lp15@69922
  1456
lp15@69922
  1457
lemma connectedin_connected_component_of:
lp15@69922
  1458
   "connectedin X (connected_component_of_set X x)"
lp15@69922
  1459
proof -
lp15@69922
  1460
  have "connected_component_of_set X x = \<Union> {T. connectedin X T \<and> x \<in> T}"
lp15@69922
  1461
    by (auto simp: connected_component_of_def)
lp15@69922
  1462
  then show ?thesis
lp15@69922
  1463
    apply (rule ssubst)
lp15@69922
  1464
    by (blast intro: connectedin_Union)
lp15@69922
  1465
qed
lp15@69922
  1466
lp15@69922
  1467
lp15@69922
  1468
lemma Union_connected_components_of:
lp15@69922
  1469
   "\<Union>(connected_components_of X) = topspace X"
lp15@69922
  1470
  unfolding connected_components_of_def
lp15@69922
  1471
  apply (rule equalityI)
lp15@69922
  1472
  apply (simp add: SUP_least connected_component_of_subset_topspace)
lp15@69922
  1473
  using connected_component_of_refl by fastforce
lp15@69922
  1474
lp15@69922
  1475
lemma connected_components_of_maximal:
lp15@69922
  1476
   "\<lbrakk>C \<in> connected_components_of X; connectedin X S; ~disjnt C S\<rbrakk> \<Longrightarrow> S \<subseteq> C"
lp15@69922
  1477
  unfolding connected_components_of_def disjnt_def
lp15@69922
  1478
  apply clarify
lp15@69922
  1479
  by (metis Int_emptyI connected_component_of_def connected_component_of_trans mem_Collect_eq)
lp15@69922
  1480
lp15@69922
  1481
lemma pairwise_disjoint_connected_components_of:
lp15@69922
  1482
   "pairwise disjnt (connected_components_of X)"
lp15@69922
  1483
  unfolding connected_components_of_def pairwise_def
lp15@69922
  1484
  apply clarify
lp15@69922
  1485
  by (metis connected_component_of_disjoint connected_component_of_equiv)
lp15@69922
  1486
lp15@69922
  1487
lemma complement_connected_components_of_Union:
lp15@69922
  1488
   "C \<in> connected_components_of X
lp15@69922
  1489
      \<Longrightarrow> topspace X - C = \<Union> (connected_components_of X - {C})"
lp15@69922
  1490
  apply (rule equalityI)
lp15@69922
  1491
  using Union_connected_components_of apply fastforce
lp15@69922
  1492
  by (metis Diff_cancel Diff_subset Union_connected_components_of cSup_singleton diff_Union_pairwise_disjoint equalityE insert_subsetI pairwise_disjoint_connected_components_of)
lp15@69922
  1493
lp15@69922
  1494
lemma nonempty_connected_components_of:
lp15@69922
  1495
   "C \<in> connected_components_of X \<Longrightarrow> C \<noteq> {}"
lp15@69922
  1496
  unfolding connected_components_of_def
lp15@69922
  1497
  by (metis (no_types, lifting) connected_component_of_eq_empty imageE)
lp15@69922
  1498
lp15@69922
  1499
lemma connected_components_of_subset:
lp15@69922
  1500
   "C \<in> connected_components_of X \<Longrightarrow> C \<subseteq> topspace X"
lp15@69922
  1501
  using Union_connected_components_of by fastforce
lp15@69922
  1502
lp15@69922
  1503
lemma connectedin_connected_components_of:
lp15@69922
  1504
  assumes "C \<in> connected_components_of X"
lp15@69922
  1505
  shows "connectedin X C"
lp15@69922
  1506
proof -
lp15@69922
  1507
  have "C \<in> connected_component_of_set X ` topspace X"
lp15@69922
  1508
    using assms connected_components_of_def by blast
lp15@69922
  1509
then show ?thesis
lp15@69922
  1510
  using connectedin_connected_component_of by fastforce
lp15@69922
  1511
qed
lp15@69922
  1512
lp15@69922
  1513
lemma connected_component_in_connected_components_of:
lp15@69922
  1514
   "connected_component_of_set X a \<in> connected_components_of X \<longleftrightarrow> a \<in> topspace X"
lp15@69922
  1515
  apply (rule iffI)
lp15@69922
  1516
  using connected_component_of_eq_empty nonempty_connected_components_of apply fastforce
lp15@69922
  1517
  by (simp add: connected_components_of_def)
lp15@69922
  1518
lp15@69922
  1519
lemma connected_space_iff_components_eq:
lp15@69922
  1520
   "connected_space X \<longleftrightarrow> (\<forall>C \<in> connected_components_of X. \<forall>C' \<in> connected_components_of X. C = C')"
lp15@69922
  1521
  apply (rule iffI)
lp15@69922
  1522
  apply (force simp: connected_components_of_def connected_space_connected_component_set image_iff)
lp15@69922
  1523
  by (metis connected_component_in_connected_components_of connected_component_of_refl connected_space_iff_connected_component mem_Collect_eq)
lp15@69922
  1524
lp15@69922
  1525
lemma connected_components_of_eq_empty:
lp15@69922
  1526
   "connected_components_of X = {} \<longleftrightarrow> topspace X = {}"
lp15@69922
  1527
  by (simp add: connected_components_of_def)
lp15@69922
  1528
lp15@69922
  1529
lemma connected_components_of_empty_space:
lp15@69922
  1530
   "topspace X = {} \<Longrightarrow> connected_components_of X = {}"
lp15@69922
  1531
  by (simp add: connected_components_of_eq_empty)
lp15@69922
  1532
lp15@69922
  1533
lemma connected_components_of_subset_sing:
lp15@69922
  1534
   "connected_components_of X \<subseteq> {S} \<longleftrightarrow> connected_space X \<and> (topspace X = {} \<or> topspace X = S)"
lp15@69922
  1535
proof (cases "topspace X = {}")
lp15@69922
  1536
  case True
lp15@69922
  1537
  then show ?thesis
lp15@69922
  1538
    by (simp add: connected_components_of_empty_space connected_space_topspace_empty)
lp15@69922
  1539
next
lp15@69922
  1540
  case False
lp15@69922
  1541
  then show ?thesis
lp15@69922
  1542
    by (metis (no_types, hide_lams) Union_connected_components_of ccpo_Sup_singleton
lp15@69922
  1543
        connected_components_of_eq_empty connected_space_iff_components_eq insertI1 singletonD
lp15@69922
  1544
        subsetI subset_singleton_iff)
lp15@69922
  1545
qed
lp15@69922
  1546
lp15@69922
  1547
lemma connected_space_iff_components_subset_singleton:
lp15@69922
  1548
   "connected_space X \<longleftrightarrow> (\<exists>a. connected_components_of X \<subseteq> {a})"
lp15@69922
  1549
  by (simp add: connected_components_of_subset_sing)
lp15@69922
  1550
lp15@69922
  1551
lemma connected_components_of_eq_singleton:
lp15@69922
  1552
   "connected_components_of X = {S}
lp15@69922
  1553
\<longleftrightarrow> connected_space X \<and> topspace X \<noteq> {} \<and> S = topspace X"
lp15@69922
  1554
  by (metis ccpo_Sup_singleton connected_components_of_subset_sing insert_not_empty subset_singleton_iff)
lp15@69922
  1555
lp15@69922
  1556
lemma connected_components_of_connected_space:
lp15@69922
  1557
   "connected_space X \<Longrightarrow> connected_components_of X = (if topspace X = {} then {} else {topspace X})"
lp15@69922
  1558
  by (simp add: connected_components_of_eq_empty connected_components_of_eq_singleton)
lp15@69922
  1559
lp15@69922
  1560
lemma exists_connected_component_of_superset:
lp15@69922
  1561
  assumes "connectedin X S" and ne: "topspace X \<noteq> {}"
lp15@69922
  1562
  shows "\<exists>C. C \<in> connected_components_of X \<and> S \<subseteq> C"
lp15@69922
  1563
proof (cases "S = {}")
lp15@69922
  1564
  case True
lp15@69922
  1565
  then show ?thesis
lp15@69922
  1566
    using ne connected_components_of_def by blast
lp15@69922
  1567
next
lp15@69922
  1568
  case False
lp15@69922
  1569
  then show ?thesis
lp15@69922
  1570
    by (meson all_not_in_conv assms(1) connected_component_in_connected_components_of connected_component_of_maximal connectedin_subset_topspace in_mono)
lp15@69922
  1571
qed
lp15@69922
  1572
lp15@69922
  1573
lemma closedin_connected_components_of:
lp15@69922
  1574
  assumes "C \<in> connected_components_of X"
lp15@69922
  1575
  shows   "closedin X C"
lp15@69922
  1576
proof -
lp15@69922
  1577
  obtain x where "x \<in> topspace X" and x: "C = connected_component_of_set X x"
lp15@69922
  1578
    using assms by (auto simp: connected_components_of_def)
lp15@69922
  1579
  have "connected_component_of_set X x \<subseteq> topspace X"
lp15@69922
  1580
    by (simp add: connected_component_of_subset_topspace)
lp15@69922
  1581
  moreover have "X closure_of connected_component_of_set X x \<subseteq> connected_component_of_set X x"
lp15@69922
  1582
  proof (rule connected_component_of_maximal)
lp15@69922
  1583
    show "connectedin X (X closure_of connected_component_of_set X x)"
lp15@69922
  1584
      by (simp add: connectedin_closure_of connectedin_connected_component_of)
lp15@69922
  1585
    show "x \<in> X closure_of connected_component_of_set X x"
lp15@69922
  1586
      by (simp add: \<open>x \<in> topspace X\<close> closure_of connected_component_of_refl)
lp15@69922
  1587
  qed
lp15@69922
  1588
  ultimately
lp15@69922
  1589
  show ?thesis
lp15@69922
  1590
    using closure_of_subset_eq x by auto
lp15@69922
  1591
qed
lp15@69922
  1592
lp15@69922
  1593
lemma closedin_connected_component_of:
lp15@69922
  1594
   "closedin X (connected_component_of_set X x)"
lp15@69922
  1595
  by (metis closedin_connected_components_of closedin_empty connected_component_in_connected_components_of connected_component_of_eq_empty)
lp15@69922
  1596
lp15@69922
  1597
lemma connected_component_of_eq_overlap:
lp15@69922
  1598
   "connected_component_of_set X x = connected_component_of_set X y \<longleftrightarrow>
lp15@69922
  1599
      (x \<notin> topspace X) \<and> (y \<notin> topspace X) \<or>
lp15@69922
  1600
      ~(connected_component_of_set X x \<inter> connected_component_of_set X y = {})"
lp15@69922
  1601
  using connected_component_of_equiv by fastforce
lp15@69922
  1602
lp15@69922
  1603
lemma connected_component_of_nonoverlap:
lp15@69922
  1604
   "connected_component_of_set X x \<inter> connected_component_of_set X y = {} \<longleftrightarrow>
lp15@69922
  1605
     (x \<notin> topspace X) \<or> (y \<notin> topspace X) \<or>
lp15@69922
  1606
     ~(connected_component_of_set X x = connected_component_of_set X y)"
lp15@69922
  1607
  by (metis connected_component_of_eq_empty connected_component_of_eq_overlap inf.idem)
lp15@69922
  1608
lp15@69922
  1609
lemma connected_component_of_overlap:
lp15@69922
  1610
   "~(connected_component_of_set X x \<inter> connected_component_of_set X y = {}) \<longleftrightarrow>
lp15@69922
  1611
    x \<in> topspace X \<and> y \<in> topspace X \<and>
lp15@69922
  1612
    connected_component_of_set X x = connected_component_of_set X y"
lp15@69922
  1613
  by (meson connected_component_of_nonoverlap)
lp15@69922
  1614
lp15@69922
  1615
immler@69616
  1616
end