New results in topology, mostly from HOL Light's moretop.ml
authorpaulson <lp15@cam.ac.uk>
Mon Oct 30 16:02:59 2017 +0000 (18 months ago)
changeset 6693904678058308f
parent 66935 d0f12783cd80
child 66940 e5776e8e152b
New results in topology, mostly from HOL Light's moretop.ml
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Oct 30 16:02:59 2017 +0000
     1.3 @@ -4446,6 +4446,46 @@
     1.4    by (simp add: ENR_imp_ANR ENR_sphere)
     1.5  
     1.6  
     1.7 +subsection\<open>Spheres are connected, etc.\<close>
     1.8 +
     1.9 +lemma locally_path_connected_sphere_gen:
    1.10 +  fixes S :: "'a::euclidean_space set"
    1.11 +  assumes "bounded S" and "convex S" 
    1.12 +  shows "locally path_connected (rel_frontier S)"
    1.13 +proof (cases "rel_interior S = {}")
    1.14 +  case True
    1.15 +  with assms show ?thesis
    1.16 +    by (simp add: rel_interior_eq_empty)
    1.17 +next
    1.18 +  case False
    1.19 +  then obtain a where a: "a \<in> rel_interior S"
    1.20 +    by blast
    1.21 +  show ?thesis
    1.22 +  proof (rule retract_of_locally_path_connected)
    1.23 +    show "locally path_connected (affine hull S - {a})"
    1.24 +      by (meson convex_affine_hull convex_imp_locally_path_connected locally_open_subset openin_delete openin_subtopology_self)
    1.25 +    show "rel_frontier S retract_of affine hull S - {a}"
    1.26 +      using a assms rel_frontier_retract_of_punctured_affine_hull by blast
    1.27 +  qed
    1.28 +qed
    1.29 +
    1.30 +lemma locally_connected_sphere_gen:
    1.31 +  fixes S :: "'a::euclidean_space set"
    1.32 +  assumes "bounded S" and "convex S" 
    1.33 +  shows "locally connected (rel_frontier S)"
    1.34 +  by (simp add: ANR_imp_locally_connected ANR_rel_frontier_convex assms)
    1.35 +
    1.36 +lemma locally_path_connected_sphere:
    1.37 +  fixes a :: "'a::euclidean_space"
    1.38 +  shows "locally path_connected (sphere a r)"
    1.39 +  using ENR_imp_locally_path_connected ENR_sphere by blast
    1.40 +
    1.41 +lemma locally_connected_sphere:
    1.42 +  fixes a :: "'a::euclidean_space"
    1.43 +  shows "locally connected(sphere a r)"
    1.44 +  using ANR_imp_locally_connected ANR_sphere by blast
    1.45 +
    1.46 +
    1.47  subsection\<open>Borsuk homotopy extension theorem\<close>
    1.48  
    1.49  text\<open>It's only this late so we can use the concept of retraction,
    1.50 @@ -4794,6 +4834,386 @@
    1.51  qed
    1.52  
    1.53  
    1.54 +subsection\<open>More extension theorems\<close>
    1.55 +
    1.56 +lemma extension_from_clopen:
    1.57 +  assumes ope: "openin (subtopology euclidean S) T"
    1.58 +      and clo: "closedin (subtopology euclidean S) T"
    1.59 +      and contf: "continuous_on T f" and fim: "f ` T \<subseteq> U" and null: "U = {} \<Longrightarrow> S = {}"
    1.60 + obtains g where "continuous_on S g" "g ` S \<subseteq> U" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
    1.61 +proof (cases "U = {}")
    1.62 +  case True
    1.63 +  then show ?thesis
    1.64 +    by (simp add: null that)
    1.65 +next
    1.66 +  case False
    1.67 +  then obtain a where "a \<in> U"
    1.68 +    by auto
    1.69 +  let ?g = "\<lambda>x. if x \<in> T then f x else a"
    1.70 +  have Seq: "S = T \<union> (S - T)"
    1.71 +    using clo closedin_imp_subset by fastforce
    1.72 +  show ?thesis
    1.73 +  proof
    1.74 +    have "continuous_on (T \<union> (S - T)) ?g"
    1.75 +      apply (rule continuous_on_cases_local)
    1.76 +      using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local)
    1.77 +    with Seq show "continuous_on S ?g"
    1.78 +      by metis
    1.79 +    show "?g ` S \<subseteq> U"
    1.80 +      using \<open>a \<in> U\<close> fim by auto
    1.81 +    show "\<And>x. x \<in> T \<Longrightarrow> ?g x = f x"
    1.82 +      by auto
    1.83 +  qed
    1.84 +qed
    1.85 +
    1.86 +
    1.87 +lemma extension_from_component:
    1.88 +  fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
    1.89 +  assumes S: "locally connected S \<or> compact S" and "ANR U"
    1.90 +     and C: "C \<in> components S" and contf: "continuous_on C f" and fim: "f ` C \<subseteq> U"
    1.91 + obtains g where "continuous_on S g" "g ` S \<subseteq> U" "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
    1.92 +proof -
    1.93 +  obtain T g where ope: "openin (subtopology euclidean S) T"
    1.94 +               and clo: "closedin (subtopology euclidean S) T"
    1.95 +               and "C \<subseteq> T" and contg: "continuous_on T g" and gim: "g ` T \<subseteq> U"
    1.96 +               and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
    1.97 +    using S
    1.98 +  proof
    1.99 +    assume "locally connected S"
   1.100 +    show ?thesis
   1.101 +      by (metis C \<open>locally connected S\<close> openin_components_locally_connected closedin_component contf fim order_refl that)
   1.102 +  next
   1.103 +    assume "compact S"
   1.104 +    then obtain W g where "C \<subseteq> W" and opeW: "openin (subtopology euclidean S) W"
   1.105 +                 and contg: "continuous_on W g"
   1.106 +                 and gim: "g ` W \<subseteq> U" and gf: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
   1.107 +      using ANR_imp_absolute_neighbourhood_extensor [of U C f S] C \<open>ANR U\<close> closedin_component contf fim by blast
   1.108 +    then obtain V where "open V" and V: "W = S \<inter> V"
   1.109 +      by (auto simp: openin_open)
   1.110 +    moreover have "locally compact S"
   1.111 +      by (simp add: \<open>compact S\<close> closed_imp_locally_compact compact_imp_closed)
   1.112 +    ultimately obtain K where opeK: "openin (subtopology euclidean S) K" and "compact K" "C \<subseteq> K" "K \<subseteq> V"
   1.113 +      by (metis C Int_subset_iff \<open>C \<subseteq> W\<close> \<open>compact S\<close> compact_components Sura_Bura_clopen_subset)
   1.114 +    show ?thesis
   1.115 +    proof
   1.116 +      show "closedin (subtopology euclidean S) K"
   1.117 +        by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
   1.118 +      show "continuous_on K g"
   1.119 +        by (metis Int_subset_iff V \<open>K \<subseteq> V\<close> contg continuous_on_subset opeK openin_subtopology subset_eq)
   1.120 +      show "g ` K \<subseteq> U"
   1.121 +        using V \<open>K \<subseteq> V\<close> gim opeK openin_imp_subset by fastforce
   1.122 +    qed (use opeK gf \<open>C \<subseteq> K\<close> in auto)
   1.123 +  qed
   1.124 +  obtain h where "continuous_on S h" "h ` S \<subseteq> U" "\<And>x. x \<in> T \<Longrightarrow> h x = g x"
   1.125 +    using extension_from_clopen
   1.126 +    by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope)
   1.127 +  then show ?thesis
   1.128 +    by (metis \<open>C \<subseteq> T\<close> gf subset_eq that)
   1.129 +qed
   1.130 +
   1.131 +
   1.132 +lemma tube_lemma:
   1.133 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   1.134 +  assumes "compact S" and S: "S \<noteq> {}" "(\<lambda>x. (x,a)) ` S \<subseteq> U" 
   1.135 +      and ope: "openin (subtopology euclidean (S \<times> T)) U"
   1.136 +  obtains V where "openin (subtopology euclidean T) V" "a \<in> V" "S \<times> V \<subseteq> U"
   1.137 +proof -
   1.138 +  let ?W = "{y. \<exists>x. x \<in> S \<and> (x, y) \<in> (S \<times> T - U)}"
   1.139 +  have "U \<subseteq> S \<times> T" "closedin (subtopology euclidean (S \<times> T)) (S \<times> T - U)"
   1.140 +    using ope by (auto simp: openin_closedin_eq)
   1.141 +  then have "closedin (subtopology euclidean T) ?W"
   1.142 +    using \<open>compact S\<close> closedin_compact_projection by blast
   1.143 +  moreover have "a \<in> T - ?W"
   1.144 +    using \<open>U \<subseteq> S \<times> T\<close> S by auto
   1.145 +  moreover have "S \<times> (T - ?W) \<subseteq> U"
   1.146 +    by auto
   1.147 +  ultimately show ?thesis
   1.148 +    by (metis (no_types, lifting) Sigma_cong closedin_def that topspace_euclidean_subtopology)
   1.149 +qed
   1.150 +
   1.151 +lemma tube_lemma_gen:
   1.152 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   1.153 +  assumes "compact S" "S \<noteq> {}" "T \<subseteq> T'" "S \<times> T \<subseteq> U"
   1.154 +      and ope: "openin (subtopology euclidean (S \<times> T')) U"
   1.155 +  obtains V where "openin (subtopology euclidean T') V" "T \<subseteq> V" "S \<times> V \<subseteq> U"
   1.156 +proof -
   1.157 +  have "\<And>x. x \<in> T \<Longrightarrow> \<exists>V. openin (subtopology euclidean T') V \<and> x \<in> V \<and> S \<times> V \<subseteq> U"
   1.158 +    using assms by (auto intro:  tube_lemma [OF \<open>compact S\<close>])
   1.159 +  then obtain F where F: "\<And>x. x \<in> T \<Longrightarrow> openin (subtopology euclidean T') (F x) \<and> x \<in> F x \<and> S \<times> F x \<subseteq> U"
   1.160 +    by metis
   1.161 +  show ?thesis
   1.162 +  proof
   1.163 +    show "openin (subtopology euclidean T') (UNION T F)"
   1.164 +      using F by blast
   1.165 +    show "T \<subseteq> UNION T F"
   1.166 +      using F by blast
   1.167 +    show "S \<times> UNION T F \<subseteq> U"
   1.168 +      using F by auto
   1.169 +  qed
   1.170 +qed
   1.171 +
   1.172 +proposition homotopic_neighbourhood_extension:
   1.173 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.174 +  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> U"
   1.175 +      and contg: "continuous_on S g" and gim: "g ` S \<subseteq> U"
   1.176 +      and clo: "closedin (subtopology euclidean S) T"
   1.177 +      and "ANR U" and hom: "homotopic_with (\<lambda>x. True) T U f g"
   1.178 +    obtains V where "T \<subseteq> V" "openin (subtopology euclidean S) V"
   1.179 +                    "homotopic_with (\<lambda>x. True) V U f g"
   1.180 +proof -
   1.181 +  have "T \<subseteq> S"
   1.182 +    using clo closedin_imp_subset by blast
   1.183 +  obtain h where conth: "continuous_on ({0..1::real} \<times> T) h"
   1.184 +             and him: "h ` ({0..1} \<times> T) \<subseteq> U"
   1.185 +             and h0: "\<And>x. h(0, x) = f x" and h1: "\<And>x. h(1, x) = g x"
   1.186 +    using hom by (auto simp: homotopic_with_def)
   1.187 +  define h' where "h' \<equiv> \<lambda>z. if fst z \<in> {0} then f(snd z)
   1.188 +                             else if fst z \<in> {1} then g(snd z)
   1.189 +                             else h z"
   1.190 +  let ?S0 = "{0::real} \<times> S" and ?S1 = "{1::real} \<times> S"
   1.191 +  have "continuous_on(?S0 \<union> (?S1 \<union> {0..1} \<times> T)) h'"
   1.192 +    unfolding h'_def
   1.193 +  proof (intro continuous_on_cases_local)
   1.194 +    show "closedin (subtopology euclidean (?S0 \<union> (?S1 \<union> {0..1} \<times> T))) ?S0"
   1.195 +         "closedin (subtopology euclidean (?S1 \<union> {0..1} \<times> T)) ?S1"
   1.196 +      using \<open>T \<subseteq> S\<close> by (force intro: closedin_Times closedin_subset_trans [of "{0..1} \<times> S"])+
   1.197 +    show "closedin (subtopology euclidean (?S0 \<union> (?S1 \<union> {0..1} \<times> T))) (?S1 \<union> {0..1} \<times> T)"
   1.198 +         "closedin (subtopology euclidean (?S1 \<union> {0..1} \<times> T)) ({0..1} \<times> T)"
   1.199 +      using \<open>T \<subseteq> S\<close> by (force intro: clo closedin_Times closedin_subset_trans [of "{0..1} \<times> S"])+
   1.200 +    show "continuous_on (?S0) (\<lambda>x. f (snd x))"
   1.201 +      by (intro continuous_intros continuous_on_compose2 [OF contf]) auto
   1.202 +    show "continuous_on (?S1) (\<lambda>x. g (snd x))"
   1.203 +      by (intro continuous_intros continuous_on_compose2 [OF contg]) auto
   1.204 +  qed (use h0 h1 conth in auto)
   1.205 +  then have "continuous_on ({0,1} \<times> S \<union> ({0..1} \<times> T)) h'"
   1.206 +    by (metis Sigma_Un_distrib1 Un_assoc insert_is_Un) 
   1.207 +  moreover have "h' ` ({0,1} \<times> S \<union> {0..1} \<times> T) \<subseteq> U"
   1.208 +    using fim gim him \<open>T \<subseteq> S\<close> unfolding h'_def by force
   1.209 +  moreover have "closedin (subtopology euclidean ({0..1::real} \<times> S)) ({0,1} \<times> S \<union> {0..1::real} \<times> T)"
   1.210 +    by (intro closedin_Times closedin_Un clo) (simp_all add: closed_subset)
   1.211 +  ultimately
   1.212 +  obtain W k where W: "({0,1} \<times> S) \<union> ({0..1} \<times> T) \<subseteq> W"
   1.213 +               and opeW: "openin (subtopology euclidean ({0..1} \<times> S)) W"
   1.214 +               and contk: "continuous_on W k"
   1.215 +               and kim: "k ` W \<subseteq> U"
   1.216 +               and kh': "\<And>x. x \<in> ({0,1} \<times> S) \<union> ({0..1} \<times> T) \<Longrightarrow> k x = h' x"
   1.217 +    by (metis ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR U\<close>, of "({0,1} \<times> S) \<union> ({0..1} \<times> T)" h' "{0..1} \<times> S"])
   1.218 +  obtain T' where opeT': "openin (subtopology euclidean S) T'" 
   1.219 +              and "T \<subseteq> T'" and TW: "{0..1} \<times> T' \<subseteq> W"
   1.220 +    using tube_lemma_gen [of "{0..1::real}" T S W] W \<open>T \<subseteq> S\<close> opeW by auto
   1.221 +  moreover have "homotopic_with (\<lambda>x. True) T' U f g"
   1.222 +  proof (simp add: homotopic_with, intro exI conjI)
   1.223 +    show "continuous_on ({0..1} \<times> T') k"
   1.224 +      using TW continuous_on_subset contk by auto
   1.225 +    show "k ` ({0..1} \<times> T') \<subseteq> U"
   1.226 +      using TW kim by fastforce
   1.227 +    have "T' \<subseteq> S"
   1.228 +      by (meson opeT' subsetD openin_imp_subset)
   1.229 +    then show "\<forall>x\<in>T'. k (0, x) = f x" "\<forall>x\<in>T'. k (1, x) = g x"
   1.230 +      by (auto simp: kh' h'_def)
   1.231 +  qed
   1.232 +  ultimately show ?thesis
   1.233 +    by (blast intro: that)
   1.234 +qed
   1.235 +
   1.236 +text\<open> Homotopy on a union of closed-open sets.\<close>
   1.237 +proposition homotopic_on_clopen_Union:
   1.238 +  fixes \<F> :: "'a::euclidean_space set set"
   1.239 +  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
   1.240 +      and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
   1.241 +      and "\<And>S. S \<in> \<F> \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
   1.242 +  shows "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f g"
   1.243 +proof -
   1.244 +  obtain \<V> where "\<V> \<subseteq> \<F>" "countable \<V>" and eqU: "\<Union>\<V> = \<Union>\<F>"
   1.245 +    using Lindelof_openin assms by blast
   1.246 +  show ?thesis
   1.247 +  proof (cases "\<V> = {}")
   1.248 +    case True
   1.249 +    then show ?thesis
   1.250 +      by (metis Union_empty eqU homotopic_on_empty)
   1.251 +  next
   1.252 +    case False
   1.253 +    then obtain V :: "nat \<Rightarrow> 'a set" where V: "range V = \<V>"
   1.254 +      using range_from_nat_into \<open>countable \<V>\<close> by metis
   1.255 +    with \<open>\<V> \<subseteq> \<F>\<close> have clo: "\<And>n. closedin (subtopology euclidean (\<Union>\<F>)) (V n)"
   1.256 +                  and ope: "\<And>n. openin (subtopology euclidean (\<Union>\<F>)) (V n)"
   1.257 +                  and hom: "\<And>n. homotopic_with (\<lambda>x. True) (V n) T f g"
   1.258 +      using assms by auto 
   1.259 +    then obtain h where conth: "\<And>n. continuous_on ({0..1::real} \<times> V n) (h n)"
   1.260 +                  and him: "\<And>n. h n ` ({0..1} \<times> V n) \<subseteq> T" 
   1.261 +                  and h0: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (0, x) = f x" 
   1.262 +                  and h1: "\<And>n. \<And>x. x \<in> V n \<Longrightarrow> h n (1, x) = g x"
   1.263 +      by (simp add: homotopic_with) metis
   1.264 +    have wop: "b \<in> V x \<Longrightarrow> \<exists>k. b \<in> V k \<and> (\<forall>j<k. b \<notin> V j)" for b x
   1.265 +        using nat_less_induct [where P = "\<lambda>i. b \<notin> V i"] by meson
   1.266 +    obtain \<zeta> where cont: "continuous_on ({0..1} \<times> UNION UNIV V) \<zeta>"
   1.267 +              and eq: "\<And>x i. \<lbrakk>x \<in> {0..1} \<times> UNION UNIV V \<inter>
   1.268 +                                   {0..1} \<times> (V i - (\<Union>m<i. V m))\<rbrakk> \<Longrightarrow> \<zeta> x = h i x"
   1.269 +    proof (rule pasting_lemma_exists)
   1.270 +      show "{0..1} \<times> UNION UNIV V \<subseteq> (\<Union>i. {0..1::real} \<times> (V i - (\<Union>m<i. V m)))"
   1.271 +        by (force simp: Ball_def dest: wop)
   1.272 +      show "openin (subtopology euclidean ({0..1} \<times> UNION UNIV V)) 
   1.273 +                   ({0..1::real} \<times> (V i - (\<Union>m<i. V m)))" for i
   1.274 +      proof (intro openin_Times openin_subtopology_self openin_diff)
   1.275 +        show "openin (subtopology euclidean (UNION UNIV V)) (V i)"
   1.276 +          using ope V eqU by auto
   1.277 +        show "closedin (subtopology euclidean (UNION UNIV V)) (\<Union>m<i. V m)"
   1.278 +          using V clo eqU by (force intro: closedin_Union)
   1.279 +      qed
   1.280 +      show "continuous_on ({0..1} \<times> (V i - (\<Union>m<i. V m))) (h i)" for i
   1.281 +        by (rule continuous_on_subset [OF conth]) auto
   1.282 +      show "\<And>i j x. x \<in> {0..1} \<times> UNION UNIV V \<inter>
   1.283 +                    {0..1} \<times> (V i - (\<Union>m<i. V m)) \<inter> {0..1} \<times> (V j - (\<Union>m<j. V m))
   1.284 +                    \<Longrightarrow> h i x = h j x"
   1.285 +        by clarsimp (metis lessThan_iff linorder_neqE_nat)
   1.286 +    qed auto
   1.287 +    show ?thesis
   1.288 +    proof (simp add: homotopic_with eqU [symmetric], intro exI conjI ballI)
   1.289 +      show "continuous_on ({0..1} \<times> \<Union>\<V>) \<zeta>"
   1.290 +        using V eqU by (blast intro!:  continuous_on_subset [OF cont])
   1.291 +      show "\<zeta>` ({0..1} \<times> \<Union>\<V>) \<subseteq> T"
   1.292 +      proof clarsimp
   1.293 +        fix t :: real and y :: "'a" and X :: "'a set"
   1.294 +        assume "y \<in> X" "X \<in> \<V>" and t: "0 \<le> t" "t \<le> 1"
   1.295 +        then obtain k where "y \<in> V k" and j: "\<forall>j<k. y \<notin> V j"
   1.296 +          by (metis image_iff V wop)
   1.297 +        with him t show "\<zeta>(t, y) \<in> T"
   1.298 +          by (subst eq) (force simp:)+
   1.299 +      qed
   1.300 +      fix X y
   1.301 +      assume "X \<in> \<V>" "y \<in> X"
   1.302 +      then obtain k where "y \<in> V k" and j: "\<forall>j<k. y \<notin> V j"
   1.303 +        by (metis image_iff V wop)
   1.304 +      then show "\<zeta>(0, y) = f y" and "\<zeta>(1, y) = g y"
   1.305 +        by (subst eq [where i=k]; force simp: h0 h1)+ 
   1.306 +    qed
   1.307 +  qed
   1.308 +qed
   1.309 +
   1.310 +proposition homotopic_on_components_eq:
   1.311 +  fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
   1.312 +  assumes S: "locally connected S \<or> compact S" and "ANR T"
   1.313 +  shows "homotopic_with (\<lambda>x. True) S T f g \<longleftrightarrow>
   1.314 +         (continuous_on S f \<and> f ` S \<subseteq> T \<and> continuous_on S g \<and> g ` S \<subseteq> T) \<and>
   1.315 +         (\<forall>C \<in> components S. homotopic_with (\<lambda>x. True) C T f g)"
   1.316 +    (is "?lhs \<longleftrightarrow> ?C \<and> ?rhs")
   1.317 +proof -
   1.318 +  have "continuous_on S f" "f ` S \<subseteq> T" "continuous_on S g" "g ` S \<subseteq> T" if ?lhs
   1.319 +    using homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2 that by blast+
   1.320 +  moreover have "?lhs \<longleftrightarrow> ?rhs"
   1.321 +    if contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
   1.322 +  proof
   1.323 +    assume ?lhs
   1.324 +    with that show ?rhs
   1.325 +      by (simp add: homotopic_with_subset_left in_components_subset)
   1.326 +  next
   1.327 +    assume R: ?rhs
   1.328 +    have "\<exists>U. C \<subseteq> U \<and> closedin (subtopology euclidean S) U \<and>
   1.329 +              openin (subtopology euclidean S) U \<and>
   1.330 +              homotopic_with (\<lambda>x. True) U T f g" if C: "C \<in> components S" for C
   1.331 +    proof -
   1.332 +      have "C \<subseteq> S"
   1.333 +        by (simp add: in_components_subset that)
   1.334 +      show ?thesis
   1.335 +        using S
   1.336 +      proof
   1.337 +        assume "locally connected S"
   1.338 +        show ?thesis
   1.339 +        proof (intro exI conjI)
   1.340 +          show "closedin (subtopology euclidean S) C"
   1.341 +            by (simp add: closedin_component that)
   1.342 +          show "openin (subtopology euclidean S) C"
   1.343 +            by (simp add: \<open>locally connected S\<close> openin_components_locally_connected that)
   1.344 +          show "homotopic_with (\<lambda>x. True) C T f g"
   1.345 +            by (simp add: R that)
   1.346 +        qed auto
   1.347 +      next
   1.348 +        assume "compact S"
   1.349 +        have hom: "homotopic_with (\<lambda>x. True) C T f g"
   1.350 +          using R that by blast
   1.351 +        obtain U where "C \<subseteq> U" and opeU: "openin (subtopology euclidean S) U"
   1.352 +                  and hom: "homotopic_with (\<lambda>x. True) U T f g"
   1.353 +          using homotopic_neighbourhood_extension [OF contf fim contg gim _ \<open>ANR T\<close> hom]
   1.354 +            \<open>C \<in> components S\<close> closedin_component by blast
   1.355 +        then obtain V where "open V" and V: "U = S \<inter> V"
   1.356 +          by (auto simp: openin_open)
   1.357 +        moreover have "locally compact S"
   1.358 +          by (simp add: \<open>compact S\<close> closed_imp_locally_compact compact_imp_closed)
   1.359 +        ultimately obtain K where opeK: "openin (subtopology euclidean S) K" and "compact K" "C \<subseteq> K" "K \<subseteq> V"
   1.360 +          by (metis C Int_subset_iff Sura_Bura_clopen_subset \<open>C \<subseteq> U\<close> \<open>compact S\<close> compact_components)
   1.361 +        show ?thesis
   1.362 +        proof (intro exI conjI)
   1.363 +          show "closedin (subtopology euclidean S) K"
   1.364 +            by (meson \<open>compact K\<close> \<open>compact S\<close> closedin_compact_eq opeK openin_imp_subset)
   1.365 +          show "homotopic_with (\<lambda>x. True) K T f g"
   1.366 +            using V \<open>K \<subseteq> V\<close> hom homotopic_with_subset_left opeK openin_imp_subset by fastforce
   1.367 +        qed (use opeK \<open>C \<subseteq> K\<close> in auto)
   1.368 +      qed
   1.369 +    qed
   1.370 +    then obtain \<phi> where \<phi>: "\<And>C. C \<in> components S \<Longrightarrow> C \<subseteq> \<phi> C"
   1.371 +                  and clo\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> closedin (subtopology euclidean S) (\<phi> C)"
   1.372 +                  and ope\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> openin (subtopology euclidean S) (\<phi> C)"
   1.373 +                  and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with (\<lambda>x. True) (\<phi> C) T f g"
   1.374 +      by metis
   1.375 +    have Seq: "S = UNION (components S) \<phi>"
   1.376 +    proof
   1.377 +      show "S \<subseteq> UNION (components S) \<phi>"
   1.378 +        by (metis Sup_mono Union_components \<phi> imageI)
   1.379 +      show "UNION (components S) \<phi> \<subseteq> S"
   1.380 +        using ope\<phi> openin_imp_subset by fastforce
   1.381 +    qed
   1.382 +    show ?lhs
   1.383 +      apply (subst Seq)
   1.384 +      apply (rule homotopic_on_clopen_Union)
   1.385 +      using Seq clo\<phi> ope\<phi> hom\<phi> by auto
   1.386 +  qed
   1.387 +  ultimately show ?thesis by blast
   1.388 +qed
   1.389 +
   1.390 +
   1.391 +lemma cohomotopically_trivial_on_components:
   1.392 +  fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
   1.393 +  assumes S: "locally connected S \<or> compact S" and "ANR T"
   1.394 +  shows
   1.395 +   "(\<forall>f g. continuous_on S f \<longrightarrow> f ` S \<subseteq> T \<longrightarrow> continuous_on S g \<longrightarrow> g ` S \<subseteq> T \<longrightarrow>
   1.396 +           homotopic_with (\<lambda>x. True) S T f g)
   1.397 +    \<longleftrightarrow>
   1.398 +    (\<forall>C\<in>components S.
   1.399 +        \<forall>f g. continuous_on C f \<longrightarrow> f ` C \<subseteq> T \<longrightarrow> continuous_on C g \<longrightarrow> g ` C \<subseteq> T \<longrightarrow>
   1.400 +              homotopic_with (\<lambda>x. True) C T f g)"
   1.401 +     (is "?lhs = ?rhs")
   1.402 +proof
   1.403 +  assume L[rule_format]: ?lhs
   1.404 +  show ?rhs
   1.405 +  proof clarify
   1.406 +    fix C f g
   1.407 +    assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> T"
   1.408 +       and contg: "continuous_on C g" and gim: "g ` C \<subseteq> T" and C: "C \<in> components S"
   1.409 +    obtain f' where contf': "continuous_on S f'" and f'im: "f' ` S \<subseteq> T" and f'f: "\<And>x. x \<in> C \<Longrightarrow> f' x = f x"
   1.410 +      using extension_from_component [OF S \<open>ANR T\<close> C contf fim] by metis
   1.411 +    obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \<subseteq> T" and g'g: "\<And>x. x \<in> C \<Longrightarrow> g' x = g x"
   1.412 +      using extension_from_component [OF S \<open>ANR T\<close> C contg gim] by metis
   1.413 +    have "homotopic_with (\<lambda>x. True) C T f' g'"
   1.414 +      using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce
   1.415 +    then show "homotopic_with (\<lambda>x. True) C T f g"
   1.416 +      using f'f g'g homotopic_with_eq by force
   1.417 +  qed
   1.418 +next
   1.419 +  assume R [rule_format]: ?rhs
   1.420 +  show ?lhs
   1.421 +  proof clarify
   1.422 +    fix f g
   1.423 +    assume contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
   1.424 +      and contg: "continuous_on S g" and gim: "g ` S \<subseteq> T"
   1.425 +    moreover have "homotopic_with (\<lambda>x. True) C T f g" if "C \<in> components S" for C
   1.426 +      using R [OF that]
   1.427 +      by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that)
   1.428 +    ultimately show "homotopic_with (\<lambda>x. True) S T f g"
   1.429 +      by (subst homotopic_on_components_eq [OF S \<open>ANR T\<close>]) auto
   1.430 +  qed
   1.431 +qed
   1.432 +
   1.433 +
   1.434  subsection\<open>The complement of a set and path-connectedness\<close>
   1.435  
   1.436  text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
     2.1 --- a/src/HOL/Analysis/Connected.thy	Sun Oct 29 19:39:03 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Connected.thy	Mon Oct 30 16:02:59 2017 +0000
     2.3 @@ -810,6 +810,10 @@
     2.4      by (auto simp: closedin_closed)
     2.5  qed
     2.6  
     2.7 +lemma closedin_component:
     2.8 +   "C \<in> components s \<Longrightarrow> closedin (subtopology euclidean s) C"
     2.9 +  using closedin_connected_component componentsE by blast
    2.10 +
    2.11  
    2.12  subsection \<open>Intersecting chains of compact sets and the Baire property\<close>
    2.13  
    2.14 @@ -3235,39 +3239,29 @@
    2.15  using assms
    2.16  by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
    2.17  
    2.18 -text\<open>Some more convenient intermediate-value theorem formulations.\<close>
    2.19 +subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
    2.20  
    2.21  lemma connected_ivt_hyperplane:
    2.22 -  assumes "connected s"
    2.23 -    and "x \<in> s"
    2.24 -    and "y \<in> s"
    2.25 -    and "inner a x \<le> b"
    2.26 -    and "b \<le> inner a y"
    2.27 -  shows "\<exists>z \<in> s. inner a z = b"
    2.28 +  assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
    2.29 +  shows "\<exists>z \<in> S. inner a z = b"
    2.30  proof (rule ccontr)
    2.31 -  assume as:"\<not> (\<exists>z\<in>s. inner a z = b)"
    2.32 +  assume as:"\<not> (\<exists>z\<in>S. inner a z = b)"
    2.33    let ?A = "{x. inner a x < b}"
    2.34    let ?B = "{x. inner a x > b}"
    2.35    have "open ?A" "open ?B"
    2.36      using open_halfspace_lt and open_halfspace_gt by auto
    2.37 -  moreover
    2.38 -  have "?A \<inter> ?B = {}" by auto
    2.39 -  moreover
    2.40 -  have "s \<subseteq> ?A \<union> ?B" using as by auto
    2.41 -  ultimately
    2.42 -  show False
    2.43 -    using assms(1)[unfolded connected_def not_ex,
    2.44 +  moreover have "?A \<inter> ?B = {}" by auto
    2.45 +  moreover have "S \<subseteq> ?A \<union> ?B" using as by auto
    2.46 +  ultimately show False
    2.47 +    using \<open>connected S\<close>[unfolded connected_def not_ex,
    2.48        THEN spec[where x="?A"], THEN spec[where x="?B"]]
    2.49 -    using assms(2-5)
    2.50 -    by auto
    2.51 +    using xy b by auto
    2.52  qed
    2.53  
    2.54  lemma connected_ivt_component:
    2.55    fixes x::"'a::euclidean_space"
    2.56 -  shows "connected s \<Longrightarrow>
    2.57 -    x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow>
    2.58 -    x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>s.  z\<bullet>k = a)"
    2.59 -  using connected_ivt_hyperplane[of s x y "k::'a" a]
    2.60 +  shows "connected S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>S.  z\<bullet>k = a)"
    2.61 +  using connected_ivt_hyperplane[of S x y "k::'a" a]
    2.62    by (auto simp: inner_commute)
    2.63  
    2.64  lemma image_affinity_cbox: fixes m::real
    2.65 @@ -4942,7 +4936,7 @@
    2.66  qed
    2.67  
    2.68  
    2.69 -proposition component_complement_connected:
    2.70 +proposition component_diff_connected:
    2.71    fixes S :: "'a::metric_space set"
    2.72    assumes "connected S" "connected U" "S \<subseteq> U" and C: "C \<in> components (U - S)"
    2.73    shows "connected(U - C)"
     3.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Oct 29 19:39:03 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Oct 30 16:02:59 2017 +0000
     3.3 @@ -2373,7 +2373,14 @@
     3.4  qed
     3.5  
     3.6  corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
     3.7 -  by(simp add: convex_connected)
     3.8 +  by (simp add: convex_connected)
     3.9 +
    3.10 +corollary component_complement_connected:
    3.11 +  fixes S :: "'a::real_normed_vector set"
    3.12 +  assumes "connected S" "C \<in> components (-S)"
    3.13 +  shows "connected(-C)"
    3.14 +  using component_diff_connected [of S UNIV] assms
    3.15 +  by (auto simp: Compl_eq_Diff_UNIV)
    3.16  
    3.17  proposition clopen:
    3.18    fixes S :: "'a :: real_normed_vector set"
     4.1 --- a/src/HOL/Analysis/Further_Topology.thy	Sun Oct 29 19:39:03 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Mon Oct 30 16:02:59 2017 +0000
     4.3 @@ -4589,4 +4589,788 @@
     4.4      using fk gfh kTS by force
     4.5  qed
     4.6  
     4.7 +
     4.8 +text\<open>If two points are separated by a closed set, there's a minimal one.\<close>
     4.9 +proposition closed_irreducible_separator:
    4.10 +  fixes a :: "'a::real_normed_vector"
    4.11 +  assumes "closed S" and ab: "\<not> connected_component (- S) a b"
    4.12 +  obtains T where "T \<subseteq> S" "closed T" "T \<noteq> {}" "\<not> connected_component (- T) a b"
    4.13 +                  "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
    4.14 +proof (cases "a \<in> S \<or> b \<in> S")
    4.15 +  case True
    4.16 +  then show ?thesis
    4.17 +  proof
    4.18 +    assume *: "a \<in> S"
    4.19 +    show ?thesis
    4.20 +    proof
    4.21 +      show "{a} \<subseteq> S"
    4.22 +        using * by blast
    4.23 +      show "\<not> connected_component (- {a}) a b"
    4.24 +        using connected_component_in by auto
    4.25 +      show "\<And>U. U \<subset> {a} \<Longrightarrow> connected_component (- U) a b"
    4.26 +        by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
    4.27 +    qed auto
    4.28 +  next
    4.29 +    assume *: "b \<in> S"
    4.30 +    show ?thesis
    4.31 +    proof
    4.32 +      show "{b} \<subseteq> S"
    4.33 +        using * by blast
    4.34 +      show "\<not> connected_component (- {b}) a b"
    4.35 +        using connected_component_in by auto
    4.36 +      show "\<And>U. U \<subset> {b} \<Longrightarrow> connected_component (- U) a b"
    4.37 +        by (metis connected_component_UNIV UNIV_I compl_bot_eq connected_component_eq_eq less_le_not_le subset_singletonD)
    4.38 +    qed auto
    4.39 +  qed
    4.40 +next
    4.41 +  case False
    4.42 +  define A where "A \<equiv> connected_component_set (- S) a"
    4.43 +  define B where "B \<equiv> connected_component_set (- (closure A)) b"
    4.44 +  have "a \<in> A"
    4.45 +    using False A_def by auto
    4.46 +  have "b \<in> B"
    4.47 +    unfolding A_def B_def closure_Un_frontier
    4.48 +    using ab False \<open>closed S\<close> frontier_complement frontier_of_connected_component_subset frontier_subset_closed by force
    4.49 +  have "frontier B \<subseteq> frontier (connected_component_set (- closure A) b)"
    4.50 +    using B_def by blast
    4.51 +  also have frsub: "... \<subseteq> frontier A"
    4.52 +  proof -
    4.53 +    have "\<And>A. closure (- closure (- A)) \<subseteq> closure A"
    4.54 +      by (metis (no_types) closure_mono closure_subset compl_le_compl_iff double_compl)
    4.55 +    then show ?thesis
    4.56 +      by (metis (no_types) closure_closure double_compl frontier_closures frontier_of_connected_component_subset le_inf_iff subset_trans)
    4.57 +  qed
    4.58 +  finally have frBA: "frontier B \<subseteq> frontier A" .
    4.59 +  show ?thesis
    4.60 +  proof
    4.61 +    show "frontier B \<subseteq> S"
    4.62 +    proof -
    4.63 +      have "frontier S \<subseteq> S"
    4.64 +        by (simp add: \<open>closed S\<close> frontier_subset_closed)
    4.65 +      then show ?thesis
    4.66 +        using frsub frontier_complement frontier_of_connected_component_subset
    4.67 +        unfolding A_def B_def by blast
    4.68 +    qed
    4.69 +    show "closed (frontier B)"
    4.70 +      by simp
    4.71 +    show "\<not> connected_component (- frontier B) a b"
    4.72 +      unfolding connected_component_def
    4.73 +    proof clarify
    4.74 +      fix T
    4.75 +      assume "connected T" and TB: "T \<subseteq> - frontier B" and "a \<in> T" and "b \<in> T"
    4.76 +      have "a \<notin> B"
    4.77 +        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component set_mp)
    4.78 +      have "T \<inter> B \<noteq> {}"
    4.79 +        using \<open>b \<in> B\<close> \<open>b \<in> T\<close> by blast
    4.80 +      moreover have "T - B \<noteq> {}"
    4.81 +        using \<open>a \<notin> B\<close> \<open>a \<in> T\<close> by blast
    4.82 +      ultimately show "False"
    4.83 +        using connected_Int_frontier [of T B] TB \<open>connected T\<close> by blast
    4.84 +    qed
    4.85 +    moreover have "connected_component (- frontier B) a b" if "frontier B = {}"
    4.86 +      apply (simp add: that)
    4.87 +      using connected_component_eq_UNIV by blast
    4.88 +    ultimately show "frontier B \<noteq> {}"
    4.89 +      by blast
    4.90 +    show "connected_component (- U) a b" if "U \<subset> frontier B" for U
    4.91 +    proof -
    4.92 +      obtain p where Usub: "U \<subseteq> frontier B" and p: "p \<in> frontier B" "p \<notin> U"
    4.93 +        using \<open>U \<subset> frontier B\<close> by blast
    4.94 +      show ?thesis
    4.95 +        unfolding connected_component_def
    4.96 +      proof (intro exI conjI)
    4.97 +        have "connected ((insert p A) \<union> (insert p B))"
    4.98 +        proof (rule connected_Un)
    4.99 +          show "connected (insert p A)"
   4.100 +            by (metis A_def IntD1 frBA \<open>p \<in> frontier B\<close> closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subsetCE subset_insertI)
   4.101 +          show "connected (insert p B)"
   4.102 +            by (metis B_def IntD1 \<open>p \<in> frontier B\<close> closure_insert closure_subset connected_connected_component connected_intermediate_closure frontier_closures insert_absorb subset_insertI)
   4.103 +        qed blast
   4.104 +        then show "connected (insert p (B \<union> A))"
   4.105 +          by (simp add: sup.commute)
   4.106 +        have "A \<subseteq> - U"
   4.107 +          using A_def Usub \<open>frontier B \<subseteq> S\<close> connected_component_subset by fastforce
   4.108 +        moreover have "B \<subseteq> - U"
   4.109 +          using B_def Usub connected_component_subset frBA frontier_closures by fastforce
   4.110 +        ultimately show "insert p (B \<union> A) \<subseteq> - U"
   4.111 +          using p by auto
   4.112 +      qed (auto simp: \<open>a \<in> A\<close> \<open>b \<in> B\<close>)
   4.113 +    qed
   4.114 +  qed
   4.115 +qed
   4.116 +
   4.117 +lemma frontier_minimal_separating_closed_pointwise:
   4.118 +  fixes S :: "'a::real_normed_vector set"
   4.119 +  assumes S: "closed S" "a \<notin> S" and nconn: "\<not> connected_component (- S) a b"
   4.120 +      and conn: "\<And>T. \<lbrakk>closed T; T \<subset> S\<rbrakk> \<Longrightarrow> connected_component (- T) a b"
   4.121 +    shows "frontier(connected_component_set (- S) a) = S" (is "?F = S")
   4.122 +proof -
   4.123 +  have "?F \<subseteq> S"
   4.124 +    by (simp add: S componentsI frontier_of_components_closed_complement)
   4.125 +  moreover have False if "?F \<subset> S"
   4.126 +  proof -
   4.127 +    have "connected_component (- ?F) a b"
   4.128 +      by (simp add: conn that)
   4.129 +    then obtain T where "connected T" "T \<subseteq> -?F" "a \<in> T" "b \<in> T"
   4.130 +      by (auto simp: connected_component_def)
   4.131 +    moreover have "T \<inter> ?F \<noteq> {}"
   4.132 +    proof (rule connected_Int_frontier [OF \<open>connected T\<close>])
   4.133 +      show "T \<inter> connected_component_set (- S) a \<noteq> {}"
   4.134 +        using \<open>a \<notin> S\<close> \<open>a \<in> T\<close> by fastforce
   4.135 +      show "T - connected_component_set (- S) a \<noteq> {}"
   4.136 +        using \<open>b \<in> T\<close> nconn by blast
   4.137 +    qed
   4.138 +    ultimately show ?thesis
   4.139 +      by blast
   4.140 +  qed
   4.141 +  ultimately show ?thesis
   4.142 +    by blast
   4.143 +qed
   4.144 +
   4.145 +
   4.146 +subsection\<open>Unicoherence (closed)\<close>
   4.147 +
   4.148 +definition unicoherent where
   4.149 +  "unicoherent U \<equiv>
   4.150 +  \<forall>S T. connected S \<and> connected T \<and> S \<union> T = U \<and>
   4.151 +        closedin (subtopology euclidean U) S \<and> closedin (subtopology euclidean U) T
   4.152 +        \<longrightarrow> connected (S \<inter> T)"
   4.153 +
   4.154 +lemma unicoherentI [intro?]:
   4.155 +  assumes "\<And>S T. \<lbrakk>connected S; connected T; U = S \<union> T; closedin (subtopology euclidean U) S; closedin (subtopology euclidean U) T\<rbrakk>
   4.156 +          \<Longrightarrow> connected (S \<inter> T)"
   4.157 +  shows "unicoherent U"
   4.158 +  using assms unfolding unicoherent_def by blast
   4.159 +
   4.160 +lemma unicoherentD:
   4.161 +  assumes "unicoherent U" "connected S" "connected T" "U = S \<union> T" "closedin (subtopology euclidean U) S" "closedin (subtopology euclidean U) T"
   4.162 +  shows "connected (S \<inter> T)"
   4.163 +  using assms unfolding unicoherent_def by blast
   4.164 +
   4.165 +lemma homeomorphic_unicoherent:
   4.166 +  assumes ST: "S homeomorphic T" and S: "unicoherent S"
   4.167 +  shows "unicoherent T"
   4.168 +proof -
   4.169 +  obtain f g where gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x" and fim: "T = f ` S" and gfim: "g ` f ` S = S"
   4.170 +    and contf: "continuous_on S f" and contg: "continuous_on (f ` S) g"
   4.171 +    using ST by (auto simp: homeomorphic_def homeomorphism_def)
   4.172 +  show ?thesis
   4.173 +  proof
   4.174 +    fix U V
   4.175 +    assume "connected U" "connected V" and T: "T = U \<union> V"
   4.176 +      and cloU: "closedin (subtopology euclidean T) U"
   4.177 +      and cloV: "closedin (subtopology euclidean T) V"
   4.178 +    have "f ` (g ` U \<inter> g ` V) \<subseteq> U" "f ` (g ` U \<inter> g ` V) \<subseteq> V"
   4.179 +      using gf fim T by auto (metis UnCI image_iff)+
   4.180 +    moreover have "U \<inter> V \<subseteq> f ` (g ` U \<inter> g ` V)"
   4.181 +      using gf fim by (force simp: image_iff T)
   4.182 +    ultimately have "U \<inter> V = f ` (g ` U \<inter> g ` V)" by blast
   4.183 +    moreover have "connected (f ` (g ` U \<inter> g ` V))"
   4.184 +    proof (rule connected_continuous_image)
   4.185 +      show "continuous_on (g ` U \<inter> g ` V) f"
   4.186 +        apply (rule continuous_on_subset [OF contf])
   4.187 +        using T fim gfim by blast
   4.188 +      show "connected (g ` U \<inter> g ` V)"
   4.189 +      proof (intro conjI unicoherentD [OF S])
   4.190 +        show "connected (g ` U)" "connected (g ` V)"
   4.191 +          using \<open>connected U\<close> cloU \<open>connected V\<close> cloV
   4.192 +          by (metis Topological_Spaces.connected_continuous_image closedin_imp_subset contg continuous_on_subset fim)+
   4.193 +        show "S = g ` U \<union> g ` V"
   4.194 +          using T fim gfim by auto
   4.195 +        have hom: "homeomorphism T S g f"
   4.196 +          by (simp add: contf contg fim gf gfim homeomorphism_def)
   4.197 +        have "closedin (subtopology euclidean T) U" "closedin (subtopology euclidean T) V"
   4.198 +          by (simp_all add: cloU cloV)
   4.199 +        then show "closedin (subtopology euclidean S) (g ` U)"
   4.200 +                  "closedin (subtopology euclidean S) (g ` V)"
   4.201 +          by (blast intro: homeomorphism_imp_closed_map [OF hom])+
   4.202 +      qed
   4.203 +    qed
   4.204 +    ultimately show "connected (U \<inter> V)" by metis
   4.205 +  qed
   4.206 +qed
   4.207 +
   4.208 +
   4.209 +lemma homeomorphic_unicoherent_eq:
   4.210 +   "S homeomorphic T \<Longrightarrow> (unicoherent S \<longleftrightarrow> unicoherent T)"
   4.211 +  by (meson homeomorphic_sym homeomorphic_unicoherent)
   4.212 +
   4.213 +lemma unicoherent_translation:
   4.214 +  fixes S :: "'a::real_normed_vector set"
   4.215 +  shows
   4.216 +   "unicoherent (image (\<lambda>x. a + x) S) \<longleftrightarrow> unicoherent S"
   4.217 +  using homeomorphic_translation homeomorphic_unicoherent_eq by blast
   4.218 +
   4.219 +lemma unicoherent_injective_linear_image:
   4.220 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.221 +  assumes "linear f" "inj f"
   4.222 +  shows "(unicoherent(f ` S) \<longleftrightarrow> unicoherent S)"
   4.223 +  using assms homeomorphic_unicoherent_eq linear_homeomorphic_image by blast
   4.224 +
   4.225 +
   4.226 +lemma Borsukian_imp_unicoherent:
   4.227 +  fixes U :: "'a::euclidean_space set"
   4.228 +  assumes "Borsukian U"  shows "unicoherent U"
   4.229 +  unfolding unicoherent_def
   4.230 +proof clarify
   4.231 +  fix S T
   4.232 +  assume "connected S" "connected T" "U = S \<union> T"
   4.233 +     and cloS: "closedin (subtopology euclidean (S \<union> T)) S"
   4.234 +     and cloT: "closedin (subtopology euclidean (S \<union> T)) T"
   4.235 +  show "connected (S \<inter> T)"
   4.236 +    unfolding connected_closedin_eq
   4.237 +  proof clarify
   4.238 +    fix V W
   4.239 +    assume "closedin (subtopology euclidean (S \<inter> T)) V"
   4.240 +       and "closedin (subtopology euclidean (S \<inter> T)) W"
   4.241 +       and VW: "V \<union> W = S \<inter> T" "V \<inter> W = {}" and "V \<noteq> {}" "W \<noteq> {}"
   4.242 +    then have cloV: "closedin (subtopology euclidean U) V" and cloW: "closedin (subtopology euclidean U) W"
   4.243 +      using \<open>U = S \<union> T\<close> cloS cloT closedin_trans by blast+
   4.244 +    obtain q where contq: "continuous_on U q"
   4.245 +         and q01: "\<And>x. x \<in> U \<Longrightarrow> q x \<in> {0..1::real}"
   4.246 +         and qV: "\<And>x. x \<in> V \<Longrightarrow> q x = 0" and qW: "\<And>x. x \<in> W \<Longrightarrow> q x = 1"
   4.247 +      by (rule Urysohn_local [OF cloV cloW \<open>V \<inter> W = {}\<close>, of 0 1])
   4.248 +         (fastforce simp: closed_segment_eq_real_ivl)
   4.249 +    let ?h = "\<lambda>x. if x \<in> S then exp(pi * \<i> * q x) else 1 / exp(pi * \<i> * q x)"
   4.250 +    have eqST: "exp(pi * \<i> * q x) = 1 / exp(pi * \<i> * q x)" if "x \<in> S \<inter> T" for x
   4.251 +    proof -
   4.252 +      have "x \<in> V \<union> W"
   4.253 +        using that \<open>V \<union> W = S \<inter> T\<close> by blast
   4.254 +      with qV qW show ?thesis by force
   4.255 +    qed
   4.256 +    obtain g where contg: "continuous_on U g"
   4.257 +      and circle: "g ` U \<subseteq> sphere 0 1"
   4.258 +      and S: "\<And>x. x \<in> S \<Longrightarrow> g x = exp(pi * \<i> * q x)"
   4.259 +      and T: "\<And>x. x \<in> T \<Longrightarrow> g x = 1 / exp(pi * \<i> * q x)"
   4.260 +    proof
   4.261 +      show "continuous_on U ?h"
   4.262 +        unfolding \<open>U = S \<union> T\<close>
   4.263 +      proof (rule continuous_on_cases_local [OF cloS cloT])
   4.264 +        show "continuous_on S (\<lambda>x. exp (pi * \<i> * q x))"
   4.265 +          apply (intro continuous_intros)
   4.266 +          using \<open>U = S \<union> T\<close> continuous_on_subset contq by blast
   4.267 +        show "continuous_on T (\<lambda>x. 1 / exp (pi * \<i> * q x))"
   4.268 +          apply (intro continuous_intros)
   4.269 +          using \<open>U = S \<union> T\<close> continuous_on_subset contq by auto
   4.270 +      qed (use eqST in auto)
   4.271 +    qed (use eqST in \<open>auto simp: norm_divide\<close>)
   4.272 +    then obtain h where conth: "continuous_on U h" and heq: "\<And>x. x \<in> U \<Longrightarrow> g x = exp (h x)"
   4.273 +      by (metis Borsukian_continuous_logarithm_circle assms)
   4.274 +    obtain v w where "v \<in> V" "w \<in> W"
   4.275 +      using \<open>V \<noteq> {}\<close> \<open>W \<noteq> {}\<close> by blast
   4.276 +    then have vw: "v \<in> S \<inter> T" "w \<in> S \<inter> T"
   4.277 +      using VW by auto
   4.278 +    have iff: "2 * pi \<le> cmod (2 * of_int m * of_real pi * \<i> - 2 * of_int n * of_real pi * \<i>)
   4.279 +          \<longleftrightarrow> 1 \<le> abs (m - n)" for m n
   4.280 +    proof -
   4.281 +      have "2 * pi \<le> cmod (2 * of_int m * of_real pi * \<i> - 2 * of_int n * of_real pi * \<i>)
   4.282 +            \<longleftrightarrow> 2 * pi \<le> cmod ((2 * pi * \<i>) * (of_int m - of_int n))"
   4.283 +        by (simp add: algebra_simps)
   4.284 +      also have "... \<longleftrightarrow> 2 * pi \<le> 2 * pi * cmod (of_int m - of_int n)"
   4.285 +        by (simp add: norm_mult)
   4.286 +      also have "... \<longleftrightarrow> 1 \<le> abs (m - n)"
   4.287 +        by simp (metis norm_of_int of_int_1_le_iff of_int_abs of_int_diff)
   4.288 +      finally show ?thesis .
   4.289 +    qed
   4.290 +    have *: "\<exists>n::int. h x - (pi * \<i> * q x) = (of_int(2*n) * pi) * \<i>" if "x \<in> S" for x
   4.291 +      using that S \<open>U = S \<union> T\<close> heq exp_eq [symmetric] by (simp add: algebra_simps)
   4.292 +    moreover have "(\<lambda>x. h x - (pi * \<i> * q x)) constant_on S"
   4.293 +    proof (rule continuous_discrete_range_constant [OF \<open>connected S\<close>])
   4.294 +      have "continuous_on S h" "continuous_on S q"
   4.295 +        using \<open>U = S \<union> T\<close> continuous_on_subset conth contq by blast+
   4.296 +      then show "continuous_on S (\<lambda>x. h x - (pi * \<i> * q x))"
   4.297 +        by (intro continuous_intros)
   4.298 +      have "2*pi \<le> cmod (h y - (pi * \<i> * q y) - (h x - (pi * \<i> * q x)))"
   4.299 +        if "x \<in> S" "y \<in> S" and ne: "h y - (pi * \<i> * q y) \<noteq> h x - (pi * \<i> * q x)" for x y
   4.300 +        using * [OF \<open>x \<in> S\<close>] * [OF \<open>y \<in> S\<close>] ne by (auto simp: iff)
   4.301 +      then show "\<And>x. x \<in> S \<Longrightarrow>
   4.302 +         \<exists>e>0. \<forall>y. y \<in> S \<and> h y - (pi * \<i> * q y) \<noteq> h x - (pi * \<i> * q x) \<longrightarrow>
   4.303 +                   e \<le> cmod (h y - (pi * \<i> * q y) - (h x - (pi * \<i> * q x)))"
   4.304 +        by (rule_tac x="2*pi" in exI) auto
   4.305 +    qed
   4.306 +    ultimately
   4.307 +    obtain m where m: "\<And>x. x \<in> S \<Longrightarrow> h x - (pi * \<i> * q x) = (of_int(2*m) * pi) * \<i>"
   4.308 +      using vw by (force simp: constant_on_def)
   4.309 +    have *: "\<exists>n::int. h x = - (pi * \<i> * q x) + (of_int(2*n) * pi) * \<i>" if "x \<in> T" for x
   4.310 +      unfolding exp_eq [symmetric]
   4.311 +      using that T \<open>U = S \<union> T\<close> by (simp add: exp_minus field_simps  heq [symmetric])
   4.312 +    moreover have "(\<lambda>x. h x + (pi * \<i> * q x)) constant_on T"
   4.313 +    proof (rule continuous_discrete_range_constant [OF \<open>connected T\<close>])
   4.314 +      have "continuous_on T h" "continuous_on T q"
   4.315 +        using \<open>U = S \<union> T\<close> continuous_on_subset conth contq by blast+
   4.316 +      then show "continuous_on T (\<lambda>x. h x + (pi * \<i> * q x))"
   4.317 +        by (intro continuous_intros)
   4.318 +      have "2*pi \<le> cmod (h y + (pi * \<i> * q y) - (h x + (pi * \<i> * q x)))"
   4.319 +        if "x \<in> T" "y \<in> T" and ne: "h y + (pi * \<i> * q y) \<noteq> h x + (pi * \<i> * q x)" for x y
   4.320 +        using * [OF \<open>x \<in> T\<close>] * [OF \<open>y \<in> T\<close>] ne by (auto simp: iff)
   4.321 +      then show "\<And>x. x \<in> T \<Longrightarrow>
   4.322 +         \<exists>e>0. \<forall>y. y \<in> T \<and> h y + (pi * \<i> * q y) \<noteq> h x + (pi * \<i> * q x) \<longrightarrow>
   4.323 +                   e \<le> cmod (h y + (pi * \<i> * q y) - (h x + (pi * \<i> * q x)))"
   4.324 +        by (rule_tac x="2*pi" in exI) auto
   4.325 +    qed
   4.326 +    ultimately
   4.327 +    obtain n where n: "\<And>x. x \<in> T \<Longrightarrow> h x + (pi * \<i> * q x) = (of_int(2*n) * pi) * \<i>"
   4.328 +      using vw by (force simp: constant_on_def)
   4.329 +    show "False"
   4.330 +      using m [of v] m [of w] n [of v] n [of w] vw
   4.331 +      by (auto simp: algebra_simps \<open>v \<in> V\<close> \<open>w \<in> W\<close> qV qW)
   4.332 +  qed
   4.333 +qed
   4.334 +
   4.335 +
   4.336 +corollary contractible_imp_unicoherent:
   4.337 +  fixes U :: "'a::euclidean_space set"
   4.338 +  assumes "contractible U"  shows "unicoherent U"
   4.339 +  by (simp add: Borsukian_imp_unicoherent assms contractible_imp_Borsukian)
   4.340 +
   4.341 +corollary convex_imp_unicoherent:
   4.342 +  fixes U :: "'a::euclidean_space set"
   4.343 +  assumes "convex U"  shows "unicoherent U"
   4.344 +  by (simp add: Borsukian_imp_unicoherent assms convex_imp_Borsukian)
   4.345 +
   4.346 +text\<open>If the type class constraint can be relaxed, I don't know how!\<close>
   4.347 +corollary unicoherent_UNIV: "unicoherent (UNIV :: 'a :: euclidean_space set)"
   4.348 +  by (simp add: convex_imp_unicoherent)
   4.349 +
   4.350 +
   4.351 +lemma unicoherent_monotone_image_compact:
   4.352 +  fixes T :: "'b :: t2_space set"
   4.353 +  assumes S: "unicoherent S" "compact S" and contf: "continuous_on S f" and fim: "f ` S = T"
   4.354 +  and conn: "\<And>y. y \<in> T \<Longrightarrow> connected (S \<inter> f -` {y})"
   4.355 +  shows "unicoherent T"
   4.356 +proof
   4.357 +  fix U V
   4.358 +  assume UV: "connected U" "connected V" "T = U \<union> V"
   4.359 +     and cloU: "closedin (subtopology euclidean T) U"
   4.360 +     and cloV: "closedin (subtopology euclidean T) V"
   4.361 +  moreover have "compact T"
   4.362 +    using \<open>compact S\<close> compact_continuous_image contf fim by blast
   4.363 +  ultimately have "closed U" "closed V"
   4.364 +    by (auto simp: closedin_closed_eq compact_imp_closed)
   4.365 +  let ?SUV = "(S \<inter> f -` U) \<inter> (S \<inter> f -` V)"
   4.366 +  have UV_eq: "f ` ?SUV = U \<inter> V"
   4.367 +    using \<open>T = U \<union> V\<close> fim by force+
   4.368 +  have "connected (f ` ?SUV)"
   4.369 +  proof (rule connected_continuous_image)
   4.370 +    show "continuous_on ?SUV f"
   4.371 +      by (meson contf continuous_on_subset inf_le1)
   4.372 +    show "connected ?SUV"
   4.373 +    proof (rule unicoherentD [OF \<open>unicoherent S\<close>, of "S \<inter> f -` U" "S \<inter> f -` V"])
   4.374 +      have "\<And>C. closedin (subtopology euclidean S) C \<Longrightarrow> closedin (subtopology euclidean T) (f ` C)"
   4.375 +        by (metis \<open>compact S\<close> closed_subset closedin_compact closedin_imp_subset compact_continuous_image compact_imp_closed contf continuous_on_subset fim image_mono)
   4.376 +      then show "connected (S \<inter> f -` U)" "connected (S \<inter> f -` V)"
   4.377 +        using UV by (auto simp: conn intro: connected_closed_monotone_preimage [OF contf fim])
   4.378 +      show "S = (S \<inter> f -` U) \<union> (S \<inter> f -` V)"
   4.379 +        using UV fim by blast
   4.380 +      show "closedin (subtopology euclidean S) (S \<inter> f -` U)"
   4.381 +            "closedin (subtopology euclidean S) (S \<inter> f -` V)"
   4.382 +        by (auto simp: continuous_on_imp_closedin cloU cloV contf fim)
   4.383 +    qed
   4.384 +  qed
   4.385 +  with UV_eq show "connected (U \<inter> V)"
   4.386 +    by simp
   4.387 +qed
   4.388 +
   4.389 +
   4.390 +
   4.391 +subsection\<open>Several common variants of unicoherence\<close>
   4.392 +
   4.393 +lemma connected_frontier_simple:
   4.394 +  fixes S :: "'a :: euclidean_space set"
   4.395 +  assumes "connected S" "connected(- S)" shows "connected(frontier S)"
   4.396 +  unfolding frontier_closures
   4.397 +  apply (rule unicoherentD [OF unicoherent_UNIV])
   4.398 +      apply (simp_all add: assms connected_imp_connected_closure)
   4.399 +  by (simp add: closure_def)
   4.400 +
   4.401 +lemma connected_frontier_component_complement:
   4.402 +  fixes S :: "'a :: euclidean_space set"
   4.403 +  assumes "connected S" and C: "C \<in> components(- S)" shows "connected(frontier C)"
   4.404 +  apply (rule connected_frontier_simple)
   4.405 +  using C in_components_connected apply blast
   4.406 +  by (metis Compl_eq_Diff_UNIV connected_UNIV assms top_greatest component_complement_connected)
   4.407 +
   4.408 +lemma connected_frontier_disjoint:
   4.409 +  fixes S :: "'a :: euclidean_space set"
   4.410 +  assumes "connected S" "connected T" "disjnt S T" and ST: "frontier S \<subseteq> frontier T"
   4.411 +  shows "connected(frontier S)"
   4.412 +proof (cases "S = UNIV")
   4.413 +  case True then show ?thesis
   4.414 +    by simp
   4.415 +next
   4.416 +  case False
   4.417 +  then have "-S \<noteq> {}"
   4.418 +    by blast
   4.419 +  then obtain C where C: "C \<in> components(- S)" and "T \<subseteq> C"
   4.420 +    by (metis ComplI disjnt_iff subsetI exists_component_superset \<open>disjnt S T\<close> \<open>connected T\<close>)
   4.421 +  moreover have "frontier S = frontier C"
   4.422 +  proof -
   4.423 +    have "frontier C \<subseteq> frontier S"
   4.424 +      using C frontier_complement frontier_of_components_subset by blast
   4.425 +    moreover have "x \<in> frontier C" if "x \<in> frontier S" for x
   4.426 +    proof -
   4.427 +      have "x \<in> closure C"
   4.428 +        using that unfolding frontier_def
   4.429 +        by (metis (no_types) Diff_eq ST \<open>T \<subseteq> C\<close> closure_mono contra_subsetD frontier_def le_inf_iff that)
   4.430 +      moreover have "x \<notin> interior C"
   4.431 +        using that unfolding frontier_def
   4.432 +        by (metis C Compl_eq_Diff_UNIV Diff_iff subsetD in_components_subset interior_diff interior_mono)
   4.433 +      ultimately show ?thesis
   4.434 +        by (auto simp: frontier_def)
   4.435 +    qed
   4.436 +    ultimately show ?thesis
   4.437 +      by blast
   4.438 +  qed
   4.439 +  ultimately show ?thesis
   4.440 +    using \<open>connected S\<close> connected_frontier_component_complement by auto
   4.441 +qed
   4.442 +
   4.443 +lemma separation_by_component_closed_pointwise:
   4.444 +  fixes S :: "'a :: euclidean_space set"
   4.445 +  assumes "closed S" "\<not> connected_component (- S) a b"
   4.446 +  obtains C where "C \<in> components S" "\<not> connected_component(- C) a b"
   4.447 +proof (cases "a \<in> S \<or> b \<in> S")
   4.448 +  case True
   4.449 +  then show ?thesis
   4.450 +    using connected_component_in componentsI that by fastforce
   4.451 +next
   4.452 +  case False
   4.453 +  obtain T where "T \<subseteq> S" "closed T" "T \<noteq> {}"
   4.454 +             and nab: "\<not> connected_component (- T) a b"
   4.455 +             and conn: "\<And>U. U \<subset> T \<Longrightarrow> connected_component (- U) a b"
   4.456 +    using closed_irreducible_separator [OF assms] by metis
   4.457 +  moreover have "connected T"
   4.458 +  proof -
   4.459 +    have ab: "frontier(connected_component_set (- T) a) = T" "frontier(connected_component_set (- T) b) = T"
   4.460 +      using frontier_minimal_separating_closed_pointwise
   4.461 +      by (metis False \<open>T \<subseteq> S\<close> \<open>closed T\<close> connected_component_sym conn connected_component_eq_empty connected_component_intermediate_subset empty_subsetI nab)+
   4.462 +    have "connected (frontier (connected_component_set (- T) a))"
   4.463 +    proof (rule connected_frontier_disjoint)
   4.464 +      show "disjnt (connected_component_set (- T) a) (connected_component_set (- T) b)"
   4.465 +        unfolding disjnt_iff
   4.466 +        by (metis connected_component_eq connected_component_eq_empty connected_component_idemp mem_Collect_eq nab)
   4.467 +      show "frontier (connected_component_set (- T) a) \<subseteq> frontier (connected_component_set (- T) b)"
   4.468 +        by (simp add: ab)
   4.469 +    qed auto
   4.470 +    with ab \<open>closed T\<close> show ?thesis
   4.471 +      by simp
   4.472 +  qed
   4.473 +  ultimately obtain C where "C \<in> components S" "T \<subseteq> C"
   4.474 +    using exists_component_superset [of T S] by blast
   4.475 +  then show ?thesis
   4.476 +    by (meson Compl_anti_mono connected_component_of_subset nab that)
   4.477 +qed
   4.478 +
   4.479 +
   4.480 +lemma separation_by_component_closed:
   4.481 +  fixes S :: "'a :: euclidean_space set"
   4.482 +  assumes "closed S" "\<not> connected(- S)"
   4.483 +  obtains C where "C \<in> components S" "\<not> connected(- C)"
   4.484 +proof -
   4.485 +  obtain x y where "closed S" "x \<notin> S" "y \<notin> S" and "\<not> connected_component (- S) x y"
   4.486 +    using assms by (auto simp: connected_iff_connected_component)
   4.487 +  then obtain C where "C \<in> components S" "\<not> connected_component(- C) x y"
   4.488 +    using separation_by_component_closed_pointwise by metis
   4.489 +  then show "thesis"
   4.490 +    apply (clarify elim!: componentsE)
   4.491 +    by (metis Compl_iff \<open>C \<in> components S\<close> \<open>x \<notin> S\<close> \<open>y \<notin> S\<close> connected_component_eq connected_component_eq_eq connected_iff_connected_component that)
   4.492 +qed
   4.493 +
   4.494 +lemma separation_by_Un_closed_pointwise:
   4.495 +  fixes S :: "'a :: euclidean_space set"
   4.496 +  assumes ST: "closed S" "closed T" "S \<inter> T = {}"
   4.497 +      and conS: "connected_component (- S) a b" and conT: "connected_component (- T) a b"
   4.498 +    shows "connected_component (- (S \<union> T)) a b"
   4.499 +proof (rule ccontr)
   4.500 +  have "a \<notin> S" "b \<notin> S" "a \<notin> T" "b \<notin> T"
   4.501 +    using conS conT connected_component_in by auto
   4.502 +  assume "\<not> connected_component (- (S \<union> T)) a b"
   4.503 +  then obtain C where "C \<in> components (S \<union> T)" and C: "\<not> connected_component(- C) a b"
   4.504 +    using separation_by_component_closed_pointwise assms by blast
   4.505 +  then have "C \<subseteq> S \<or> C \<subseteq> T"
   4.506 +  proof -
   4.507 +    have "connected C" "C \<subseteq> S \<union> T"
   4.508 +      using \<open>C \<in> components (S \<union> T)\<close> in_components_subset by (blast elim: componentsE)+
   4.509 +    moreover then have "C \<inter> T = {} \<or> C \<inter> S = {}"
   4.510 +      by (metis Int_empty_right ST inf.commute connected_closed)
   4.511 +    ultimately show ?thesis
   4.512 +      by blast
   4.513 +  qed
   4.514 +  then show False
   4.515 +    by (meson Compl_anti_mono C conS conT connected_component_of_subset)
   4.516 +qed
   4.517 +
   4.518 +lemma separation_by_Un_closed:
   4.519 +  fixes S :: "'a :: euclidean_space set"
   4.520 +  assumes ST: "closed S" "closed T" "S \<inter> T = {}" and conS: "connected(- S)" and conT: "connected(- T)"
   4.521 +  shows "connected(- (S \<union> T))"
   4.522 +  using assms separation_by_Un_closed_pointwise
   4.523 +  by (fastforce simp add: connected_iff_connected_component)
   4.524 +
   4.525 +lemma open_unicoherent_UNIV:
   4.526 +  fixes S :: "'a :: euclidean_space set"
   4.527 +  assumes "open S" "open T" "connected S" "connected T" "S \<union> T = UNIV"
   4.528 +  shows "connected(S \<inter> T)"
   4.529 +proof -
   4.530 +  have "connected(- (-S \<union> -T))"
   4.531 +    by (metis closed_Compl compl_sup compl_top_eq double_compl separation_by_Un_closed assms)
   4.532 +  then show ?thesis
   4.533 +    by simp
   4.534 +qed
   4.535 +
   4.536 +lemma separation_by_component_open_aux:
   4.537 +  fixes S :: "'a :: euclidean_space set"
   4.538 +  assumes ST: "closed S" "closed T" "S \<inter> T = {}"
   4.539 +      and "S \<noteq> {}" "T \<noteq> {}"
   4.540 +  obtains C where "C \<in> components(-(S \<union> T))" "C \<noteq> {}" "frontier C \<inter> S \<noteq> {}" "frontier C \<inter> T \<noteq> {}"
   4.541 +proof (rule ccontr)
   4.542 +  let ?S = "S \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> S}"
   4.543 +  let ?T = "T \<union> \<Union>{C \<in> components(- (S \<union> T)). frontier C \<subseteq> T}"
   4.544 +  assume "~ thesis"
   4.545 +  with that have *: "frontier C \<inter> S = {} \<or> frontier C \<inter> T = {}"
   4.546 +            if C: "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
   4.547 +    using C by blast
   4.548 +  have "\<exists>A B::'a set. closed A \<and> closed B \<and> UNIV \<subseteq> A \<union> B \<and> A \<inter> B = {} \<and> A \<noteq> {} \<and> B \<noteq> {}"
   4.549 +  proof (intro exI conjI)
   4.550 +    have "frontier (\<Union>{C \<in> components (- S \<inter> - T). frontier C \<subseteq> S}) \<subseteq> S"
   4.551 +      apply (rule subset_trans [OF frontier_Union_subset_closure])
   4.552 +      by (metis (no_types, lifting) SUP_least \<open>closed S\<close> closure_minimal mem_Collect_eq)
   4.553 +    then have "frontier ?S \<subseteq> S"
   4.554 +      by (simp add: frontier_subset_eq assms  subset_trans [OF frontier_Un_subset])
   4.555 +    then show "closed ?S"
   4.556 +      using frontier_subset_eq by fastforce
   4.557 +    have "frontier (\<Union>{C \<in> components (- S \<inter> - T). frontier C \<subseteq> T}) \<subseteq> T"
   4.558 +      apply (rule subset_trans [OF frontier_Union_subset_closure])
   4.559 +      by (metis (no_types, lifting) SUP_least \<open>closed T\<close> closure_minimal mem_Collect_eq)
   4.560 +    then have "frontier ?T \<subseteq> T"
   4.561 +      by (simp add: frontier_subset_eq assms  subset_trans [OF frontier_Un_subset])
   4.562 +    then show "closed ?T"
   4.563 +      using frontier_subset_eq by fastforce
   4.564 +    have "UNIV \<subseteq> (S \<union> T) \<union> \<Union>(components(- (S \<union> T)))"
   4.565 +      using Union_components by blast
   4.566 +    also have "...  \<subseteq> ?S \<union> ?T"
   4.567 +    proof -
   4.568 +      have "C \<in> components (-(S \<union> T)) \<and> frontier C \<subseteq> S \<or>
   4.569 +            C \<in> components (-(S \<union> T)) \<and> frontier C \<subseteq> T"
   4.570 +        if "C \<in> components (- (S \<union> T))" "C \<noteq> {}" for C
   4.571 +        using * [OF that] that
   4.572 +        by clarify (metis (no_types, lifting) UnE \<open>closed S\<close> \<open>closed T\<close> closed_Un disjoint_iff_not_equal frontier_of_components_closed_complement subsetCE)
   4.573 +      then show ?thesis
   4.574 +        by blast
   4.575 +    qed
   4.576 +    finally show "UNIV \<subseteq> ?S \<union> ?T" .
   4.577 +    have "\<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> S} \<union>
   4.578 +          \<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> T} \<subseteq> - (S \<union> T)"
   4.579 +      using in_components_subset by fastforce
   4.580 +    moreover have "\<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> S} \<inter>
   4.581 +                   \<Union>{C \<in> components (- (S \<union> T)). frontier C \<subseteq> T} = {}"
   4.582 +    proof -
   4.583 +      have "C \<inter> C' = {}" if "C \<in> components (- (S \<union> T))" "frontier C \<subseteq> S"
   4.584 +                            "C' \<in> components (- (S \<union> T))" "frontier C' \<subseteq> T" for C C'
   4.585 +      proof -
   4.586 +        have NUN: "- S \<inter> - T \<noteq> UNIV"
   4.587 +          using \<open>T \<noteq> {}\<close> by blast
   4.588 +        have "C \<noteq> C'"
   4.589 +        proof
   4.590 +          assume "C = C'"
   4.591 +          with that have "frontier C' \<subseteq> S \<inter> T"
   4.592 +            by simp
   4.593 +          also have "... = {}"
   4.594 +            using \<open>S \<inter> T = {}\<close> by blast
   4.595 +          finally have "C' = {} \<or> C' = UNIV"
   4.596 +            using frontier_eq_empty by auto
   4.597 +          then show False
   4.598 +            using \<open>C = C'\<close> NUN that by (force simp: dest: in_components_nonempty in_components_subset)
   4.599 +        qed
   4.600 +        with that show ?thesis
   4.601 +          by (simp add: components_nonoverlap [of _ "-(S \<union> T)"])
   4.602 +      qed
   4.603 +      then show ?thesis
   4.604 +        by blast
   4.605 +    qed
   4.606 +    ultimately show "?S \<inter> ?T = {}"
   4.607 +      using ST by blast
   4.608 +    show "?S \<noteq> {}" "?T \<noteq> {}"
   4.609 +      using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> by blast+
   4.610 +  qed
   4.611 +    then show False
   4.612 +      by (metis Compl_disjoint Convex_Euclidean_Space.connected_UNIV compl_bot_eq compl_unique connected_closedD inf_sup_absorb sup_compl_top_left1 top.extremum_uniqueI)
   4.613 +qed
   4.614 +
   4.615 +
   4.616 +lemma separation_by_component_open:
   4.617 +  fixes S :: "'a :: euclidean_space set"
   4.618 +  assumes "open S" and non: "\<not> connected(- S)"
   4.619 +  obtains C where "C \<in> components S" "\<not> connected(- C)"
   4.620 +proof -
   4.621 +  obtain T U
   4.622 +    where "closed T" "closed U" and TU: "T \<union> U = - S" "T \<inter> U = {}" "T \<noteq> {}" "U \<noteq> {}"
   4.623 +    using assms by (auto simp: connected_closed_set closed_def)
   4.624 +  then obtain C where C: "C \<in> components(-(T \<union> U))" "C \<noteq> {}"
   4.625 +          and "frontier C \<inter> T \<noteq> {}" "frontier C \<inter> U \<noteq> {}"
   4.626 +    using separation_by_component_open_aux [OF \<open>closed T\<close> \<open>closed U\<close> \<open>T \<inter> U = {}\<close>] by force
   4.627 +  show "thesis"
   4.628 +  proof
   4.629 +    show "C \<in> components S"
   4.630 +      using C(1) TU(1) by auto
   4.631 +    show "\<not> connected (- C)"
   4.632 +    proof
   4.633 +      assume "connected (- C)"
   4.634 +      then have "connected (frontier C)"
   4.635 +        using connected_frontier_simple [of C] \<open>C \<in> components S\<close> in_components_connected by blast
   4.636 +      then show False
   4.637 +        unfolding connected_closed
   4.638 +        by (metis C(1) TU(2) \<open>closed T\<close> \<open>closed U\<close> \<open>frontier C \<inter> T \<noteq> {}\<close> \<open>frontier C \<inter> U \<noteq> {}\<close> closed_Un frontier_of_components_closed_complement inf_bot_right inf_commute)
   4.639 +    qed
   4.640 +  qed
   4.641 +qed
   4.642 +
   4.643 +lemma separation_by_Un_open:
   4.644 +  fixes S :: "'a :: euclidean_space set"
   4.645 +  assumes "open S" "open T" "S \<inter> T = {}" and cS: "connected(-S)" and cT: "connected(-T)"
   4.646 +    shows "connected(- (S \<union> T))"
   4.647 +  using assms unicoherent_UNIV unfolding unicoherent_def by force
   4.648 +
   4.649 +
   4.650 +lemma nonseparation_by_component_eq:
   4.651 +  fixes S :: "'a :: euclidean_space set"
   4.652 +  assumes "open S \<or> closed S"
   4.653 +  shows "((\<forall>C \<in> components S. connected(-C)) \<longleftrightarrow> connected(- S))" (is "?lhs = ?rhs")
   4.654 +proof
   4.655 +  assume ?lhs with assms show ?rhs
   4.656 +    by (meson separation_by_component_closed separation_by_component_open)
   4.657 +next
   4.658 +  assume ?rhs with assms show ?lhs
   4.659 +    using component_complement_connected by force
   4.660 +qed
   4.661 +
   4.662 +
   4.663 +text\<open>Another interesting equivalent of an inessential mapping into C-{0}\<close>
   4.664 +proposition inessential_eq_extensible:
   4.665 +  fixes f :: "'a::euclidean_space \<Rightarrow> complex"
   4.666 +  assumes "closed S"
   4.667 +  shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)) \<longleftrightarrow>
   4.668 +         (\<exists>g. continuous_on UNIV g \<and> (\<forall>x \<in> S. g x = f x) \<and> (\<forall>x. g x \<noteq> 0))"
   4.669 +     (is "?lhs = ?rhs")
   4.670 +proof
   4.671 +  assume ?lhs
   4.672 +  then obtain a where a: "homotopic_with (\<lambda>h. True) S (-{0}) f (\<lambda>t. a)" ..
   4.673 +  show ?rhs
   4.674 +  proof (cases "S = {}")
   4.675 +    case True
   4.676 +    with a show ?thesis
   4.677 +      using continuous_on_const by force
   4.678 +  next
   4.679 +    case False
   4.680 +    have anr: "ANR (-{0::complex})"
   4.681 +      by (simp add: ANR_delete open_Compl open_imp_ANR)
   4.682 +    obtain g where contg: "continuous_on UNIV g" and gim: "g ` UNIV \<subseteq> -{0}"
   4.683 +                   and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   4.684 +    proof (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ homotopic_with_symD [OF a]])
   4.685 +      show "closedin (subtopology euclidean UNIV) S"
   4.686 +        using assms by auto
   4.687 +      show "range (\<lambda>t. a) \<subseteq> - {0}"
   4.688 +        using a homotopic_with_imp_subset2 False by blast
   4.689 +    qed (use anr that in \<open>force+\<close>)
   4.690 +    then show ?thesis
   4.691 +      by force
   4.692 +  qed
   4.693 +next
   4.694 +  assume ?rhs
   4.695 +  then obtain g where contg: "continuous_on UNIV g"
   4.696 +          and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" and non0: "\<And>x. g x \<noteq> 0"
   4.697 +    by metis
   4.698 +  obtain h k::"'a\<Rightarrow>'a" where hk: "homeomorphism (ball 0 1) UNIV h k"
   4.699 +    using homeomorphic_ball01_UNIV homeomorphic_def by blast
   4.700 +  then have "continuous_on (ball 0 1) (g \<circ> h)"
   4.701 +    by (meson contg continuous_on_compose continuous_on_subset homeomorphism_cont1 top_greatest)
   4.702 +  then obtain j where contj: "continuous_on (ball 0 1) j"
   4.703 +                  and j: "\<And>z. z \<in> ball 0 1 \<Longrightarrow> exp(j z) = (g \<circ> h) z"
   4.704 +    by (metis (mono_tags, hide_lams) continuous_logarithm_on_ball comp_apply non0)
   4.705 +  have [simp]: "\<And>x. x \<in> S \<Longrightarrow> h (k x) = x"
   4.706 +    using hk homeomorphism_apply2 by blast
   4.707 +  have "\<exists>\<zeta>. continuous_on S \<zeta>\<and> (\<forall>x\<in>S. f x = exp (\<zeta> x))"
   4.708 +  proof (intro exI conjI ballI)
   4.709 +    show "continuous_on S (j \<circ> k)"
   4.710 +    proof (rule continuous_on_compose)
   4.711 +      show "continuous_on S k"
   4.712 +        by (meson continuous_on_subset hk homeomorphism_cont2 top_greatest)
   4.713 +      show "continuous_on (k ` S) j"
   4.714 +        apply (rule continuous_on_subset [OF contj])
   4.715 +        using homeomorphism_image2 [OF hk] continuous_on_subset [OF contj] by blast
   4.716 +    qed
   4.717 +    show "f x = exp ((j \<circ> k) x)" if "x \<in> S" for x
   4.718 +    proof -
   4.719 +      have "f x = (g \<circ> h) (k x)"
   4.720 +        by (simp add: gf that)
   4.721 +      also have "... = exp (j (k x))"
   4.722 +        by (metis rangeI homeomorphism_image2 [OF hk] j)
   4.723 +      finally show ?thesis by simp
   4.724 +    qed
   4.725 +  qed
   4.726 +  then show ?lhs
   4.727 +    by (simp add: inessential_eq_continuous_logarithm)
   4.728 +qed
   4.729 +
   4.730 +lemma inessential_on_clopen_Union:
   4.731 +  fixes \<F> :: "'a::euclidean_space set set"
   4.732 +  assumes T: "path_connected T"
   4.733 +      and "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
   4.734 +      and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
   4.735 +      and hom: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a. homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)"
   4.736 +  obtains a where "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
   4.737 +proof (cases "\<Union>\<F> = {}")
   4.738 +  case True
   4.739 +  with that show ?thesis
   4.740 +    by force
   4.741 +next
   4.742 +  case False
   4.743 +  then obtain C where "C \<in> \<F>" "C \<noteq> {}"
   4.744 +    by blast
   4.745 +  then obtain a where clo: "closedin (subtopology euclidean (\<Union>\<F>)) C"
   4.746 +    and ope: "openin (subtopology euclidean (\<Union>\<F>)) C"
   4.747 +    and "homotopic_with (\<lambda>x. True) C T f (\<lambda>x. a)"
   4.748 +    using assms by blast
   4.749 +  with \<open>C \<noteq> {}\<close> have "f ` C \<subseteq> T" "a \<in> T"
   4.750 +    using homotopic_with_imp_subset1 homotopic_with_imp_subset2 by blast+
   4.751 +  have "homotopic_with (\<lambda>x. True) (\<Union>\<F>) T f (\<lambda>x. a)"
   4.752 +  proof (rule homotopic_on_clopen_Union)
   4.753 +    show "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
   4.754 +         "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
   4.755 +      by (simp_all add: assms)
   4.756 +    show "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. a)" if "S \<in> \<F>" for S
   4.757 +    proof (cases "S = {}")
   4.758 +      case True
   4.759 +      then show ?thesis
   4.760 +        by auto
   4.761 +    next
   4.762 +      case False
   4.763 +      then obtain b where "b \<in> S"
   4.764 +        by blast
   4.765 +      obtain c where c: "homotopic_with (\<lambda>x. True) S T f (\<lambda>x. c)"
   4.766 +        using \<open>S \<in> \<F>\<close> hom by blast
   4.767 +      then have "c \<in> T"
   4.768 +        using \<open>b \<in> S\<close> homotopic_with_imp_subset2 by blast
   4.769 +      then have "homotopic_with (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. c)"
   4.770 +        using T \<open>a \<in> T\<close> homotopic_constant_maps path_connected_component by blast
   4.771 +      then show ?thesis
   4.772 +        using c homotopic_with_symD homotopic_with_trans by blast
   4.773 +    qed
   4.774 +  qed
   4.775 +  then show ?thesis ..
   4.776 +qed
   4.777 +
   4.778 +lemma Janiszewski_dual:
   4.779 +  fixes S :: "complex set"
   4.780 +  assumes
   4.781 +   "compact S" "compact T" "connected S" "connected T" "connected(- (S \<union> T))"
   4.782 + shows "connected(S \<inter> T)"
   4.783 +proof -
   4.784 +  have ST: "compact (S \<union> T)"
   4.785 +    by (simp add: assms compact_Un)
   4.786 +  with Borsukian_imp_unicoherent [of "S \<union> T"] ST assms
   4.787 +  show ?thesis
   4.788 +    by (auto simp: closed_subset compact_imp_closed Borsukian_separation_compact unicoherent_def)
   4.789 +qed
   4.790 +
   4.791  end
     5.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Oct 29 19:39:03 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Oct 30 16:02:59 2017 +0000
     5.3 @@ -6969,7 +6969,7 @@
     5.4    shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
     5.5  apply (rule iffI)
     5.6  using homotopy_eqv_def apply fastforce
     5.7 -by (simp add: homotopy_eqv_contractible_sets contractible_empty)
     5.8 +by (simp add: homotopy_eqv_contractible_sets)
     5.9  
    5.10  lemma homotopy_eqv_empty2 [simp]:
    5.11    fixes S :: "'a::real_normed_vector set"
     6.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 29 19:39:03 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 30 16:02:59 2017 +0000
     6.3 @@ -2501,6 +2501,29 @@
     6.4  lemma frontier_closures: "frontier S = closure S \<inter> closure (- S)"
     6.5    by (auto simp: frontier_def interior_closure)
     6.6  
     6.7 +lemma frontier_Int: "frontier(S \<inter> T) = closure(S \<inter> T) \<inter> (frontier S \<union> frontier T)"
     6.8 +proof -
     6.9 +  have "closure (S \<inter> T) \<subseteq> closure S" "closure (S \<inter> T) \<subseteq> closure T"
    6.10 +    by (simp_all add: closure_mono)
    6.11 +  then show ?thesis
    6.12 +    by (auto simp: frontier_closures)
    6.13 +qed
    6.14 +
    6.15 +lemma frontier_Int_subset: "frontier(S \<inter> T) \<subseteq> frontier S \<union> frontier T"
    6.16 +  by (auto simp: frontier_Int)
    6.17 +
    6.18 +lemma frontier_Int_closed:
    6.19 +  assumes "closed S" "closed T"
    6.20 +  shows "frontier(S \<inter> T) = (frontier S \<inter> T) \<union> (S \<inter> frontier T)"
    6.21 +proof -
    6.22 +  have "closure (S \<inter> T) = T \<inter> S"
    6.23 +    using assms by (simp add: Int_commute closed_Int)
    6.24 +  moreover have "T \<inter> (closure S \<inter> closure (- S)) = frontier S \<inter> T"
    6.25 +    by (simp add: Int_commute frontier_closures)
    6.26 +  ultimately show ?thesis
    6.27 +    by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
    6.28 +qed
    6.29 +
    6.30  lemma frontier_straddle:
    6.31    fixes a :: "'a::metric_space"
    6.32    shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
    6.33 @@ -2528,6 +2551,9 @@
    6.34  lemma frontier_complement [simp]: "frontier (- S) = frontier S"
    6.35    by (auto simp: frontier_def closure_complement interior_complement)
    6.36  
    6.37 +lemma frontier_Un_subset: "frontier(S \<union> T) \<subseteq> frontier S \<union> frontier T"
    6.38 +  by (metis compl_sup frontier_Int_subset frontier_complement)
    6.39 +
    6.40  lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
    6.41    using frontier_complement frontier_subset_eq[of "- S"]
    6.42    unfolding open_closed by auto