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