src/HOL/Analysis/Brouwer_Fixpoint.thy
changeset 66939 04678058308f
parent 66884 c2128ab11f61
child 67399 eab6ce8368fa
     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