facts about ANRs, ENRs, covering spaces
authorpaulson <lp15@cam.ac.uk>
Thu Jan 05 16:37:49 2017 +0000 (2017-01-05)
changeset 6479105a2b3b20664
parent 64790 ed38f9a834d8
child 64792 3074080f4f12
facts about ANRs, ENRs, covering spaces
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Jan 05 16:03:23 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Jan 05 16:37:49 2017 +0000
     1.3 @@ -4051,7 +4051,6 @@
     1.4    assumes "AR S" "AR T" shows "AR(S \<times> T)"
     1.5  using assms by (simp add: AR_ANR ANR_Times contractible_Times)
     1.6  
     1.7 -
     1.8  lemma ENR_rel_frontier_convex:
     1.9    fixes S :: "'a::euclidean_space set"
    1.10    assumes "bounded S" "convex S"
    1.11 @@ -4092,6 +4091,297 @@
    1.12    assumes "bounded S" "convex S"
    1.13      shows "ANR(rel_frontier S)"
    1.14  by (simp add: ENR_imp_ANR ENR_rel_frontier_convex assms)
    1.15 +    
    1.16 +lemma ENR_closedin_Un_local:
    1.17 +  fixes S :: "'a::euclidean_space set"
    1.18 +  shows "\<lbrakk>ENR S; ENR T; ENR(S \<inter> T);
    1.19 +          closedin (subtopology euclidean (S \<union> T)) S; closedin (subtopology euclidean (S \<union> T)) T\<rbrakk>
    1.20 +        \<Longrightarrow> ENR(S \<union> T)"
    1.21 +by (simp add: ENR_ANR ANR_closed_Un_local locally_compact_closedin_Un)
    1.22 +
    1.23 +lemma ENR_closed_Un:
    1.24 +  fixes S :: "'a::euclidean_space set"
    1.25 +  shows "\<lbrakk>closed S; closed T; ENR S; ENR T; ENR(S \<inter> T)\<rbrakk> \<Longrightarrow> ENR(S \<union> T)"
    1.26 +by (auto simp: closed_subset ENR_closedin_Un_local)
    1.27 +
    1.28 +lemma absolute_retract_Un:
    1.29 +  fixes S :: "'a::euclidean_space set"
    1.30 +  shows "\<lbrakk>S retract_of UNIV; T retract_of UNIV; (S \<inter> T) retract_of UNIV\<rbrakk>
    1.31 +         \<Longrightarrow> (S \<union> T) retract_of UNIV"
    1.32 +  by (meson AR_closed_Un_local_aux closed_subset retract_of_UNIV retract_of_imp_subset)
    1.33 +
    1.34 +lemma retract_from_Un_Int:
    1.35 +  fixes S :: "'a::euclidean_space set"
    1.36 +  assumes clS: "closedin (subtopology euclidean (S \<union> T)) S"
    1.37 +      and clT: "closedin (subtopology euclidean (S \<union> T)) T"
    1.38 +      and Un: "(S \<union> T) retract_of U" and Int: "(S \<inter> T) retract_of T"
    1.39 +    shows "S retract_of U"
    1.40 +proof -
    1.41 +  obtain r where r: "continuous_on T r" "r ` T \<subseteq> S \<inter> T" "\<forall>x\<in>S \<inter> T. r x = x"
    1.42 +    using Int by (auto simp: retraction_def retract_of_def)
    1.43 +  have "S retract_of S \<union> T"
    1.44 +    unfolding retraction_def retract_of_def
    1.45 +  proof (intro exI conjI)
    1.46 +    show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then x else r x)"
    1.47 +      apply (rule continuous_on_cases_local [OF clS clT])
    1.48 +      using r by (auto simp: continuous_on_id)
    1.49 +  qed (use r in auto)
    1.50 +  also have "... retract_of U"
    1.51 +    by (rule Un)
    1.52 +  finally show ?thesis .
    1.53 +qed
    1.54 +
    1.55 +lemma AR_from_Un_Int_local:
    1.56 +  fixes S :: "'a::euclidean_space set"
    1.57 +  assumes clS: "closedin (subtopology euclidean (S \<union> T)) S"
    1.58 +      and clT: "closedin (subtopology euclidean (S \<union> T)) T"
    1.59 +      and Un: "AR(S \<union> T)" and Int: "AR(S \<inter> T)"
    1.60 +    shows "AR S"
    1.61 +  apply (rule AR_retract_of_AR [OF Un])
    1.62 +  by (meson AR_imp_retract clS clT closedin_closed_subset local.Int retract_from_Un_Int retract_of_refl sup_ge2)
    1.63 +
    1.64 +lemma AR_from_Un_Int_local':
    1.65 +  fixes S :: "'a::euclidean_space set"
    1.66 +  assumes "closedin (subtopology euclidean (S \<union> T)) S"
    1.67 +      and "closedin (subtopology euclidean (S \<union> T)) T"
    1.68 +      and "AR(S \<union> T)" "AR(S \<inter> T)"
    1.69 +    shows "AR T"
    1.70 +  using AR_from_Un_Int_local [of T S] assms by (simp add: Un_commute Int_commute)
    1.71 +
    1.72 +lemma AR_from_Un_Int:
    1.73 +  fixes S :: "'a::euclidean_space set"
    1.74 +  assumes clo: "closed S" "closed T" and Un: "AR(S \<union> T)" and Int: "AR(S \<inter> T)"
    1.75 +  shows "AR S"
    1.76 +  by (metis AR_from_Un_Int_local [OF _ _ Un Int] Un_commute clo closed_closedin closedin_closed_subset inf_sup_absorb subtopology_UNIV top_greatest)
    1.77 +
    1.78 +lemma ANR_from_Un_Int_local:
    1.79 +  fixes S :: "'a::euclidean_space set"
    1.80 +  assumes clS: "closedin (subtopology euclidean (S \<union> T)) S"
    1.81 +      and clT: "closedin (subtopology euclidean (S \<union> T)) T"
    1.82 +      and Un: "ANR(S \<union> T)" and Int: "ANR(S \<inter> T)"
    1.83 +    shows "ANR S"
    1.84 +proof -
    1.85 +  obtain V where clo: "closedin (subtopology euclidean (S \<union> T)) (S \<inter> T)"
    1.86 +             and ope: "openin (subtopology euclidean (S \<union> T)) V"
    1.87 +             and ret: "S \<inter> T retract_of V"
    1.88 +    using ANR_imp_neighbourhood_retract [OF Int] by (metis clS clT closedin_Int)
    1.89 +  then obtain r where r: "continuous_on V r" and rim: "r ` V \<subseteq> S \<inter> T" and req: "\<forall>x\<in>S \<inter> T. r x = x"
    1.90 +    by (auto simp: retraction_def retract_of_def)
    1.91 +  have Vsub: "V \<subseteq> S \<union> T"
    1.92 +    by (meson ope openin_contains_cball)
    1.93 +  have Vsup: "S \<inter> T \<subseteq> V"
    1.94 +    by (simp add: retract_of_imp_subset ret)
    1.95 +  then have eq: "S \<union> V = ((S \<union> T) - T) \<union> V"
    1.96 +    by auto
    1.97 +  have eq': "S \<union> V = S \<union> (V \<inter> T)"
    1.98 +    using Vsub by blast
    1.99 +  have "continuous_on (S \<union> V \<inter> T) (\<lambda>x. if x \<in> S then x else r x)"
   1.100 +  proof (rule continuous_on_cases_local)
   1.101 +    show "closedin (subtopology euclidean (S \<union> V \<inter> T)) S"
   1.102 +      using clS closedin_subset_trans inf.boundedE by blast
   1.103 +    show "closedin (subtopology euclidean (S \<union> V \<inter> T)) (V \<inter> T)"
   1.104 +      using clT Vsup by (auto simp: closedin_closed)
   1.105 +    show "continuous_on (V \<inter> T) r"
   1.106 +      by (meson Int_lower1 continuous_on_subset r)
   1.107 +  qed (use req continuous_on_id in auto)
   1.108 +  with rim have "S retract_of S \<union> V"
   1.109 +    unfolding retraction_def retract_of_def
   1.110 +    apply (rule_tac x="\<lambda>x. if x \<in> S then x else r x" in exI)
   1.111 +    apply (auto simp: eq')
   1.112 +    done
   1.113 +  then show ?thesis
   1.114 +    using ANR_neighborhood_retract [OF Un]
   1.115 +    using \<open>S \<union> V = S \<union> T - T \<union> V\<close> clT ope by fastforce
   1.116 +qed
   1.117 +
   1.118 +lemma ANR_from_Un_Int:
   1.119 +  fixes S :: "'a::euclidean_space set"
   1.120 +  assumes clo: "closed S" "closed T" and Un: "ANR(S \<union> T)" and Int: "ANR(S \<inter> T)"
   1.121 +  shows "ANR S"
   1.122 +  by (metis ANR_from_Un_Int_local [OF _ _ Un Int] Un_commute clo closed_closedin closedin_closed_subset inf_sup_absorb subtopology_UNIV top_greatest)
   1.123 +
   1.124 +proposition ANR_finite_Union_convex_closed:
   1.125 +  fixes \<T> :: "'a::euclidean_space set set"
   1.126 +  assumes \<T>: "finite \<T>" and clo: "\<And>C. C \<in> \<T> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<T> \<Longrightarrow> convex C"
   1.127 +  shows "ANR(\<Union>\<T>)"
   1.128 +proof -
   1.129 +  have "ANR(\<Union>\<T>)" if "card \<T> < n" for n
   1.130 +  using assms that
   1.131 +  proof (induction n arbitrary: \<T>)
   1.132 +    case 0 then show ?case by simp
   1.133 +  next
   1.134 +    case (Suc n)
   1.135 +    have "ANR(\<Union>\<U>)" if "finite \<U>" "\<U> \<subseteq> \<T>" for \<U>
   1.136 +      using that
   1.137 +    proof (induction \<U>)
   1.138 +      case empty
   1.139 +      then show ?case  by simp
   1.140 +    next
   1.141 +      case (insert C \<U>)
   1.142 +      have "ANR (C \<union> \<Union>\<U>)"
   1.143 +      proof (rule ANR_closed_Un)
   1.144 +        show "ANR (C \<inter> \<Union>\<U>)"
   1.145 +          unfolding Int_Union
   1.146 +        proof (rule Suc)
   1.147 +          show "finite (op \<inter> C ` \<U>)"
   1.148 +            by (simp add: insert.hyps(1))
   1.149 +          show "\<And>Ca. Ca \<in> op \<inter> C ` \<U> \<Longrightarrow> closed Ca"
   1.150 +            by (metis (no_types, hide_lams) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2)
   1.151 +          show "\<And>Ca. Ca \<in> op \<inter> C ` \<U> \<Longrightarrow> convex Ca"
   1.152 +            by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE)
   1.153 +          show "card (op \<inter> C ` \<U>) < n"
   1.154 +          proof -
   1.155 +            have "card \<T> \<le> n"
   1.156 +              by (meson Suc.prems(4) not_less not_less_eq)
   1.157 +            then show ?thesis
   1.158 +              by (metis Suc.prems(1) card_image_le card_seteq insert.hyps insert.prems insert_subset le_trans not_less)
   1.159 +          qed
   1.160 +        qed
   1.161 +        show "closed (\<Union>\<U>)"
   1.162 +          using Suc.prems(2) insert.hyps(1) insert.prems by blast
   1.163 +      qed (use Suc.prems convex_imp_ANR insert.prems insert.IH in auto)
   1.164 +      then show ?case
   1.165 +        by simp
   1.166 +    qed
   1.167 +    then show ?case
   1.168 +      using Suc.prems(1) by blast
   1.169 +  qed
   1.170 +  then show ?thesis
   1.171 +    by blast
   1.172 +qed
   1.173 +
   1.174 +
   1.175 +lemma finite_imp_ANR:
   1.176 +  fixes S :: "'a::euclidean_space set"
   1.177 +  assumes "finite S"
   1.178 +  shows "ANR S"
   1.179 +proof -
   1.180 +  have "ANR(\<Union>x \<in> S. {x})"
   1.181 +    by (blast intro: ANR_finite_Union_convex_closed assms)
   1.182 +  then show ?thesis
   1.183 +    by simp
   1.184 +qed
   1.185 +
   1.186 +lemma ANR_insert:
   1.187 +  fixes S :: "'a::euclidean_space set"
   1.188 +  assumes "ANR S" "closed S"
   1.189 +  shows "ANR(insert a S)"
   1.190 +  by (metis ANR_closed_Un ANR_empty ANR_singleton Diff_disjoint Diff_insert_absorb assms closed_singleton insert_absorb insert_is_Un)
   1.191 +
   1.192 +lemma ANR_path_component_ANR:
   1.193 +  fixes S :: "'a::euclidean_space set"
   1.194 +  shows "ANR S \<Longrightarrow> ANR(path_component_set S x)"
   1.195 +  using ANR_imp_locally_path_connected ANR_openin openin_path_component_locally_path_connected by blast
   1.196 +
   1.197 +lemma ANR_connected_component_ANR:
   1.198 +  fixes S :: "'a::euclidean_space set"
   1.199 +  shows "ANR S \<Longrightarrow> ANR(connected_component_set S x)"
   1.200 +  by (metis ANR_openin openin_connected_component_locally_connected ANR_imp_locally_connected)
   1.201 +
   1.202 +lemma ANR_component_ANR:
   1.203 +  fixes S :: "'a::euclidean_space set"
   1.204 +  assumes "ANR S" "c \<in> components S"
   1.205 +  shows "ANR c"
   1.206 +  by (metis ANR_connected_component_ANR assms componentsE)
   1.207 +
   1.208 +subsection\<open>Original ANR material, now for ENRs.\<close>
   1.209 +
   1.210 +lemma ENR_bounded:
   1.211 +  fixes S :: "'a::euclidean_space set"
   1.212 +  assumes "bounded S"
   1.213 +  shows "ENR S \<longleftrightarrow> (\<exists>U. open U \<and> bounded U \<and> S retract_of U)"
   1.214 +         (is "?lhs = ?rhs")
   1.215 +proof
   1.216 +  obtain r where "0 < r" and r: "S \<subseteq> ball 0 r"
   1.217 +    using bounded_subset_ballD assms by blast
   1.218 +  assume ?lhs
   1.219 +  then show ?rhs
   1.220 +    apply (clarsimp simp: ENR_def)
   1.221 +    apply (rule_tac x="ball 0 r \<inter> U" in exI, auto)
   1.222 +    using r retract_of_imp_subset retract_of_subset by fastforce
   1.223 +next
   1.224 +  assume ?rhs
   1.225 +  then show ?lhs
   1.226 +    using ENR_def by blast
   1.227 +qed
   1.228 +
   1.229 +lemma absolute_retract_imp_AR_gen:
   1.230 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   1.231 +  assumes "S retract_of T" "convex T" "T \<noteq> {}" "S homeomorphic S'" "closedin (subtopology euclidean U) S'"
   1.232 +  shows "S' retract_of U"
   1.233 +proof -
   1.234 +  have "AR T"
   1.235 +    by (simp add: assms convex_imp_AR)
   1.236 +  then have "AR S"
   1.237 +    using AR_retract_of_AR assms by auto
   1.238 +  then show ?thesis
   1.239 +    using assms AR_imp_absolute_retract by metis
   1.240 +qed
   1.241 +
   1.242 +lemma absolute_retract_imp_AR:
   1.243 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   1.244 +  assumes "S retract_of UNIV" "S homeomorphic S'" "closed S'"
   1.245 +  shows "S' retract_of UNIV"
   1.246 +  using AR_imp_absolute_retract_UNIV assms retract_of_UNIV by blast
   1.247 +
   1.248 +lemma homeomorphic_compact_arness:
   1.249 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
   1.250 +  assumes "S homeomorphic S'"
   1.251 +  shows "compact S \<and> S retract_of UNIV \<longleftrightarrow> compact S' \<and> S' retract_of UNIV"
   1.252 +  using assms homeomorphic_compactness
   1.253 +  apply auto
   1.254 +   apply (meson assms compact_AR homeomorphic_AR_iff_AR homeomorphic_compactness)+
   1.255 +  done
   1.256 +
   1.257 +lemma absolute_retract_from_Un_Int:
   1.258 +  fixes S :: "'a::euclidean_space set"
   1.259 +  assumes "(S \<union> T) retract_of UNIV" "(S \<inter> T) retract_of UNIV" "closed S" "closed T"
   1.260 +  shows "S retract_of UNIV"
   1.261 +  using AR_from_Un_Int assms retract_of_UNIV by auto
   1.262 +
   1.263 +lemma ENR_from_Un_Int_gen:
   1.264 +  fixes S :: "'a::euclidean_space set"
   1.265 +  assumes "closedin (subtopology euclidean (S \<union> T)) S" "closedin (subtopology euclidean (S \<union> T)) T" "ENR(S \<union> T)" "ENR(S \<inter> T)"
   1.266 +  shows "ENR S"
   1.267 +  apply (simp add: ENR_ANR)
   1.268 +  using ANR_from_Un_Int_local ENR_ANR assms locally_compact_closedin by blast
   1.269 +
   1.270 +
   1.271 +lemma ENR_from_Un_Int:
   1.272 +  fixes S :: "'a::euclidean_space set"
   1.273 +  assumes "closed S" "closed T" "ENR(S \<union> T)" "ENR(S \<inter> T)"
   1.274 +  shows "ENR S"
   1.275 +  by (meson ENR_from_Un_Int_gen assms closed_subset sup_ge1 sup_ge2)
   1.276 +
   1.277 +
   1.278 +lemma ENR_finite_Union_convex_closed:
   1.279 +  fixes \<T> :: "'a::euclidean_space set set"
   1.280 +  assumes \<T>: "finite \<T>" and clo: "\<And>C. C \<in> \<T> \<Longrightarrow> closed C" and con: "\<And>C. C \<in> \<T> \<Longrightarrow> convex C"
   1.281 +  shows "ENR(\<Union> \<T>)"
   1.282 +  by (simp add: ENR_ANR ANR_finite_Union_convex_closed \<T> clo closed_Union closed_imp_locally_compact con)
   1.283 +
   1.284 +lemma finite_imp_ENR:
   1.285 +  fixes S :: "'a::euclidean_space set"
   1.286 +  shows "finite S \<Longrightarrow> ENR S"
   1.287 +  by (simp add: ENR_ANR finite_imp_ANR finite_imp_closed closed_imp_locally_compact)
   1.288 +
   1.289 +lemma ENR_insert:
   1.290 +  fixes S :: "'a::euclidean_space set"
   1.291 +  assumes "closed S" "ENR S"
   1.292 +  shows "ENR(insert a S)"
   1.293 +proof -
   1.294 +  have "ENR ({a} \<union> S)"
   1.295 +    by (metis ANR_insert ENR_ANR Un_commute Un_insert_right assms closed_imp_locally_compact closed_insert sup_bot_right)
   1.296 +  then show ?thesis
   1.297 +    by auto
   1.298 +qed
   1.299 +
   1.300 +lemma ENR_path_component_ENR:
   1.301 +  fixes S :: "'a::euclidean_space set"
   1.302 +  assumes "ENR S"
   1.303 +  shows "ENR(path_component_set S x)"
   1.304 +  by (metis ANR_imp_locally_path_connected ENR_empty ENR_imp_ANR ENR_openin assms
   1.305 +            locally_path_connected_2 openin_subtopology_self path_component_eq_empty)
   1.306  
   1.307  (*UNUSED
   1.308  lemma ENR_Times:
   1.309 @@ -4103,6 +4393,61 @@
   1.310    SIMP_TAC[ENR_ANR; ANR_PCROSS; LOCALLY_COMPACT_PCROSS]);;
   1.311  *)
   1.312  
   1.313 +subsection\<open>Finally, spheres are ANRs and ENRs\<close>
   1.314 +
   1.315 +lemma absolute_retract_homeomorphic_convex_compact:
   1.316 +  fixes S :: "'a::euclidean_space set" and U :: "'b::euclidean_space set"
   1.317 +  assumes "S homeomorphic U" "S \<noteq> {}" "S \<subseteq> T" "convex U" "compact U"
   1.318 +  shows "S retract_of T"
   1.319 +  by (metis UNIV_I assms compact_AR convex_imp_AR homeomorphic_AR_iff_AR homeomorphic_compactness homeomorphic_empty(1) retract_of_subset subsetI)
   1.320 +
   1.321 +lemma frontier_retract_of_punctured_universe:
   1.322 +  fixes S :: "'a::euclidean_space set"
   1.323 +  assumes "convex S" "bounded S" "a \<in> interior S"
   1.324 +  shows "(frontier S) retract_of (- {a})"
   1.325 +  using rel_frontier_retract_of_punctured_affine_hull
   1.326 +  by (metis Compl_eq_Diff_UNIV affine_hull_nonempty_interior assms empty_iff rel_frontier_frontier rel_interior_nonempty_interior)
   1.327 +
   1.328 +lemma sphere_retract_of_punctured_universe_gen:
   1.329 +  fixes a :: "'a::euclidean_space"
   1.330 +  assumes "b \<in> ball a r"
   1.331 +  shows  "sphere a r retract_of (- {b})"
   1.332 +proof -
   1.333 +  have "frontier (cball a r) retract_of (- {b})"
   1.334 +    apply (rule frontier_retract_of_punctured_universe)
   1.335 +    using assms by auto
   1.336 +  then show ?thesis
   1.337 +    by simp
   1.338 +qed
   1.339 +
   1.340 +lemma sphere_retract_of_punctured_universe:
   1.341 +  fixes a :: "'a::euclidean_space"
   1.342 +  assumes "0 < r"
   1.343 +  shows "sphere a r retract_of (- {a})"
   1.344 +  by (simp add: assms sphere_retract_of_punctured_universe_gen)
   1.345 +
   1.346 +proposition ENR_sphere:
   1.347 +  fixes a :: "'a::euclidean_space"
   1.348 +  shows "ENR(sphere a r)"
   1.349 +proof (cases "0 < r")
   1.350 +  case True
   1.351 +  then have "sphere a r retract_of -{a}"
   1.352 +    by (simp add: sphere_retract_of_punctured_universe)
   1.353 +  with open_delete show ?thesis
   1.354 +    by (auto simp: ENR_def)
   1.355 +next
   1.356 +  case False
   1.357 +  then show ?thesis
   1.358 +    using finite_imp_ENR
   1.359 +    by (metis finite_insert infinite_imp_nonempty less_linear sphere_eq_empty sphere_trivial)
   1.360 +qed
   1.361 +
   1.362 +corollary ANR_sphere:
   1.363 +  fixes a :: "'a::euclidean_space"
   1.364 +  shows "ANR(sphere a r)"
   1.365 +  by (simp add: ENR_imp_ANR ENR_sphere)
   1.366 +
   1.367 +
   1.368  subsection\<open>Borsuk homotopy extension theorem\<close>
   1.369  
   1.370  text\<open>It's only this late so we can use the concept of retraction,
   1.371 @@ -4379,6 +4724,78 @@
   1.372    then show ?thesis by blast
   1.373  qed
   1.374  
   1.375 +lemma homotopic_Borsuk_maps_in_bounded_component:
   1.376 +  fixes a :: "'a :: euclidean_space"
   1.377 +  assumes "compact S" and "a \<notin> S"and "b \<notin> S"
   1.378 +      and boc: "bounded (connected_component_set (- S) a)"
   1.379 +      and hom: "homotopic_with (\<lambda>x. True) S (sphere 0 1)
   1.380 +                               (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
   1.381 +                               (\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
   1.382 +   shows "connected_component (- S) a b"
   1.383 +proof (rule ccontr)
   1.384 +  assume notcc: "\<not> connected_component (- S) a b"
   1.385 +  let ?T = "S \<union> connected_component_set (- S) a"
   1.386 +  have "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
   1.387 +            g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
   1.388 +            (\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a))"
   1.389 +    by (simp add: \<open>a \<notin> S\<close> componentsI non_extensible_Borsuk_map [OF \<open>compact S\<close> _ boc])
   1.390 +  moreover obtain g where "continuous_on (S \<union> connected_component_set (- S) a) g"
   1.391 +                          "g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1"
   1.392 +                          "\<And>x. x \<in> S \<Longrightarrow> g x = (x - a) /\<^sub>R norm (x - a)"
   1.393 +  proof (rule Borsuk_homotopy_extension_homotopic)
   1.394 +    show "closedin (subtopology euclidean ?T) S"
   1.395 +      by (simp add: \<open>compact S\<close> closed_subset compact_imp_closed)
   1.396 +    show "continuous_on ?T (\<lambda>x. (x - b) /\<^sub>R norm (x - b))"
   1.397 +      by (simp add: \<open>b \<notin> S\<close> notcc continuous_on_Borsuk_map)
   1.398 +    show "(\<lambda>x. (x - b) /\<^sub>R norm (x - b)) ` ?T \<subseteq> sphere 0 1"
   1.399 +      by (simp add: \<open>b \<notin> S\<close> notcc Borsuk_map_into_sphere)
   1.400 +    show "homotopic_with (\<lambda>x. True) S (sphere 0 1)
   1.401 +             (\<lambda>x. (x - b) /\<^sub>R norm (x - b)) (\<lambda>x. (x - a) /\<^sub>R norm (x - a))"
   1.402 +      by (simp add: hom homotopic_with_symD)
   1.403 +    qed (auto simp: ANR_sphere intro: that)
   1.404 +  ultimately show False by blast
   1.405 +qed
   1.406 +
   1.407 +
   1.408 +lemma Borsuk_maps_homotopic_in_connected_component_eq:
   1.409 +  fixes a :: "'a :: euclidean_space"
   1.410 +  assumes S: "compact S" "a \<notin> S" "b \<notin> S" and 2: "2 \<le> DIM('a)"
   1.411 +    shows "(homotopic_with (\<lambda>x. True) S (sphere 0 1)
   1.412 +                   (\<lambda>x. (x - a) /\<^sub>R norm (x - a))
   1.413 +                   (\<lambda>x. (x - b) /\<^sub>R norm (x - b)) \<longleftrightarrow>
   1.414 +           connected_component (- S) a b)"
   1.415 +         (is "?lhs = ?rhs")
   1.416 +proof
   1.417 +  assume L: ?lhs
   1.418 +  show ?rhs
   1.419 +  proof (cases "bounded(connected_component_set (- S) a)")
   1.420 +    case True
   1.421 +    show ?thesis
   1.422 +      by (rule homotopic_Borsuk_maps_in_bounded_component [OF S True L])
   1.423 +  next
   1.424 +    case not_bo_a: False
   1.425 +    show ?thesis
   1.426 +    proof (cases "bounded(connected_component_set (- S) b)")
   1.427 +      case True
   1.428 +      show ?thesis
   1.429 +        using homotopic_Borsuk_maps_in_bounded_component [OF S]
   1.430 +        by (simp add: L True assms connected_component_sym homotopic_Borsuk_maps_in_bounded_component homotopic_with_sym)
   1.431 +    next
   1.432 +      case False
   1.433 +      then show ?thesis
   1.434 +        using cobounded_unique_unbounded_component [of "-S" a b] \<open>compact S\<close> not_bo_a
   1.435 +        by (auto simp: compact_eq_bounded_closed assms connected_component_eq_eq)
   1.436 +    qed
   1.437 +  qed
   1.438 +next
   1.439 +  assume R: ?rhs
   1.440 +  then have "path_component (- S) a b"
   1.441 +    using assms(1) compact_eq_bounded_closed open_Compl open_path_connected_component_set by fastforce
   1.442 +  then show ?lhs
   1.443 +    by (simp add: Borsuk_maps_homotopic_in_path_component)
   1.444 +qed
   1.445 +
   1.446 +
   1.447  subsection\<open>The complement of a set and path-connectedness\<close>
   1.448  
   1.449  text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
     2.1 --- a/src/HOL/Analysis/Further_Topology.thy	Thu Jan 05 16:03:23 2017 +0000
     2.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jan 05 16:37:49 2017 +0000
     2.3 @@ -1134,11 +1134,6 @@
     2.4  
     2.5  (*Up to extend_map_affine_to_sphere_cofinite_gen*)
     2.6  
     2.7 -lemma closedin_closed_subset:
     2.8 - "\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
     2.9 -             \<Longrightarrow> closedin (subtopology euclidean T) S"
    2.10 -  by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)
    2.11 -
    2.12  lemma extend_map_affine_to_sphere1:
    2.13    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::topological_space"
    2.14    assumes "finite K" "affine U" and contf: "continuous_on (U - K) f"
     3.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 05 16:03:23 2017 +0000
     3.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Jan 05 16:37:49 2017 +0000
     3.3 @@ -1388,4 +1388,127 @@
     3.4     shows "g1 x = g2 x"
     3.5  using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv by blast
     3.6  
     3.7 +
     3.8 +lemma covering_space_locally:
     3.9 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    3.10 +  assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
    3.11 +      and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
    3.12 +    shows "locally \<psi> S"
    3.13 +proof -
    3.14 +  have "locally \<psi> (p ` C)"
    3.15 +    apply (rule locally_open_map_image [OF loc])
    3.16 +    using cov covering_space_imp_continuous apply blast
    3.17 +    using cov covering_space_imp_surjective covering_space_open_map apply blast
    3.18 +    by (simp add: pim)
    3.19 +  then show ?thesis
    3.20 +    using covering_space_imp_surjective [OF cov] by metis
    3.21 +qed
    3.22 +
    3.23 +
    3.24 +proposition covering_space_locally_eq:
    3.25 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    3.26 +  assumes cov: "covering_space C p S"
    3.27 +      and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
    3.28 +      and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
    3.29 +    shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
    3.30 +         (is "?lhs = ?rhs")
    3.31 +proof
    3.32 +  assume L: ?lhs
    3.33 +  show ?rhs
    3.34 +  proof (rule locallyI)
    3.35 +    fix V x
    3.36 +    assume V: "openin (subtopology euclidean C) V" and "x \<in> V"
    3.37 +    have "p x \<in> p ` C"
    3.38 +      by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
    3.39 +    then obtain T \<V> where "p x \<in> T"
    3.40 +                      and opeT: "openin (subtopology euclidean S) T"
    3.41 +                      and veq: "\<Union>\<V> = {x \<in> C. p x \<in> T}"
    3.42 +                      and ope: "\<forall>U\<in>\<V>. openin (subtopology euclidean C) U"
    3.43 +                      and hom: "\<forall>U\<in>\<V>. \<exists>q. homeomorphism U T p q"
    3.44 +      using cov unfolding covering_space_def by (blast intro: that)
    3.45 +    have "x \<in> \<Union>\<V>"
    3.46 +      using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce
    3.47 +    then obtain U where "x \<in> U" "U \<in> \<V>"
    3.48 +      by blast
    3.49 +    then obtain q where opeU: "openin (subtopology euclidean C) U" and q: "homeomorphism U T p q"
    3.50 +      using ope hom by blast
    3.51 +    with V have "openin (subtopology euclidean C) (U \<inter> V)"
    3.52 +      by blast
    3.53 +    then have UV: "openin (subtopology euclidean S) (p ` (U \<inter> V))"
    3.54 +      using cov covering_space_open_map by blast
    3.55 +    obtain W W' where opeW: "openin (subtopology euclidean S) W" and "\<psi> W'" "p x \<in> W" "W \<subseteq> W'" and W'sub: "W' \<subseteq> p ` (U \<inter> V)"
    3.56 +      using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast
    3.57 +    then have "W \<subseteq> T"
    3.58 +      by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans)
    3.59 +    show "\<exists>U Z. openin (subtopology euclidean C) U \<and>
    3.60 +                 \<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V"
    3.61 +    proof (intro exI conjI)
    3.62 +      have "openin (subtopology euclidean T) W"
    3.63 +        by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>)
    3.64 +      then have "openin (subtopology euclidean U) (q ` W)"
    3.65 +        by (meson homeomorphism_imp_open_map homeomorphism_symD q)
    3.66 +      then show "openin (subtopology euclidean C) (q ` W)"
    3.67 +        using opeU openin_trans by blast
    3.68 +      show "\<phi> (q ` W')"
    3.69 +        by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \<open>\<psi> W'\<close> continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim)
    3.70 +      show "x \<in> q ` W"
    3.71 +        by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q)
    3.72 +      show "q ` W \<subseteq> q ` W'"
    3.73 +        using \<open>W \<subseteq> W'\<close> by blast
    3.74 +      have "W' \<subseteq> p ` V"
    3.75 +        using W'sub by blast
    3.76 +      then show "q ` W' \<subseteq> V"
    3.77 +        using W'sub homeomorphism_apply1 [OF q] by auto
    3.78 +      qed
    3.79 +  qed
    3.80 +next
    3.81 +  assume ?rhs
    3.82 +  then show ?lhs
    3.83 +    using cov covering_space_locally pim by blast
    3.84 +qed
    3.85 +
    3.86 +lemma covering_space_locally_compact_eq:
    3.87 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    3.88 +  assumes "covering_space C p S"
    3.89 +  shows "locally compact S \<longleftrightarrow> locally compact C"
    3.90 +  apply (rule covering_space_locally_eq [OF assms])
    3.91 +   apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
    3.92 +  using compact_continuous_image by blast
    3.93 +
    3.94 +lemma covering_space_locally_connected_eq:
    3.95 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    3.96 +  assumes "covering_space C p S"
    3.97 +    shows "locally connected S \<longleftrightarrow> locally connected C"
    3.98 +  apply (rule covering_space_locally_eq [OF assms])
    3.99 +   apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
   3.100 +  using connected_continuous_image by blast
   3.101 +
   3.102 +lemma covering_space_locally_path_connected_eq:
   3.103 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   3.104 +  assumes "covering_space C p S"
   3.105 +    shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
   3.106 +  apply (rule covering_space_locally_eq [OF assms])
   3.107 +   apply (meson path_connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
   3.108 +  using path_connected_continuous_image by blast
   3.109 +
   3.110 +
   3.111 +lemma covering_space_locally_compact:
   3.112 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   3.113 +  assumes "locally compact C" "covering_space C p S"
   3.114 +  shows "locally compact S"
   3.115 +  using assms covering_space_locally_compact_eq by blast
   3.116 +
   3.117 +
   3.118 +lemma covering_space_locally_connected:
   3.119 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   3.120 +  assumes "locally connected C" "covering_space C p S"
   3.121 +  shows "locally connected S"
   3.122 +  using assms covering_space_locally_connected_eq by blast
   3.123 +
   3.124 +lemma covering_space_locally_path_connected:
   3.125 +  fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   3.126 +  assumes "locally path_connected C" "covering_space C p S"
   3.127 +  shows "locally path_connected S"
   3.128 +  using assms covering_space_locally_path_connected_eq by blast
   3.129 +
   3.130  end
     4.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jan 05 16:03:23 2017 +0000
     4.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jan 05 16:37:49 2017 +0000
     4.3 @@ -876,6 +876,11 @@
     4.4  lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
     4.5    by (auto simp add: closedin_closed)
     4.6  
     4.7 +lemma closedin_closed_subset:
     4.8 + "\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
     4.9 +             \<Longrightarrow> closedin (subtopology euclidean T) S"
    4.10 +  by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)
    4.11 +
    4.12  lemma finite_imp_closedin:
    4.13    fixes S :: "'a::t1_space set"
    4.14    shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S"