author nipkow Thu Jul 12 11:23:46 2018 +0200 (13 months ago) changeset 68617 75129a73aca3 parent 68616 cedf3480fdad child 68619 79abf4201e8d
more economic tagging
 src/HOL/Analysis/Brouwer_Fixpoint.thy file | annotate | diff | revisions src/HOL/Analysis/Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Inner_Product.thy file | annotate | diff | revisions src/HOL/Analysis/Measure_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Product_Vector.thy file | annotate | diff | revisions src/HOL/Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Jul 11 23:24:25 2018 +0100
1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Jul 12 11:23:46 2018 +0200
1.3 @@ -12,12 +12,1748 @@
1.4  (*                                                                           *)
1.5  (*              (c) Copyright, John Harrison 1998-2008                       *)
1.6
1.7 -section \<open>Results connected with topological dimension\<close>
1.8 +section \<open>Brouwer's Fixed Point Theorem\<close>
1.9
1.10  theory Brouwer_Fixpoint
1.11  imports Path_Connected Homeomorphism
1.12  begin
1.13
1.14 +subsection \<open>Unit cubes\<close>
1.15 +
1.16 +(* FIXME mv euclidean topological space *)
1.17 +definition unit_cube :: "'a::euclidean_space set"
1.18 +  where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
1.19 +
1.20 +lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
1.21 +  unfolding unit_cube_def by simp
1.22 +
1.23 +lemma bounded_unit_cube: "bounded unit_cube"
1.24 +  unfolding bounded_def
1.25 +proof (intro exI ballI)
1.26 +  fix y :: 'a assume y: "y \<in> unit_cube"
1.27 +  have "dist 0 y = norm y" by (rule dist_0_norm)
1.28 +  also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
1.29 +  also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_sum)
1.30 +  also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
1.31 +    by (rule sum_mono, simp add: y [unfolded mem_unit_cube])
1.32 +  finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
1.33 +qed
1.34 +
1.35 +lemma closed_unit_cube: "closed unit_cube"
1.36 +  unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
1.37 +  by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
1.38 +
1.39 +lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
1.40 +  unfolding compact_eq_seq_compact_metric
1.41 +  using bounded_unit_cube closed_unit_cube
1.42 +  by (rule bounded_closed_imp_seq_compact)
1.43 +
1.44 +lemma convex_unit_cube: "convex unit_cube"
1.45 +  by (rule is_interval_convex) (fastforce simp add: is_interval_def mem_unit_cube)
1.46 +
1.47 +
1.48 +(* FIXME mv topology euclidean space *)
1.49 +subsection \<open>Retractions\<close>
1.50 +
1.51 +definition "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
1.52 +
1.53 +definition retract_of (infixl "retract'_of" 50)
1.54 +  where "(T retract_of S) \<longleftrightarrow> (\<exists>r. retraction S T r)"
1.55 +
1.56 +lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
1.57 +  unfolding retraction_def by auto
1.58 +
1.59 +text \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
1.60 +
1.61 +lemma invertible_fixpoint_property:
1.62 +  fixes S :: "'a::euclidean_space set"
1.63 +    and T :: "'b::euclidean_space set"
1.64 +  assumes contt: "continuous_on T i"
1.65 +    and "i ` T \<subseteq> S"
1.66 +    and contr: "continuous_on S r"
1.67 +    and "r ` S \<subseteq> T"
1.68 +    and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
1.69 +    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
1.70 +    and contg: "continuous_on T g"
1.71 +    and "g ` T \<subseteq> T"
1.72 +  obtains y where "y \<in> T" and "g y = y"
1.73 +proof -
1.74 +  have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
1.75 +  proof (rule FP)
1.76 +    show "continuous_on S (i \<circ> g \<circ> r)"
1.77 +      by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
1.78 +    show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
1.79 +      using assms(2,4,8) by force
1.80 +  qed
1.81 +  then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
1.82 +  then have *: "g (r x) \<in> T"
1.83 +    using assms(4,8) by auto
1.84 +  have "r ((i \<circ> g \<circ> r) x) = r x"
1.85 +    using x by auto
1.86 +  then show ?thesis
1.87 +    using "*" ri that by auto
1.88 +qed
1.89 +
1.90 +lemma homeomorphic_fixpoint_property:
1.91 +  fixes S :: "'a::euclidean_space set"
1.92 +    and T :: "'b::euclidean_space set"
1.93 +  assumes "S homeomorphic T"
1.94 +  shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
1.95 +         (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
1.96 +         (is "?lhs = ?rhs")
1.97 +proof -
1.98 +  obtain r i where r:
1.99 +      "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
1.100 +      "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
1.101 +    using assms unfolding homeomorphic_def homeomorphism_def  by blast
1.102 +  show ?thesis
1.103 +  proof
1.104 +    assume ?lhs
1.105 +    with r show ?rhs
1.106 +      by (metis invertible_fixpoint_property[of T i S r] order_refl)
1.107 +  next
1.108 +    assume ?rhs
1.109 +    with r show ?lhs
1.110 +      by (metis invertible_fixpoint_property[of S r T i] order_refl)
1.111 +  qed
1.112 +qed
1.113 +
1.114 +lemma retract_fixpoint_property:
1.115 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.116 +    and S :: "'a set"
1.117 +  assumes "T retract_of S"
1.118 +    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
1.119 +    and contg: "continuous_on T g"
1.120 +    and "g ` T \<subseteq> T"
1.121 +  obtains y where "y \<in> T" and "g y = y"
1.122 +proof -
1.123 +  obtain h where "retraction S T h"
1.124 +    using assms(1) unfolding retract_of_def ..
1.125 +  then show ?thesis
1.126 +    unfolding retraction_def
1.127 +    using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
1.128 +    by (metis assms(4) contg image_ident that)
1.129 +qed
1.130 +
1.131 +lemma retraction:
1.132 +   "retraction S T r \<longleftrightarrow>
1.133 +    T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
1.134 +by (force simp: retraction_def)
1.135 +
1.136 +lemma retract_of_imp_extensible:
1.137 +  assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
1.138 +  obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.139 +using assms
1.140 +apply (clarsimp simp add: retract_of_def retraction)
1.141 +apply (rule_tac g = "f \<circ> r" in that)
1.142 +apply (auto simp: continuous_on_compose2)
1.143 +done
1.144 +
1.145 +lemma idempotent_imp_retraction:
1.146 +  assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
1.147 +    shows "retraction S (f ` S) f"
1.148 +by (simp add: assms retraction)
1.149 +
1.150 +lemma retraction_subset:
1.151 +  assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
1.152 +  shows "retraction s' T r"
1.153 +  unfolding retraction_def
1.154 +  by (metis assms continuous_on_subset image_mono retraction)
1.155 +
1.156 +lemma retract_of_subset:
1.157 +  assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
1.158 +    shows "T retract_of s'"
1.159 +by (meson assms retract_of_def retraction_subset)
1.160 +
1.161 +lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
1.162 +by (simp add: continuous_on_id retraction)
1.163 +
1.164 +lemma retract_of_refl [iff]: "S retract_of S"
1.165 +  unfolding retract_of_def retraction_def
1.166 +  using continuous_on_id by blast
1.167 +
1.168 +lemma retract_of_imp_subset:
1.169 +   "S retract_of T \<Longrightarrow> S \<subseteq> T"
1.170 +by (simp add: retract_of_def retraction_def)
1.171 +
1.172 +lemma retract_of_empty [simp]:
1.173 +     "({} retract_of S) \<longleftrightarrow> S = {}"  "(S retract_of {}) \<longleftrightarrow> S = {}"
1.174 +by (auto simp: retract_of_def retraction_def)
1.175 +
1.176 +lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
1.177 +  unfolding retract_of_def retraction_def by force
1.178 +
1.179 +lemma retraction_comp:
1.180 +   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
1.181 +        \<Longrightarrow> retraction S U (g \<circ> f)"
1.182 +apply (auto simp: retraction_def intro: continuous_on_compose2)
1.183 +by blast
1.184 +
1.185 +lemma retract_of_trans [trans]:
1.186 +  assumes "S retract_of T" and "T retract_of U"
1.187 +    shows "S retract_of U"
1.188 +using assms by (auto simp: retract_of_def intro: retraction_comp)
1.189 +
1.190 +lemma closedin_retract:
1.191 +  fixes S :: "'a :: real_normed_vector set"
1.192 +  assumes "S retract_of T"
1.193 +    shows "closedin (subtopology euclidean T) S"
1.194 +proof -
1.195 +  obtain r where "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
1.196 +    using assms by (auto simp: retract_of_def retraction_def)
1.197 +  then have S: "S = {x \<in> T. (norm(r x - x)) = 0}" by auto
1.198 +  show ?thesis
1.199 +    apply (subst S)
1.200 +    apply (rule continuous_closedin_preimage_constant)
1.201 +    by (simp add: \<open>continuous_on T r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
1.202 +qed
1.203 +
1.204 +lemma closedin_self [simp]:
1.205 +    fixes S :: "'a :: real_normed_vector set"
1.206 +    shows "closedin (subtopology euclidean S) S"
1.207 +  by (simp add: closedin_retract)
1.208 +
1.209 +lemma retract_of_contractible:
1.210 +  assumes "contractible T" "S retract_of T"
1.211 +    shows "contractible S"
1.212 +using assms
1.213 +apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
1.214 +apply (rule_tac x="r a" in exI)
1.215 +apply (rule_tac x="r \<circ> h" in exI)
1.216 +apply (intro conjI continuous_intros continuous_on_compose)
1.217 +apply (erule continuous_on_subset | force)+
1.218 +done
1.219 +
1.220 +lemma retract_of_compact:
1.221 +     "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
1.222 +  by (metis compact_continuous_image retract_of_def retraction)
1.223 +
1.224 +lemma retract_of_closed:
1.225 +    fixes S :: "'a :: real_normed_vector set"
1.226 +    shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
1.227 +  by (metis closedin_retract closedin_closed_eq)
1.228 +
1.229 +lemma retract_of_connected:
1.230 +    "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
1.231 +  by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
1.232 +
1.233 +lemma retract_of_path_connected:
1.234 +    "\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
1.235 +  by (metis path_connected_continuous_image retract_of_def retraction)
1.236 +
1.237 +lemma retract_of_simply_connected:
1.238 +    "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
1.239 +apply (simp add: retract_of_def retraction_def, clarify)
1.240 +apply (rule simply_connected_retraction_gen)
1.241 +apply (force simp: continuous_on_id elim!: continuous_on_subset)+
1.242 +done
1.243 +
1.244 +lemma retract_of_homotopically_trivial:
1.245 +  assumes ts: "T retract_of S"
1.246 +      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
1.247 +                       continuous_on U g; g ` U \<subseteq> S\<rbrakk>
1.248 +                       \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
1.249 +      and "continuous_on U f" "f ` U \<subseteq> T"
1.250 +      and "continuous_on U g" "g ` U \<subseteq> T"
1.251 +    shows "homotopic_with (\<lambda>x. True) U T f g"
1.252 +proof -
1.253 +  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
1.254 +    using ts by (auto simp: retract_of_def retraction)
1.255 +  then obtain k where "Retracts S r T k"
1.256 +    unfolding Retracts_def
1.257 +    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
1.258 +  then show ?thesis
1.259 +    apply (rule Retracts.homotopically_trivial_retraction_gen)
1.260 +    using assms
1.261 +    apply (force simp: hom)+
1.262 +    done
1.263 +qed
1.264 +
1.265 +lemma retract_of_homotopically_trivial_null:
1.266 +  assumes ts: "T retract_of S"
1.267 +      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
1.268 +                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
1.269 +      and "continuous_on U f" "f ` U \<subseteq> T"
1.270 +  obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
1.271 +proof -
1.272 +  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
1.273 +    using ts by (auto simp: retract_of_def retraction)
1.274 +  then obtain k where "Retracts S r T k"
1.275 +    unfolding Retracts_def
1.276 +    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
1.277 +  then show ?thesis
1.278 +    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
1.279 +    apply (rule TrueI refl assms that | assumption)+
1.280 +    done
1.281 +qed
1.282 +
1.283 +lemma retraction_imp_quotient_map:
1.284 +   "retraction S T r
1.285 +    \<Longrightarrow> U \<subseteq> T
1.286 +            \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow>
1.287 +                 openin (subtopology euclidean T) U)"
1.288 +apply (clarsimp simp add: retraction)
1.289 +apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
1.290 +apply (auto simp: elim: continuous_on_subset)
1.291 +done
1.292 +
1.293 +lemma retract_of_locally_compact:
1.294 +    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
1.295 +    shows  "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T"
1.296 +  by (metis locally_compact_closedin closedin_retract)
1.297 +
1.298 +lemma retract_of_Times:
1.299 +   "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
1.300 +apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
1.301 +apply (rename_tac f g)
1.302 +apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
1.303 +apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
1.304 +done
1.305 +
1.306 +lemma homotopic_into_retract:
1.307 +   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
1.308 +        \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
1.309 +apply (subst (asm) homotopic_with_def)
1.310 +apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
1.311 +apply (rule_tac x="r \<circ> h" in exI)
1.312 +apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
1.313 +done
1.314 +
1.315 +lemma retract_of_locally_connected:
1.316 +  assumes "locally connected T" "S retract_of T"
1.317 +    shows "locally connected S"
1.318 +  using assms
1.319 +  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image)
1.320 +
1.321 +lemma retract_of_locally_path_connected:
1.322 +  assumes "locally path_connected T" "S retract_of T"
1.323 +    shows "locally path_connected S"
1.324 +  using assms
1.325 +  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
1.326 +
1.327 +text \<open>A few simple lemmas about deformation retracts\<close>
1.328 +
1.329 +lemma deformation_retract_imp_homotopy_eqv:
1.330 +  fixes S :: "'a::euclidean_space set"
1.331 +  assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
1.332 +  shows "S homotopy_eqv T"
1.333 +proof -
1.334 +  have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
1.335 +    by (simp add: assms(1) homotopic_with_symD)
1.336 +  moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
1.337 +    using r unfolding retraction_def
1.338 +    by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
1.339 +  ultimately
1.340 +  show ?thesis
1.341 +    unfolding homotopy_eqv_def
1.342 +    by (metis continuous_on_id' id_def image_id r retraction_def)
1.343 +qed
1.344 +
1.345 +lemma deformation_retract:
1.346 +  fixes S :: "'a::euclidean_space set"
1.347 +    shows "(\<exists>r. homotopic_with (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
1.348 +           T retract_of S \<and> (\<exists>f. homotopic_with (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
1.349 +    (is "?lhs = ?rhs")
1.350 +proof
1.351 +  assume ?lhs
1.352 +  then show ?rhs
1.353 +    by (auto simp: retract_of_def retraction_def)
1.354 +next
1.355 +  assume ?rhs
1.356 +  then show ?lhs
1.357 +    apply (clarsimp simp add: retract_of_def retraction_def)
1.358 +    apply (rule_tac x=r in exI, simp)
1.359 +     apply (rule homotopic_with_trans, assumption)
1.360 +     apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
1.361 +        apply (rule_tac Y=S in homotopic_compose_continuous_left)
1.362 +         apply (auto simp: homotopic_with_sym)
1.363 +    done
1.364 +qed
1.365 +
1.366 +lemma deformation_retract_of_contractible_sing:
1.367 +  fixes S :: "'a::euclidean_space set"
1.368 +  assumes "contractible S" "a \<in> S"
1.369 +  obtains r where "homotopic_with (\<lambda>x. True) S S id r" "retraction S {a} r"
1.370 +proof -
1.371 +  have "{a} retract_of S"
1.372 +    by (simp add: \<open>a \<in> S\<close>)
1.373 +  moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
1.374 +      using assms
1.375 +      by (auto simp: contractible_def continuous_on_const continuous_on_id homotopic_into_contractible image_subset_iff)
1.376 +  moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
1.377 +    by (simp add: image_subsetI)
1.378 +  ultimately show ?thesis
1.379 +    using that deformation_retract  by metis
1.380 +qed
1.381 +
1.382 +
1.383 +lemma continuous_on_compact_surface_projection_aux:
1.384 +  fixes S :: "'a::t2_space set"
1.385 +  assumes "compact S" "S \<subseteq> T" "image q T \<subseteq> S"
1.386 +      and contp: "continuous_on T p"
1.387 +      and "\<And>x. x \<in> S \<Longrightarrow> q x = x"
1.388 +      and [simp]: "\<And>x. x \<in> T \<Longrightarrow> q(p x) = q x"
1.389 +      and "\<And>x. x \<in> T \<Longrightarrow> p(q x) = p x"
1.390 +    shows "continuous_on T q"
1.391 +proof -
1.392 +  have *: "image p T = image p S"
1.393 +    using assms by auto (metis imageI subset_iff)
1.394 +  have contp': "continuous_on S p"
1.395 +    by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
1.396 +  have "continuous_on (p ` T) q"
1.397 +    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
1.398 +  then have "continuous_on T (q \<circ> p)"
1.399 +    by (rule continuous_on_compose [OF contp])
1.400 +  then show ?thesis
1.401 +    by (rule continuous_on_eq [of _ "q \<circ> p"]) (simp add: o_def)
1.402 +qed
1.403 +
1.404 +lemma continuous_on_compact_surface_projection:
1.405 +  fixes S :: "'a::real_normed_vector set"
1.406 +  assumes "compact S"
1.407 +      and S: "S \<subseteq> V - {0}" and "cone V"
1.408 +      and iff: "\<And>x k. x \<in> V - {0} \<Longrightarrow> 0 < k \<and> (k *\<^sub>R x) \<in> S \<longleftrightarrow> d x = k"
1.409 +  shows "continuous_on (V - {0}) (\<lambda>x. d x *\<^sub>R x)"
1.410 +proof (rule continuous_on_compact_surface_projection_aux [OF \<open>compact S\<close> S])
1.411 +  show "(\<lambda>x. d x *\<^sub>R x) ` (V - {0}) \<subseteq> S"
1.412 +    using iff by auto
1.413 +  show "continuous_on (V - {0}) (\<lambda>x. inverse(norm x) *\<^sub>R x)"
1.414 +    by (intro continuous_intros) force
1.415 +  show "\<And>x. x \<in> S \<Longrightarrow> d x *\<^sub>R x = x"
1.416 +    by (metis S zero_less_one local.iff scaleR_one subset_eq)
1.417 +  show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \<in> V - {0}" for x
1.418 +    using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \<open>cone V\<close>
1.419 +    by (simp add: field_simps cone_def zero_less_mult_iff)
1.420 +  show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \<in> V - {0}" for x
1.421 +  proof -
1.422 +    have "0 < d x"
1.423 +      using local.iff that by blast
1.424 +    then show ?thesis
1.425 +      by simp
1.426 +  qed
1.427 +qed
1.428 +
1.429 +subsection \<open>Absolute retracts, absolute neighbourhood retracts (ANR) and Euclidean neighbourhood retracts (ENR)\<close>
1.430 +
1.431 +text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
1.432 +retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
1.433 +in spaces of higher dimension.
1.434 +
1.435 +John Harrison writes: "This turns out to be sufficient (since any set in \$\mathbb{R}^n\$ can be
1.436 +embedded as a closed subset of a convex subset of \$\mathbb{R}^{n+1}\$) to derive the usual
1.437 +definitions, but we need to split them into two implications because of the lack of type
1.438 +quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."\<close>
1.439 +
1.440 +definition AR :: "'a::topological_space set => bool"
1.441 +  where
1.442 +   "AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
1.443 +                \<longrightarrow> S' retract_of U"
1.444 +
1.445 +definition ANR :: "'a::topological_space set => bool"
1.446 +  where
1.447 +   "ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
1.448 +                \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and>
1.449 +                        S' retract_of T)"
1.450 +
1.451 +definition ENR :: "'a::topological_space set => bool"
1.452 +  where "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
1.453 +
1.454 +text \<open>First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
1.455 +
1.456 +lemma AR_imp_absolute_extensor:
1.457 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.458 +  assumes "AR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
1.459 +      and cloUT: "closedin (subtopology euclidean U) T"
1.460 +  obtains g where "continuous_on U g" "g ` U \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
1.461 +proof -
1.462 +  have "aff_dim S < int (DIM('b \<times> real))"
1.463 +    using aff_dim_le_DIM [of S] by simp
1.464 +  then obtain C and S' :: "('b * real) set"
1.465 +          where C: "convex C" "C \<noteq> {}"
1.466 +            and cloCS: "closedin (subtopology euclidean C) S'"
1.467 +            and hom: "S homeomorphic S'"
1.468 +    by (metis that homeomorphic_closedin_convex)
1.469 +  then have "S' retract_of C"
1.470 +    using \<open>AR S\<close> by (simp add: AR_def)
1.471 +  then obtain r where "S' \<subseteq> C" and contr: "continuous_on C r"
1.472 +                  and "r ` C \<subseteq> S'" and rid: "\<And>x. x\<in>S' \<Longrightarrow> r x = x"
1.473 +    by (auto simp: retraction_def retract_of_def)
1.474 +  obtain g h where "homeomorphism S S' g h"
1.475 +    using hom by (force simp: homeomorphic_def)
1.476 +  then have "continuous_on (f ` T) g"
1.477 +    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
1.478 +  then have contgf: "continuous_on T (g \<circ> f)"
1.479 +    by (metis continuous_on_compose contf)
1.480 +  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
1.481 +  proof -
1.482 +    have "g ` S = S'"
1.483 +      by (metis (no_types) \<open>homeomorphism S S' g h\<close> homeomorphism_def)
1.484 +    with \<open>S' \<subseteq> C\<close> \<open>f ` T \<subseteq> S\<close> show ?thesis by force
1.485 +  qed
1.486 +  obtain f' where f': "continuous_on U f'"  "f' ` U \<subseteq> C"
1.487 +                      "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
1.488 +    by (metis Dugundji [OF C cloUT contgf gfTC])
1.489 +  show ?thesis
1.490 +  proof (rule_tac g = "h \<circ> r \<circ> f'" in that)
1.491 +    show "continuous_on U (h \<circ> r \<circ> f')"
1.492 +      apply (intro continuous_on_compose f')
1.493 +       using continuous_on_subset contr f' apply blast
1.494 +      by (meson \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> continuous_on_subset \<open>f' ` U \<subseteq> C\<close> homeomorphism_def image_mono)
1.495 +    show "(h \<circ> r \<circ> f') ` U \<subseteq> S"
1.496 +      using \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> \<open>f' ` U \<subseteq> C\<close>
1.497 +      by (fastforce simp: homeomorphism_def)
1.498 +    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
1.499 +      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> f'
1.500 +      by (auto simp: rid homeomorphism_def)
1.501 +  qed
1.502 +qed
1.503 +
1.504 +lemma AR_imp_absolute_retract:
1.505 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.506 +  assumes "AR S" "S homeomorphic S'"
1.507 +      and clo: "closedin (subtopology euclidean U) S'"
1.508 +    shows "S' retract_of U"
1.509 +proof -
1.510 +  obtain g h where hom: "homeomorphism S S' g h"
1.511 +    using assms by (force simp: homeomorphic_def)
1.512 +  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
1.513 +    using hom homeomorphism_def apply blast
1.514 +    apply (metis hom equalityE homeomorphism_def)
1.515 +    done
1.516 +  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
1.517 +              and h'h: "\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
1.518 +    by (blast intro: AR_imp_absolute_extensor [OF \<open>AR S\<close> h clo])
1.519 +  have [simp]: "S' \<subseteq> U" using clo closedin_limpt by blast
1.520 +  show ?thesis
1.521 +  proof (simp add: retraction_def retract_of_def, intro exI conjI)
1.522 +    show "continuous_on U (g \<circ> h')"
1.523 +      apply (intro continuous_on_compose h')
1.524 +      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.525 +      done
1.526 +    show "(g \<circ> h') ` U \<subseteq> S'"
1.527 +      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.528 +    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
1.529 +      by clarsimp (metis h'h hom homeomorphism_def)
1.530 +  qed
1.531 +qed
1.532 +
1.533 +lemma AR_imp_absolute_retract_UNIV:
1.534 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.535 +  assumes "AR S" and hom: "S homeomorphic S'"
1.536 +      and clo: "closed S'"
1.537 +    shows "S' retract_of UNIV"
1.538 +apply (rule AR_imp_absolute_retract [OF \<open>AR S\<close> hom])
1.539 +using clo closed_closedin by auto
1.540 +
1.541 +lemma absolute_extensor_imp_AR:
1.542 +  fixes S :: "'a::euclidean_space set"
1.543 +  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
1.544 +           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
1.545 +                  closedin (subtopology euclidean U) T\<rbrakk>
1.546 +                 \<Longrightarrow> \<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
1.547 +  shows "AR S"
1.548 +proof (clarsimp simp: AR_def)
1.549 +  fix U and T :: "('a * real) set"
1.550 +  assume "S homeomorphic T" and clo: "closedin (subtopology euclidean U) T"
1.551 +  then obtain g h where hom: "homeomorphism S T g h"
1.552 +    by (force simp: homeomorphic_def)
1.553 +  have h: "continuous_on T h" " h ` T \<subseteq> S"
1.554 +    using hom homeomorphism_def apply blast
1.555 +    apply (metis hom equalityE homeomorphism_def)
1.556 +    done
1.557 +  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
1.558 +              and h'h: "\<forall>x\<in>T. h' x = h x"
1.559 +    using assms [OF h clo] by blast
1.560 +  have [simp]: "T \<subseteq> U"
1.561 +    using clo closedin_imp_subset by auto
1.562 +  show "T retract_of U"
1.563 +  proof (simp add: retraction_def retract_of_def, intro exI conjI)
1.564 +    show "continuous_on U (g \<circ> h')"
1.565 +      apply (intro continuous_on_compose h')
1.566 +      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.567 +      done
1.568 +    show "(g \<circ> h') ` U \<subseteq> T"
1.569 +      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.570 +    show "\<forall>x\<in>T. (g \<circ> h') x = x"
1.571 +      by clarsimp (metis h'h hom homeomorphism_def)
1.572 +  qed
1.573 +qed
1.574 +
1.575 +lemma AR_eq_absolute_extensor:
1.576 +  fixes S :: "'a::euclidean_space set"
1.577 +  shows "AR S \<longleftrightarrow>
1.578 +       (\<forall>f :: 'a * real \<Rightarrow> 'a.
1.579 +        \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
1.580 +               closedin (subtopology euclidean U) T \<longrightarrow>
1.581 +                (\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
1.582 +apply (rule iffI)
1.583 + apply (metis AR_imp_absolute_extensor)
1.585 +done
1.586 +
1.587 +lemma AR_imp_retract:
1.588 +  fixes S :: "'a::euclidean_space set"
1.589 +  assumes "AR S \<and> closedin (subtopology euclidean U) S"
1.590 +    shows "S retract_of U"
1.591 +using AR_imp_absolute_retract assms homeomorphic_refl by blast
1.592 +
1.593 +lemma AR_homeomorphic_AR:
1.594 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.595 +  assumes "AR T" "S homeomorphic T"
1.596 +    shows "AR S"
1.597 +unfolding AR_def
1.598 +by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym)
1.599 +
1.600 +lemma homeomorphic_AR_iff_AR:
1.601 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.602 +  shows "S homeomorphic T \<Longrightarrow> AR S \<longleftrightarrow> AR T"
1.603 +by (metis AR_homeomorphic_AR homeomorphic_sym)
1.604 +
1.605 +
1.606 +lemma ANR_imp_absolute_neighbourhood_extensor:
1.607 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.608 +  assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
1.609 +      and cloUT: "closedin (subtopology euclidean U) T"
1.610 +  obtains V g where "T \<subseteq> V" "openin (subtopology euclidean U) V"
1.611 +                    "continuous_on V g"
1.612 +                    "g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
1.613 +proof -
1.614 +  have "aff_dim S < int (DIM('b \<times> real))"
1.615 +    using aff_dim_le_DIM [of S] by simp
1.616 +  then obtain C and S' :: "('b * real) set"
1.617 +          where C: "convex C" "C \<noteq> {}"
1.618 +            and cloCS: "closedin (subtopology euclidean C) S'"
1.619 +            and hom: "S homeomorphic S'"
1.620 +    by (metis that homeomorphic_closedin_convex)
1.621 +  then obtain D where opD: "openin (subtopology euclidean C) D" and "S' retract_of D"
1.622 +    using \<open>ANR S\<close> by (auto simp: ANR_def)
1.623 +  then obtain r where "S' \<subseteq> D" and contr: "continuous_on D r"
1.624 +                  and "r ` D \<subseteq> S'" and rid: "\<And>x. x \<in> S' \<Longrightarrow> r x = x"
1.625 +    by (auto simp: retraction_def retract_of_def)
1.626 +  obtain g h where homgh: "homeomorphism S S' g h"
1.627 +    using hom by (force simp: homeomorphic_def)
1.628 +  have "continuous_on (f ` T) g"
1.629 +    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
1.630 +  then have contgf: "continuous_on T (g \<circ> f)"
1.631 +    by (intro continuous_on_compose contf)
1.632 +  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
1.633 +  proof -
1.634 +    have "g ` S = S'"
1.635 +      by (metis (no_types) homeomorphism_def homgh)
1.636 +    then show ?thesis
1.637 +      by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology)
1.638 +  qed
1.639 +  obtain f' where contf': "continuous_on U f'"
1.640 +              and "f' ` U \<subseteq> C"
1.641 +              and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
1.642 +    by (metis Dugundji [OF C cloUT contgf gfTC])
1.643 +  show ?thesis
1.644 +  proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
1.645 +    show "T \<subseteq> U \<inter> f' -` D"
1.646 +      using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
1.647 +      by fastforce
1.648 +    show ope: "openin (subtopology euclidean U) (U \<inter> f' -` D)"
1.649 +      using  \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
1.650 +    have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
1.651 +      apply (rule continuous_on_subset [of S'])
1.652 +      using homeomorphism_def homgh apply blast
1.653 +      using \<open>r ` D \<subseteq> S'\<close> by blast
1.654 +    show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
1.655 +      apply (intro continuous_on_compose conth
1.656 +                   continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
1.657 +      done
1.658 +    show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
1.659 +      using \<open>homeomorphism S S' g h\<close>  \<open>f' ` U \<subseteq> C\<close>  \<open>r ` D \<subseteq> S'\<close>
1.660 +      by (auto simp: homeomorphism_def)
1.661 +    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
1.662 +      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> eq
1.663 +      by (auto simp: rid homeomorphism_def)
1.664 +  qed
1.665 +qed
1.666 +
1.667 +
1.668 +corollary ANR_imp_absolute_neighbourhood_retract:
1.669 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.670 +  assumes "ANR S" "S homeomorphic S'"
1.671 +      and clo: "closedin (subtopology euclidean U) S'"
1.672 +  obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
1.673 +proof -
1.674 +  obtain g h where hom: "homeomorphism S S' g h"
1.675 +    using assms by (force simp: homeomorphic_def)
1.676 +  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
1.677 +    using hom homeomorphism_def apply blast
1.678 +    apply (metis hom equalityE homeomorphism_def)
1.679 +    done
1.680 +    from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
1.681 +  obtain V h' where "S' \<subseteq> V" and opUV: "openin (subtopology euclidean U) V"
1.682 +                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
1.683 +                and h'h:"\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
1.684 +    by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
1.685 +  have "S' retract_of V"
1.686 +  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
1.687 +    show "continuous_on V (g \<circ> h')"
1.688 +      apply (intro continuous_on_compose h')
1.689 +      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.690 +      done
1.691 +    show "(g \<circ> h') ` V \<subseteq> S'"
1.692 +      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.693 +    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
1.694 +      by clarsimp (metis h'h hom homeomorphism_def)
1.695 +  qed
1.696 +  then show ?thesis
1.697 +    by (rule that [OF opUV])
1.698 +qed
1.699 +
1.700 +corollary ANR_imp_absolute_neighbourhood_retract_UNIV:
1.701 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.702 +  assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'"
1.703 +  obtains V where "open V" "S' retract_of V"
1.704 +  using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
1.705 +by (metis clo closed_closedin open_openin subtopology_UNIV)
1.706 +
1.707 +corollary neighbourhood_extension_into_ANR:
1.708 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.709 +  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
1.710 +  obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
1.711 +                    "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.712 +  using ANR_imp_absolute_neighbourhood_extensor [OF  \<open>ANR T\<close> contf fim]
1.713 +  by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
1.714 +
1.715 +lemma absolute_neighbourhood_extensor_imp_ANR:
1.716 +  fixes S :: "'a::euclidean_space set"
1.717 +  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
1.718 +           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
1.719 +                  closedin (subtopology euclidean U) T\<rbrakk>
1.720 +                 \<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
1.721 +                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
1.722 +  shows "ANR S"
1.723 +proof (clarsimp simp: ANR_def)
1.724 +  fix U and T :: "('a * real) set"
1.725 +  assume "S homeomorphic T" and clo: "closedin (subtopology euclidean U) T"
1.726 +  then obtain g h where hom: "homeomorphism S T g h"
1.727 +    by (force simp: homeomorphic_def)
1.728 +  have h: "continuous_on T h" " h ` T \<subseteq> S"
1.729 +    using hom homeomorphism_def apply blast
1.730 +    apply (metis hom equalityE homeomorphism_def)
1.731 +    done
1.732 +  obtain V h' where "T \<subseteq> V" and opV: "openin (subtopology euclidean U) V"
1.733 +                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
1.734 +              and h'h: "\<forall>x\<in>T. h' x = h x"
1.735 +    using assms [OF h clo] by blast
1.736 +  have [simp]: "T \<subseteq> U"
1.737 +    using clo closedin_imp_subset by auto
1.738 +  have "T retract_of V"
1.739 +  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
1.740 +    show "continuous_on V (g \<circ> h')"
1.741 +      apply (intro continuous_on_compose h')
1.742 +      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.743 +      done
1.744 +    show "(g \<circ> h') ` V \<subseteq> T"
1.745 +      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.746 +    show "\<forall>x\<in>T. (g \<circ> h') x = x"
1.747 +      by clarsimp (metis h'h hom homeomorphism_def)
1.748 +  qed
1.749 +  then show "\<exists>V. openin (subtopology euclidean U) V \<and> T retract_of V"
1.750 +    using opV by blast
1.751 +qed
1.752 +
1.753 +lemma ANR_eq_absolute_neighbourhood_extensor:
1.754 +  fixes S :: "'a::euclidean_space set"
1.755 +  shows "ANR S \<longleftrightarrow>
1.756 +         (\<forall>f :: 'a * real \<Rightarrow> 'a.
1.757 +          \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
1.758 +                closedin (subtopology euclidean U) T \<longrightarrow>
1.759 +               (\<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
1.760 +                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
1.761 +apply (rule iffI)
1.762 + apply (metis ANR_imp_absolute_neighbourhood_extensor)
1.764 +done
1.765 +
1.766 +lemma ANR_imp_neighbourhood_retract:
1.767 +  fixes S :: "'a::euclidean_space set"
1.768 +  assumes "ANR S" "closedin (subtopology euclidean U) S"
1.769 +  obtains V where "openin (subtopology euclidean U) V" "S retract_of V"
1.770 +using ANR_imp_absolute_neighbourhood_retract assms homeomorphic_refl by blast
1.771 +
1.772 +lemma ANR_imp_absolute_closed_neighbourhood_retract:
1.773 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.774 +  assumes "ANR S" "S homeomorphic S'" and US': "closedin (subtopology euclidean U) S'"
1.775 +  obtains V W
1.776 +    where "openin (subtopology euclidean U) V"
1.777 +          "closedin (subtopology euclidean U) W"
1.778 +          "S' \<subseteq> V" "V \<subseteq> W" "S' retract_of W"
1.779 +proof -
1.780 +  obtain Z where "openin (subtopology euclidean U) Z" and S'Z: "S' retract_of Z"
1.781 +    by (blast intro: assms ANR_imp_absolute_neighbourhood_retract)
1.782 +  then have UUZ: "closedin (subtopology euclidean U) (U - Z)"
1.783 +    by auto
1.784 +  have "S' \<inter> (U - Z) = {}"
1.785 +    using \<open>S' retract_of Z\<close> closedin_retract closedin_subtopology by fastforce
1.786 +  then obtain V W
1.787 +      where "openin (subtopology euclidean U) V"
1.788 +        and "openin (subtopology euclidean U) W"
1.789 +        and "S' \<subseteq> V" "U - Z \<subseteq> W" "V \<inter> W = {}"
1.790 +      using separation_normal_local [OF US' UUZ]  by auto
1.791 +  moreover have "S' retract_of U - W"
1.792 +    apply (rule retract_of_subset [OF S'Z])
1.793 +    using US' \<open>S' \<subseteq> V\<close> \<open>V \<inter> W = {}\<close> closedin_subset apply fastforce
1.794 +    using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
1.795 +  ultimately show ?thesis
1.796 +    apply (rule_tac V=V and W = "U-W" in that)
1.797 +    using openin_imp_subset apply force+
1.798 +    done
1.799 +qed
1.800 +
1.801 +lemma ANR_imp_closed_neighbourhood_retract:
1.802 +  fixes S :: "'a::euclidean_space set"
1.803 +  assumes "ANR S" "closedin (subtopology euclidean U) S"
1.804 +  obtains V W where "openin (subtopology euclidean U) V"
1.805 +                    "closedin (subtopology euclidean U) W"
1.806 +                    "S \<subseteq> V" "V \<subseteq> W" "S retract_of W"
1.807 +by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl)
1.808 +
1.809 +lemma ANR_homeomorphic_ANR:
1.810 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.811 +  assumes "ANR T" "S homeomorphic T"
1.812 +    shows "ANR S"
1.813 +unfolding ANR_def
1.814 +by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym)
1.815 +
1.816 +lemma homeomorphic_ANR_iff_ANR:
1.817 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.818 +  shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
1.819 +by (metis ANR_homeomorphic_ANR homeomorphic_sym)
1.820 +
1.821 +subsubsection \<open>Analogous properties of ENRs\<close>
1.822 +
1.823 +lemma ENR_imp_absolute_neighbourhood_retract:
1.824 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.825 +  assumes "ENR S" and hom: "S homeomorphic S'"
1.826 +      and "S' \<subseteq> U"
1.827 +  obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
1.828 +proof -
1.829 +  obtain X where "open X" "S retract_of X"
1.830 +    using \<open>ENR S\<close> by (auto simp: ENR_def)
1.831 +  then obtain r where "retraction X S r"
1.832 +    by (auto simp: retract_of_def)
1.833 +  have "locally compact S'"
1.834 +    using retract_of_locally_compact open_imp_locally_compact
1.835 +          homeomorphic_local_compactness \<open>S retract_of X\<close> \<open>open X\<close> hom by blast
1.836 +  then obtain W where UW: "openin (subtopology euclidean U) W"
1.837 +                  and WS': "closedin (subtopology euclidean W) S'"
1.838 +    apply (rule locally_compact_closedin_open)
1.839 +    apply (rename_tac W)
1.840 +    apply (rule_tac W = "U \<inter> W" in that, blast)
1.841 +    by (simp add: \<open>S' \<subseteq> U\<close> closedin_limpt)
1.842 +  obtain f g where hom: "homeomorphism S S' f g"
1.843 +    using assms by (force simp: homeomorphic_def)
1.844 +  have contg: "continuous_on S' g"
1.845 +    using hom homeomorphism_def by blast
1.846 +  moreover have "g ` S' \<subseteq> S" by (metis hom equalityE homeomorphism_def)
1.847 +  ultimately obtain h where conth: "continuous_on W h" and hg: "\<And>x. x \<in> S' \<Longrightarrow> h x = g x"
1.848 +    using Tietze_unbounded [of S' g W] WS' by blast
1.849 +  have "W \<subseteq> U" using UW openin_open by auto
1.850 +  have "S' \<subseteq> W" using WS' closedin_closed by auto
1.851 +  have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
1.852 +    by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
1.853 +  have "S' retract_of (W \<inter> h -` X)"
1.854 +  proof (simp add: retraction_def retract_of_def, intro exI conjI)
1.855 +    show "S' \<subseteq> W" "S' \<subseteq> h -` X"
1.856 +      using him WS' closedin_imp_subset by blast+
1.857 +    show "continuous_on (W \<inter> h -` X) (f \<circ> r \<circ> h)"
1.858 +    proof (intro continuous_on_compose)
1.859 +      show "continuous_on (W \<inter> h -` X) h"
1.860 +        by (meson conth continuous_on_subset inf_le1)
1.861 +      show "continuous_on (h ` (W \<inter> h -` X)) r"
1.862 +      proof -
1.863 +        have "h ` (W \<inter> h -` X) \<subseteq> X"
1.864 +          by blast
1.865 +        then show "continuous_on (h ` (W \<inter> h -` X)) r"
1.866 +          by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
1.867 +      qed
1.868 +      show "continuous_on (r ` h ` (W \<inter> h -` X)) f"
1.869 +        apply (rule continuous_on_subset [of S])
1.870 +         using hom homeomorphism_def apply blast
1.871 +        apply clarify
1.872 +        apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
1.873 +        done
1.874 +    qed
1.875 +    show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
1.876 +      using \<open>retraction X S r\<close> hom
1.877 +      by (auto simp: retraction_def homeomorphism_def)
1.878 +    show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
1.879 +      using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
1.880 +  qed
1.881 +  then show ?thesis
1.882 +    apply (rule_tac V = "W \<inter> h -` X" in that)
1.883 +     apply (rule openin_trans [OF _ UW])
1.884 +     using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
1.885 +     done
1.886 +qed
1.887 +
1.888 +corollary ENR_imp_absolute_neighbourhood_retract_UNIV:
1.889 +  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.890 +  assumes "ENR S" "S homeomorphic S'"
1.891 +  obtains T' where "open T'" "S' retract_of T'"
1.892 +by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV)
1.893 +
1.894 +lemma ENR_homeomorphic_ENR:
1.895 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.896 +  assumes "ENR T" "S homeomorphic T"
1.897 +    shows "ENR S"
1.898 +unfolding ENR_def
1.899 +by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym)
1.900 +
1.901 +lemma homeomorphic_ENR_iff_ENR:
1.902 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.903 +  assumes "S homeomorphic T"
1.904 +    shows "ENR S \<longleftrightarrow> ENR T"
1.905 +by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)
1.906 +
1.907 +lemma ENR_translation:
1.908 +  fixes S :: "'a::euclidean_space set"
1.909 +  shows "ENR(image (\<lambda>x. a + x) S) \<longleftrightarrow> ENR S"
1.910 +by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)
1.911 +
1.912 +lemma ENR_linear_image_eq:
1.913 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.914 +  assumes "linear f" "inj f"
1.915 +  shows "ENR (image f S) \<longleftrightarrow> ENR S"
1.916 +apply (rule homeomorphic_ENR_iff_ENR)
1.917 +using assms homeomorphic_sym linear_homeomorphic_image by auto
1.918 +
1.919 +text \<open>Some relations among the concepts. We also relate AR to being a retract of UNIV, which is
1.920 +often a more convenient proxy in the closed case.\<close>
1.921 +
1.922 +lemma AR_imp_ANR: "AR S \<Longrightarrow> ANR S"
1.923 +  using ANR_def AR_def by fastforce
1.924 +
1.925 +lemma ENR_imp_ANR:
1.926 +  fixes S :: "'a::euclidean_space set"
1.927 +  shows "ENR S \<Longrightarrow> ANR S"
1.929 +by (metis ENR_imp_absolute_neighbourhood_retract closedin_imp_subset)
1.930 +
1.931 +lemma ENR_ANR:
1.932 +  fixes S :: "'a::euclidean_space set"
1.933 +  shows "ENR S \<longleftrightarrow> ANR S \<and> locally compact S"
1.934 +proof
1.935 +  assume "ENR S"
1.936 +  then have "locally compact S"
1.937 +    using ENR_def open_imp_locally_compact retract_of_locally_compact by auto
1.938 +  then show "ANR S \<and> locally compact S"
1.939 +    using ENR_imp_ANR \<open>ENR S\<close> by blast
1.940 +next
1.941 +  assume "ANR S \<and> locally compact S"
1.942 +  then have "ANR S" "locally compact S" by auto
1.943 +  then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T"
1.944 +    using locally_compact_homeomorphic_closed
1.945 +    by (metis DIM_prod DIM_real Suc_eq_plus1 lessI)
1.946 +  then show "ENR S"
1.947 +    using \<open>ANR S\<close>
1.948 +    apply (simp add: ANR_def)
1.949 +    apply (drule_tac x=UNIV in spec)
1.950 +    apply (drule_tac x=T in spec, clarsimp)
1.951 +    apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
1.952 +    done
1.953 +qed
1.954 +
1.955 +
1.956 +lemma AR_ANR:
1.957 +  fixes S :: "'a::euclidean_space set"
1.958 +  shows "AR S \<longleftrightarrow> ANR S \<and> contractible S \<and> S \<noteq> {}"
1.959 +        (is "?lhs = ?rhs")
1.960 +proof
1.961 +  assume ?lhs
1.962 +  obtain C and S' :: "('a * real) set"
1.963 +    where "convex C" "C \<noteq> {}" "closedin (subtopology euclidean C) S'" "S homeomorphic S'"
1.964 +      apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"])
1.965 +      using aff_dim_le_DIM [of S] by auto
1.966 +  with \<open>AR S\<close> have "contractible S"
1.967 +    apply (simp add: AR_def)
1.968 +    apply (drule_tac x=C in spec)
1.969 +    apply (drule_tac x="S'" in spec, simp)
1.970 +    using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce
1.971 +  with \<open>AR S\<close> show ?rhs
1.972 +    apply (auto simp: AR_imp_ANR)
1.973 +    apply (force simp: AR_def)
1.974 +    done
1.975 +next
1.976 +  assume ?rhs
1.977 +  then obtain a and h:: "real \<times> 'a \<Rightarrow> 'a"
1.978 +      where conth: "continuous_on ({0..1} \<times> S) h"
1.979 +        and hS: "h ` ({0..1} \<times> S) \<subseteq> S"
1.980 +        and [simp]: "\<And>x. h(0, x) = x"
1.981 +        and [simp]: "\<And>x. h(1, x) = a"
1.982 +        and "ANR S" "S \<noteq> {}"
1.983 +    by (auto simp: contractible_def homotopic_with_def)
1.984 +  then have "a \<in> S"
1.985 +    by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
1.986 +  have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
1.987 +         if      f: "continuous_on T f" "f ` T \<subseteq> S"
1.988 +            and WT: "closedin (subtopology euclidean W) T"
1.989 +         for W T and f :: "'a \<times> real \<Rightarrow> 'a"
1.990 +  proof -
1.991 +    obtain U g
1.992 +      where "T \<subseteq> U" and WU: "openin (subtopology euclidean W) U"
1.993 +        and contg: "continuous_on U g"
1.994 +        and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
1.995 +      using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, rule_format, OF f WT]
1.996 +      by auto
1.997 +    have WWU: "closedin (subtopology euclidean W) (W - U)"
1.998 +      using WU closedin_diff by fastforce
1.999 +    moreover have "(W - U) \<inter> T = {}"
1.1000 +      using \<open>T \<subseteq> U\<close> by auto
1.1001 +    ultimately obtain V V'
1.1002 +      where WV': "openin (subtopology euclidean W) V'"
1.1003 +        and WV: "openin (subtopology euclidean W) V"
1.1004 +        and "W - U \<subseteq> V'" "T \<subseteq> V" "V' \<inter> V = {}"
1.1005 +      using separation_normal_local [of W "W-U" T] WT by blast
1.1006 +    then have WVT: "T \<inter> (W - V) = {}"
1.1007 +      by auto
1.1008 +    have WWV: "closedin (subtopology euclidean W) (W - V)"
1.1009 +      using WV closedin_diff by fastforce
1.1010 +    obtain j :: " 'a \<times> real \<Rightarrow> real"
1.1011 +      where contj: "continuous_on W j"
1.1012 +        and j:  "\<And>x. x \<in> W \<Longrightarrow> j x \<in> {0..1}"
1.1013 +        and j0: "\<And>x. x \<in> W - V \<Longrightarrow> j x = 1"
1.1014 +        and j1: "\<And>x. x \<in> T \<Longrightarrow> j x = 0"
1.1015 +      by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
1.1016 +    have Weq: "W = (W - V) \<union> (W - V')"
1.1017 +      using \<open>V' \<inter> V = {}\<close> by force
1.1018 +    show ?thesis
1.1019 +    proof (intro conjI exI)
1.1020 +      have *: "continuous_on (W - V') (\<lambda>x. h (j x, g x))"
1.1021 +        apply (rule continuous_on_compose2 [OF conth continuous_on_Pair])
1.1022 +          apply (rule continuous_on_subset [OF contj Diff_subset])
1.1023 +         apply (rule continuous_on_subset [OF contg])
1.1024 +         apply (metis Diff_subset_conv Un_commute \<open>W - U \<subseteq> V'\<close>)
1.1025 +        using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> apply fastforce
1.1026 +        done
1.1027 +      show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
1.1028 +        apply (subst Weq)
1.1029 +        apply (rule continuous_on_cases_local)
1.1030 +            apply (simp_all add: Weq [symmetric] WWV continuous_on_const *)
1.1031 +          using WV' closedin_diff apply fastforce
1.1032 +         apply (auto simp: j0 j1)
1.1033 +        done
1.1034 +    next
1.1035 +      have "h (j (x, y), g (x, y)) \<in> S" if "(x, y) \<in> W" "(x, y) \<in> V" for x y
1.1036 +      proof -
1.1037 +        have "j(x, y) \<in> {0..1}"
1.1038 +          using j that by blast
1.1039 +        moreover have "g(x, y) \<in> S"
1.1040 +          using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
1.1041 +        ultimately show ?thesis
1.1042 +          using hS by blast
1.1043 +      qed
1.1044 +      with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
1.1045 +      show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"
1.1046 +        by auto
1.1047 +    next
1.1048 +      show "\<forall>x\<in>T. (if x \<in> W - V then a else h (j x, g x)) = f x"
1.1049 +        using \<open>T \<subseteq> V\<close> by (auto simp: j0 j1 gf)
1.1050 +    qed
1.1051 +  qed
1.1052 +  then show ?lhs
1.1053 +    by (simp add: AR_eq_absolute_extensor)
1.1054 +qed
1.1055 +
1.1056 +
1.1057 +lemma ANR_retract_of_ANR:
1.1058 +  fixes S :: "'a::euclidean_space set"
1.1059 +  assumes "ANR T" "S retract_of T"
1.1060 +  shows "ANR S"
1.1061 +using assms
1.1062 +apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def)
1.1063 +apply (clarsimp elim!: all_forward)
1.1064 +apply (erule impCE, metis subset_trans)
1.1065 +apply (clarsimp elim!: ex_forward)
1.1066 +apply (rule_tac x="r \<circ> g" in exI)
1.1067 +by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans)
1.1068 +
1.1069 +lemma AR_retract_of_AR:
1.1070 +  fixes S :: "'a::euclidean_space set"
1.1071 +  shows "\<lbrakk>AR T; S retract_of T\<rbrakk> \<Longrightarrow> AR S"
1.1072 +using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce
1.1073 +
1.1074 +lemma ENR_retract_of_ENR:
1.1075 +   "\<lbrakk>ENR T; S retract_of T\<rbrakk> \<Longrightarrow> ENR S"
1.1076 +by (meson ENR_def retract_of_trans)
1.1077 +
1.1078 +lemma retract_of_UNIV:
1.1079 +  fixes S :: "'a::euclidean_space set"
1.1080 +  shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> closed S"
1.1081 +by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV)
1.1082 +
1.1083 +lemma compact_AR:
1.1084 +  fixes S :: "'a::euclidean_space set"
1.1085 +  shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
1.1086 +using compact_imp_closed retract_of_UNIV by blast
1.1087 +
1.1088 +text \<open>More properties of ARs, ANRs and ENRs\<close>
1.1089 +
1.1090 +lemma not_AR_empty [simp]: "~ AR({})"
1.1091 +  by (auto simp: AR_def)
1.1092 +
1.1093 +lemma ENR_empty [simp]: "ENR {}"
1.1094 +  by (simp add: ENR_def)
1.1095 +
1.1096 +lemma ANR_empty [simp]: "ANR ({} :: 'a::euclidean_space set)"
1.1097 +  by (simp add: ENR_imp_ANR)
1.1098 +
1.1099 +lemma convex_imp_AR:
1.1100 +  fixes S :: "'a::euclidean_space set"
1.1101 +  shows "\<lbrakk>convex S; S \<noteq> {}\<rbrakk> \<Longrightarrow> AR S"
1.1102 +apply (rule absolute_extensor_imp_AR)
1.1103 +apply (rule Dugundji, assumption+)
1.1104 +by blast
1.1105 +
1.1106 +lemma convex_imp_ANR:
1.1107 +  fixes S :: "'a::euclidean_space set"
1.1108 +  shows "convex S \<Longrightarrow> ANR S"
1.1109 +using ANR_empty AR_imp_ANR convex_imp_AR by blast
1.1110 +
1.1111 +lemma ENR_convex_closed:
1.1112 +  fixes S :: "'a::euclidean_space set"
1.1113 +  shows "\<lbrakk>closed S; convex S\<rbrakk> \<Longrightarrow> ENR S"
1.1114 +using ENR_def ENR_empty convex_imp_AR retract_of_UNIV by blast
1.1115 +
1.1116 +lemma AR_UNIV [simp]: "AR (UNIV :: 'a::euclidean_space set)"
1.1117 +  using retract_of_UNIV by auto
1.1118 +
1.1119 +lemma ANR_UNIV [simp]: "ANR (UNIV :: 'a::euclidean_space set)"
1.1120 +  by (simp add: AR_imp_ANR)
1.1121 +
1.1122 +lemma ENR_UNIV [simp]:"ENR UNIV"
1.1123 +  using ENR_def by blast
1.1124 +
1.1125 +lemma AR_singleton:
1.1126 +    fixes a :: "'a::euclidean_space"
1.1127 +    shows "AR {a}"
1.1128 +  using retract_of_UNIV by blast
1.1129 +
1.1130 +lemma ANR_singleton:
1.1131 +    fixes a :: "'a::euclidean_space"
1.1132 +    shows "ANR {a}"
1.1133 +  by (simp add: AR_imp_ANR AR_singleton)
1.1134 +
1.1135 +lemma ENR_singleton: "ENR {a}"
1.1136 +  using ENR_def by blast
1.1137 +
1.1138 +text \<open>ARs closed under union\<close>
1.1139 +
1.1140 +lemma AR_closed_Un_local_aux:
1.1141 +  fixes U :: "'a::euclidean_space set"
1.1142 +  assumes "closedin (subtopology euclidean U) S"
1.1143 +          "closedin (subtopology euclidean U) T"
1.1144 +          "AR S" "AR T" "AR(S \<inter> T)"
1.1145 +  shows "(S \<union> T) retract_of U"
1.1146 +proof -
1.1147 +  have "S \<inter> T \<noteq> {}"
1.1148 +    using assms AR_def by fastforce
1.1149 +  have "S \<subseteq> U" "T \<subseteq> U"
1.1150 +    using assms by (auto simp: closedin_imp_subset)
1.1151 +  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
1.1152 +  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
1.1153 +  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
1.1154 +  have US': "closedin (subtopology euclidean U) S'"
1.1155 +    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
1.1156 +    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.1157 +  have UT': "closedin (subtopology euclidean U) T'"
1.1158 +    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
1.1159 +    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.1160 +  have "S \<subseteq> S'"
1.1161 +    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.1162 +  have "T \<subseteq> T'"
1.1163 +    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.1164 +  have "S \<inter> T \<subseteq> W" "W \<subseteq> U"
1.1165 +    using \<open>S \<subseteq> U\<close> by (auto simp: W_def setdist_sing_in_set)
1.1166 +  have "(S \<inter> T) retract_of W"
1.1167 +    apply (rule AR_imp_absolute_retract [OF \<open>AR(S \<inter> T)\<close>])
1.1168 +     apply (simp add: homeomorphic_refl)
1.1169 +    apply (rule closedin_subset_trans [of U])
1.1170 +    apply (simp_all add: assms closedin_Int \<open>S \<inter> T \<subseteq> W\<close> \<open>W \<subseteq> U\<close>)
1.1171 +    done
1.1172 +  then obtain r0
1.1173 +    where "S \<inter> T \<subseteq> W" and contr0: "continuous_on W r0"
1.1174 +      and "r0 ` W \<subseteq> S \<inter> T"
1.1175 +      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
1.1176 +      by (auto simp: retract_of_def retraction_def)
1.1177 +  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
1.1178 +    using setdist_eq_0_closedin \<open>S \<inter> T \<noteq> {}\<close> assms
1.1179 +    by (force simp: W_def setdist_sing_in_set)
1.1180 +  have "S' \<inter> T' = W"
1.1181 +    by (auto simp: S'_def T'_def W_def)
1.1182 +  then have cloUW: "closedin (subtopology euclidean U) W"
1.1183 +    using closedin_Int US' UT' by blast
1.1184 +  define r where "r \<equiv> \<lambda>x. if x \<in> W then r0 x else x"
1.1185 +  have "r ` (W \<union> S) \<subseteq> S" "r ` (W \<union> T) \<subseteq> T"
1.1186 +    using \<open>r0 ` W \<subseteq> S \<inter> T\<close> r_def by auto
1.1187 +  have contr: "continuous_on (W \<union> (S \<union> T)) r"
1.1188 +  unfolding r_def
1.1189 +  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
1.1190 +    show "closedin (subtopology euclidean (W \<union> (S \<union> T))) W"
1.1191 +      using \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> \<open>closedin (subtopology euclidean U) W\<close> closedin_subset_trans by fastforce
1.1192 +    show "closedin (subtopology euclidean (W \<union> (S \<union> T))) (S \<union> T)"
1.1193 +      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
1.1194 +    show "\<And>x. x \<in> W \<and> x \<notin> W \<or> x \<in> S \<union> T \<and> x \<in> W \<Longrightarrow> r0 x = x"
1.1195 +      by (auto simp: ST)
1.1196 +  qed
1.1197 +  have cloUWS: "closedin (subtopology euclidean U) (W \<union> S)"
1.1198 +    by (simp add: cloUW assms closedin_Un)
1.1199 +  obtain g where contg: "continuous_on U g"
1.1200 +             and "g ` U \<subseteq> S" and geqr: "\<And>x. x \<in> W \<union> S \<Longrightarrow> g x = r x"
1.1201 +    apply (rule AR_imp_absolute_extensor [OF \<open>AR S\<close> _ _ cloUWS])
1.1202 +      apply (rule continuous_on_subset [OF contr])
1.1203 +      using \<open>r ` (W \<union> S) \<subseteq> S\<close> apply auto
1.1204 +    done
1.1205 +  have cloUWT: "closedin (subtopology euclidean U) (W \<union> T)"
1.1206 +    by (simp add: cloUW assms closedin_Un)
1.1207 +  obtain h where conth: "continuous_on U h"
1.1208 +             and "h ` U \<subseteq> T" and heqr: "\<And>x. x \<in> W \<union> T \<Longrightarrow> h x = r x"
1.1209 +    apply (rule AR_imp_absolute_extensor [OF \<open>AR T\<close> _ _ cloUWT])
1.1210 +      apply (rule continuous_on_subset [OF contr])
1.1211 +      using \<open>r ` (W \<union> T) \<subseteq> T\<close> apply auto
1.1212 +    done
1.1213 +  have "U = S' \<union> T'"
1.1214 +    by (force simp: S'_def T'_def)
1.1215 +  then have cont: "continuous_on U (\<lambda>x. if x \<in> S' then g x else h x)"
1.1216 +    apply (rule ssubst)
1.1217 +    apply (rule continuous_on_cases_local)
1.1218 +    using US' UT' \<open>S' \<inter> T' = W\<close> \<open>U = S' \<union> T'\<close>
1.1219 +          contg conth continuous_on_subset geqr heqr apply auto
1.1220 +    done
1.1221 +  have UST: "(\<lambda>x. if x \<in> S' then g x else h x) ` U \<subseteq> S \<union> T"
1.1222 +    using \<open>g ` U \<subseteq> S\<close> \<open>h ` U \<subseteq> T\<close> by auto
1.1223 +  show ?thesis
1.1224 +    apply (simp add: retract_of_def retraction_def \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close>)
1.1225 +    apply (rule_tac x="\<lambda>x. if x \<in> S' then g x else h x" in exI)
1.1226 +    apply (intro conjI cont UST)
1.1227 +    by (metis IntI ST Un_iff \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> subsetD geqr heqr r0 r_def)
1.1228 +qed
1.1229 +
1.1230 +
1.1231 +lemma AR_closed_Un_local:
1.1232 +  fixes S :: "'a::euclidean_space set"
1.1233 +  assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
1.1234 +      and STT: "closedin (subtopology euclidean (S \<union> T)) T"
1.1235 +      and "AR S" "AR T" "AR(S \<inter> T)"
1.1236 +    shows "AR(S \<union> T)"
1.1237 +proof -
1.1238 +  have "C retract_of U"
1.1239 +       if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
1.1240 +       for U and C :: "('a * real) set"
1.1241 +  proof -
1.1242 +    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
1.1243 +      using hom by (force simp: homeomorphic_def)
1.1244 +    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
1.1245 +      apply (rule closedin_trans [OF _ UC])
1.1246 +      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
1.1247 +      using hom homeomorphism_def apply blast
1.1248 +      apply (metis hom homeomorphism_def set_eq_subset)
1.1249 +      done
1.1250 +    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
1.1251 +      apply (rule closedin_trans [OF _ UC])
1.1252 +      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
1.1253 +      using hom homeomorphism_def apply blast
1.1254 +      apply (metis hom homeomorphism_def set_eq_subset)
1.1255 +      done
1.1256 +    have ARS: "AR (C \<inter> g -` S)"
1.1257 +      apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
1.1258 +      apply (simp add: homeomorphic_def)
1.1259 +      apply (rule_tac x=g in exI)
1.1260 +      apply (rule_tac x=f in exI)
1.1261 +      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.1262 +      apply (rule_tac x="f x" in image_eqI, auto)
1.1263 +      done
1.1264 +    have ART: "AR (C \<inter> g -` T)"
1.1265 +      apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
1.1266 +      apply (simp add: homeomorphic_def)
1.1267 +      apply (rule_tac x=g in exI)
1.1268 +      apply (rule_tac x=f in exI)
1.1269 +      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.1270 +      apply (rule_tac x="f x" in image_eqI, auto)
1.1271 +      done
1.1272 +    have ARI: "AR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
1.1273 +      apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
1.1274 +      apply (simp add: homeomorphic_def)
1.1275 +      apply (rule_tac x=g in exI)
1.1276 +      apply (rule_tac x=f in exI)
1.1277 +      using hom
1.1278 +      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.1279 +      apply (rule_tac x="f x" in image_eqI, auto)
1.1280 +      done
1.1281 +    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
1.1282 +      using hom  by (auto simp: homeomorphism_def)
1.1283 +    then show ?thesis
1.1284 +      by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
1.1285 +  qed
1.1286 +  then show ?thesis
1.1287 +    by (force simp: AR_def)
1.1288 +qed
1.1289 +
1.1290 +corollary AR_closed_Un:
1.1291 +  fixes S :: "'a::euclidean_space set"
1.1292 +  shows "\<lbrakk>closed S; closed T; AR S; AR T; AR (S \<inter> T)\<rbrakk> \<Longrightarrow> AR (S \<union> T)"
1.1293 +by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV)
1.1294 +
1.1295 +text \<open>ANRs closed under union\<close>
1.1296 +
1.1297 +lemma ANR_closed_Un_local_aux:
1.1298 +  fixes U :: "'a::euclidean_space set"
1.1299 +  assumes US: "closedin (subtopology euclidean U) S"
1.1300 +      and UT: "closedin (subtopology euclidean U) T"
1.1301 +      and "ANR S" "ANR T" "ANR(S \<inter> T)"
1.1302 +  obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
1.1303 +proof (cases "S = {} \<or> T = {}")
1.1304 +  case True with assms that show ?thesis
1.1305 +    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
1.1306 +next
1.1307 +  case False
1.1308 +  then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
1.1309 +  have "S \<subseteq> U" "T \<subseteq> U"
1.1310 +    using assms by (auto simp: closedin_imp_subset)
1.1311 +  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
1.1312 +  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
1.1313 +  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
1.1314 +  have cloUS': "closedin (subtopology euclidean U) S'"
1.1315 +    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
1.1316 +    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.1317 +  have cloUT': "closedin (subtopology euclidean U) T'"
1.1318 +    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
1.1319 +    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.1320 +  have "S \<subseteq> S'"
1.1321 +    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.1322 +  have "T \<subseteq> T'"
1.1323 +    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.1324 +  have "S' \<union> T' = U"
1.1325 +    by (auto simp: S'_def T'_def)
1.1326 +  have "W \<subseteq> S'"
1.1327 +    by (simp add: Collect_mono S'_def W_def)
1.1328 +  have "W \<subseteq> T'"
1.1329 +    by (simp add: Collect_mono T'_def W_def)
1.1330 +  have ST_W: "S \<inter> T \<subseteq> W" and "W \<subseteq> U"
1.1331 +    using \<open>S \<subseteq> U\<close> by (force simp: W_def setdist_sing_in_set)+
1.1332 +  have "S' \<inter> T' = W"
1.1333 +    by (auto simp: S'_def T'_def W_def)
1.1334 +  then have cloUW: "closedin (subtopology euclidean U) W"
1.1335 +    using closedin_Int cloUS' cloUT' by blast
1.1336 +  obtain W' W0 where "openin (subtopology euclidean W) W'"
1.1337 +                 and cloWW0: "closedin (subtopology euclidean W) W0"
1.1338 +                 and "S \<inter> T \<subseteq> W'" "W' \<subseteq> W0"
1.1339 +                 and ret: "(S \<inter> T) retract_of W0"
1.1340 +    apply (rule ANR_imp_closed_neighbourhood_retract [OF \<open>ANR(S \<inter> T)\<close>])
1.1341 +    apply (rule closedin_subset_trans [of U, OF _ ST_W \<open>W \<subseteq> U\<close>])
1.1342 +    apply (blast intro: assms)+
1.1343 +    done
1.1344 +  then obtain U0 where opeUU0: "openin (subtopology euclidean U) U0"
1.1345 +                   and U0: "S \<inter> T \<subseteq> U0" "U0 \<inter> W \<subseteq> W0"
1.1346 +    unfolding openin_open  using \<open>W \<subseteq> U\<close> by blast
1.1347 +  have "W0 \<subseteq> U"
1.1348 +    using \<open>W \<subseteq> U\<close> cloWW0 closedin_subset by fastforce
1.1349 +  obtain r0
1.1350 +    where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
1.1351 +      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
1.1352 +    using ret  by (force simp: retract_of_def retraction_def)
1.1353 +  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
1.1354 +    using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
1.1355 +  define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
1.1356 +  have "r ` (W0 \<union> S) \<subseteq> S" "r ` (W0 \<union> T) \<subseteq> T"
1.1357 +    using \<open>r0 ` W0 \<subseteq> S \<inter> T\<close> r_def by auto
1.1358 +  have contr: "continuous_on (W0 \<union> (S \<union> T)) r"
1.1359 +  unfolding r_def
1.1360 +  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
1.1361 +    show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) W0"
1.1362 +      apply (rule closedin_subset_trans [of U])
1.1363 +      using cloWW0 cloUW closedin_trans \<open>W0 \<subseteq> U\<close> \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> apply blast+
1.1364 +      done
1.1365 +    show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) (S \<union> T)"
1.1366 +      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W0 \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
1.1367 +    show "\<And>x. x \<in> W0 \<and> x \<notin> W0 \<or> x \<in> S \<union> T \<and> x \<in> W0 \<Longrightarrow> r0 x = x"
1.1368 +      using ST cloWW0 closedin_subset by fastforce
1.1369 +  qed
1.1370 +  have cloS'WS: "closedin (subtopology euclidean S') (W0 \<union> S)"
1.1371 +    by (meson closedin_subset_trans US cloUS' \<open>S \<subseteq> S'\<close> \<open>W \<subseteq> S'\<close> cloUW cloWW0
1.1372 +              closedin_Un closedin_imp_subset closedin_trans)
1.1373 +  obtain W1 g where "W0 \<union> S \<subseteq> W1" and contg: "continuous_on W1 g"
1.1374 +                and opeSW1: "openin (subtopology euclidean S') W1"
1.1375 +                and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
1.1376 +    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
1.1377 +     apply (rule continuous_on_subset [OF contr], blast+)
1.1378 +    done
1.1379 +  have cloT'WT: "closedin (subtopology euclidean T') (W0 \<union> T)"
1.1380 +    by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0
1.1381 +              closedin_Un closedin_imp_subset closedin_trans)
1.1382 +  obtain W2 h where "W0 \<union> T \<subseteq> W2" and conth: "continuous_on W2 h"
1.1383 +                and opeSW2: "openin (subtopology euclidean T') W2"
1.1384 +                and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
1.1385 +    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
1.1386 +     apply (rule continuous_on_subset [OF contr], blast+)
1.1387 +    done
1.1388 +  have "S' \<inter> T' = W"
1.1389 +    by (force simp: S'_def T'_def W_def)
1.1390 +  obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
1.1391 +    using opeSW1 opeSW2 by (force simp: openin_open)
1.1392 +  show ?thesis
1.1393 +  proof
1.1394 +    have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
1.1395 +         ((U - T') \<inter> O1 \<union> (U - S') \<inter> O2 \<union> U \<inter> O1 \<inter> O2) - (W - U0)"
1.1396 +     using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close>
1.1397 +      by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
1.1398 +    show "openin (subtopology euclidean U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
1.1399 +      apply (subst eq)
1.1400 +      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>, simp_all)
1.1401 +      done
1.1402 +    have cloW1: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
1.1403 +      using cloUS' apply (simp add: closedin_closed)
1.1404 +      apply (erule ex_forward)
1.1405 +      using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
1.1406 +      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
1.1407 +      done
1.1408 +    have cloW2: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
1.1409 +      using cloUT' apply (simp add: closedin_closed)
1.1410 +      apply (erule ex_forward)
1.1411 +      using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
1.1412 +      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
1.1413 +      done
1.1414 +    have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
1.1415 +      using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr
1.1416 +      apply (auto simp: r_def, fastforce)
1.1417 +      using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close>  by auto
1.1418 +    have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
1.1419 +              r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and>
1.1420 +              (\<forall>x\<in>S \<union> T. r x = x)"
1.1421 +      apply (rule_tac x = "\<lambda>x. if  x \<in> S' then g x else h x" in exI)
1.1422 +      apply (intro conjI *)
1.1423 +      apply (rule continuous_on_cases_local
1.1424 +                  [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]])
1.1425 +      using \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close>
1.1426 +            \<open>g ` W1 \<subseteq> S\<close> \<open>h ` W2 \<subseteq> T\<close> apply auto
1.1427 +      using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> apply (fastforce simp add: geqr heqr)+
1.1428 +      done
1.1429 +    then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
1.1430 +      using  \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
1.1431 +      by (auto simp: retract_of_def retraction_def)
1.1432 +  qed
1.1433 +qed
1.1434 +
1.1435 +
1.1436 +lemma ANR_closed_Un_local:
1.1437 +  fixes S :: "'a::euclidean_space set"
1.1438 +  assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
1.1439 +      and STT: "closedin (subtopology euclidean (S \<union> T)) T"
1.1440 +      and "ANR S" "ANR T" "ANR(S \<inter> T)"
1.1441 +    shows "ANR(S \<union> T)"
1.1442 +proof -
1.1443 +  have "\<exists>T. openin (subtopology euclidean U) T \<and> C retract_of T"
1.1444 +       if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
1.1445 +       for U and C :: "('a * real) set"
1.1446 +  proof -
1.1447 +    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
1.1448 +      using hom by (force simp: homeomorphic_def)
1.1449 +    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
1.1450 +      apply (rule closedin_trans [OF _ UC])
1.1451 +      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
1.1452 +      using hom [unfolded homeomorphism_def] apply blast
1.1453 +      apply (metis hom homeomorphism_def set_eq_subset)
1.1454 +      done
1.1455 +    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
1.1456 +      apply (rule closedin_trans [OF _ UC])
1.1457 +      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
1.1458 +      using hom [unfolded homeomorphism_def] apply blast
1.1459 +      apply (metis hom homeomorphism_def set_eq_subset)
1.1460 +      done
1.1461 +    have ANRS: "ANR (C \<inter> g -` S)"
1.1462 +      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
1.1463 +      apply (simp add: homeomorphic_def)
1.1464 +      apply (rule_tac x=g in exI)
1.1465 +      apply (rule_tac x=f in exI)
1.1466 +      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.1467 +      apply (rule_tac x="f x" in image_eqI, auto)
1.1468 +      done
1.1469 +    have ANRT: "ANR (C \<inter> g -` T)"
1.1470 +      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
1.1471 +      apply (simp add: homeomorphic_def)
1.1472 +      apply (rule_tac x=g in exI)
1.1473 +      apply (rule_tac x=f in exI)
1.1474 +      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.1475 +      apply (rule_tac x="f x" in image_eqI, auto)
1.1476 +      done
1.1477 +    have ANRI: "ANR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
1.1478 +      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
1.1479 +      apply (simp add: homeomorphic_def)
1.1480 +      apply (rule_tac x=g in exI)
1.1481 +      apply (rule_tac x=f in exI)
1.1482 +      using hom
1.1483 +      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.1484 +      apply (rule_tac x="f x" in image_eqI, auto)
1.1485 +      done
1.1486 +    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
1.1487 +      using hom by (auto simp: homeomorphism_def)
1.1488 +    then show ?thesis
1.1489 +      by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
1.1490 +  qed
1.1491 +  then show ?thesis
1.1492 +    by (auto simp: ANR_def)
1.1493 +qed
1.1494 +
1.1495 +corollary ANR_closed_Un:
1.1496 +  fixes S :: "'a::euclidean_space set"
1.1497 +  shows "\<lbrakk>closed S; closed T; ANR S; ANR T; ANR (S \<inter> T)\<rbrakk> \<Longrightarrow> ANR (S \<union> T)"
1.1498 +by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int)
1.1499 +
1.1500 +lemma ANR_openin:
1.1501 +  fixes S :: "'a::euclidean_space set"
1.1502 +  assumes "ANR T" and opeTS: "openin (subtopology euclidean T) S"
1.1503 +  shows "ANR S"
1.1504 +proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
1.1505 +  fix f :: "'a \<times> real \<Rightarrow> 'a" and U C
1.1506 +  assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> S"
1.1507 +     and cloUC: "closedin (subtopology euclidean U) C"
1.1508 +  have "f ` C \<subseteq> T"
1.1509 +    using fim opeTS openin_imp_subset by blast
1.1510 +  obtain W g where "C \<subseteq> W"
1.1511 +               and UW: "openin (subtopology euclidean U) W"
1.1512 +               and contg: "continuous_on W g"
1.1513 +               and gim: "g ` W \<subseteq> T"
1.1514 +               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
1.1515 +    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f ` C \<subseteq> T\<close> cloUC])
1.1516 +    using fim by auto
1.1517 +  show "\<exists>V g. C \<subseteq> V \<and> openin (subtopology euclidean U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
1.1518 +  proof (intro exI conjI)
1.1519 +    show "C \<subseteq> W \<inter> g -` S"
1.1520 +      using \<open>C \<subseteq> W\<close> fim geq by blast
1.1521 +    show "openin (subtopology euclidean U) (W \<inter> g -` S)"
1.1522 +      by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
1.1523 +    show "continuous_on (W \<inter> g -` S) g"
1.1524 +      by (blast intro: continuous_on_subset [OF contg])
1.1525 +    show "g ` (W \<inter> g -` S) \<subseteq> S"
1.1526 +      using gim by blast
1.1527 +    show "\<forall>x\<in>C. g x = f x"
1.1528 +      using geq by blast
1.1529 +  qed
1.1530 +qed
1.1531 +
1.1532 +lemma ENR_openin:
1.1533 +    fixes S :: "'a::euclidean_space set"
1.1534 +    assumes "ENR T" and opeTS: "openin (subtopology euclidean T) S"
1.1535 +    shows "ENR S"
1.1536 +  using assms apply (simp add: ENR_ANR)
1.1537 +  using ANR_openin locally_open_subset by blast
1.1538 +
1.1539 +lemma ANR_neighborhood_retract:
1.1540 +    fixes S :: "'a::euclidean_space set"
1.1541 +    assumes "ANR U" "S retract_of T" "openin (subtopology euclidean U) T"
1.1542 +    shows "ANR S"
1.1543 +  using ANR_openin ANR_retract_of_ANR assms by blast
1.1544 +
1.1545 +lemma ENR_neighborhood_retract:
1.1546 +    fixes S :: "'a::euclidean_space set"
1.1547 +    assumes "ENR U" "S retract_of T" "openin (subtopology euclidean U) T"
1.1548 +    shows "ENR S"
1.1549 +  using ENR_openin ENR_retract_of_ENR assms by blast
1.1550 +
1.1551 +lemma ANR_rel_interior:
1.1552 +  fixes S :: "'a::euclidean_space set"
1.1553 +  shows "ANR S \<Longrightarrow> ANR(rel_interior S)"
1.1554 +   by (blast intro: ANR_openin openin_set_rel_interior)
1.1555 +
1.1556 +lemma ANR_delete:
1.1557 +  fixes S :: "'a::euclidean_space set"
1.1558 +  shows "ANR S \<Longrightarrow> ANR(S - {a})"
1.1559 +   by (blast intro: ANR_openin openin_delete openin_subtopology_self)
1.1560 +
1.1561 +lemma ENR_rel_interior:
1.1562 +  fixes S :: "'a::euclidean_space set"
1.1563 +  shows "ENR S \<Longrightarrow> ENR(rel_interior S)"
1.1564 +   by (blast intro: ENR_openin openin_set_rel_interior)
1.1565 +
1.1566 +lemma ENR_delete:
1.1567 +  fixes S :: "'a::euclidean_space set"
1.1568 +  shows "ENR S \<Longrightarrow> ENR(S - {a})"
1.1569 +   by (blast intro: ENR_openin openin_delete openin_subtopology_self)
1.1570 +
1.1571 +lemma open_imp_ENR: "open S \<Longrightarrow> ENR S"
1.1572 +    using ENR_def by blast
1.1573 +
1.1574 +lemma open_imp_ANR:
1.1575 +    fixes S :: "'a::euclidean_space set"
1.1576 +    shows "open S \<Longrightarrow> ANR S"
1.1577 +  by (simp add: ENR_imp_ANR open_imp_ENR)
1.1578 +
1.1579 +lemma ANR_ball [iff]:
1.1580 +    fixes a :: "'a::euclidean_space"
1.1581 +    shows "ANR(ball a r)"
1.1582 +  by (simp add: convex_imp_ANR)
1.1583 +
1.1584 +lemma ENR_ball [iff]: "ENR(ball a r)"
1.1585 +  by (simp add: open_imp_ENR)
1.1586 +
1.1587 +lemma AR_ball [simp]:
1.1588 +    fixes a :: "'a::euclidean_space"
1.1589 +    shows "AR(ball a r) \<longleftrightarrow> 0 < r"
1.1590 +  by (auto simp: AR_ANR convex_imp_contractible)
1.1591 +
1.1592 +lemma ANR_cball [iff]:
1.1593 +    fixes a :: "'a::euclidean_space"
1.1594 +    shows "ANR(cball a r)"
1.1595 +  by (simp add: convex_imp_ANR)
1.1596 +
1.1597 +lemma ENR_cball:
1.1598 +    fixes a :: "'a::euclidean_space"
1.1599 +    shows "ENR(cball a r)"
1.1600 +  using ENR_convex_closed by blast
1.1601 +
1.1602 +lemma AR_cball [simp]:
1.1603 +    fixes a :: "'a::euclidean_space"
1.1604 +    shows "AR(cball a r) \<longleftrightarrow> 0 \<le> r"
1.1605 +  by (auto simp: AR_ANR convex_imp_contractible)
1.1606 +
1.1607 +lemma ANR_box [iff]:
1.1608 +    fixes a :: "'a::euclidean_space"
1.1609 +    shows "ANR(cbox a b)" "ANR(box a b)"
1.1610 +  by (auto simp: convex_imp_ANR open_imp_ANR)
1.1611 +
1.1612 +lemma ENR_box [iff]:
1.1613 +    fixes a :: "'a::euclidean_space"
1.1614 +    shows "ENR(cbox a b)" "ENR(box a b)"
1.1615 +apply (simp add: ENR_convex_closed closed_cbox)
1.1616 +by (simp add: open_box open_imp_ENR)
1.1617 +
1.1618 +lemma AR_box [simp]:
1.1619 +    "AR(cbox a b) \<longleftrightarrow> cbox a b \<noteq> {}" "AR(box a b) \<longleftrightarrow> box a b \<noteq> {}"
1.1620 +  by (auto simp: AR_ANR convex_imp_contractible)
1.1621 +
1.1622 +lemma ANR_interior:
1.1623 +     fixes S :: "'a::euclidean_space set"
1.1624 +     shows "ANR(interior S)"
1.1625 +  by (simp add: open_imp_ANR)
1.1626 +
1.1627 +lemma ENR_interior:
1.1628 +     fixes S :: "'a::euclidean_space set"
1.1629 +     shows "ENR(interior S)"
1.1630 +  by (simp add: open_imp_ENR)
1.1631 +
1.1632 +lemma AR_imp_contractible:
1.1633 +    fixes S :: "'a::euclidean_space set"
1.1634 +    shows "AR S \<Longrightarrow> contractible S"
1.1635 +  by (simp add: AR_ANR)
1.1636 +
1.1637 +lemma ENR_imp_locally_compact:
1.1638 +    fixes S :: "'a::euclidean_space set"
1.1639 +    shows "ENR S \<Longrightarrow> locally compact S"
1.1640 +  by (simp add: ENR_ANR)
1.1641 +
1.1642 +lemma ANR_imp_locally_path_connected:
1.1643 +  fixes S :: "'a::euclidean_space set"
1.1644 +  assumes "ANR S"
1.1645 +    shows "locally path_connected S"
1.1646 +proof -
1.1647 +  obtain U and T :: "('a \<times> real) set"
1.1648 +     where "convex U" "U \<noteq> {}"
1.1649 +       and UT: "closedin (subtopology euclidean U) T"
1.1650 +       and "S homeomorphic T"
1.1651 +    apply (rule homeomorphic_closedin_convex [of S])
1.1652 +    using aff_dim_le_DIM [of S] apply auto
1.1653 +    done
1.1654 +  then have "locally path_connected T"
1.1655 +    by (meson ANR_imp_absolute_neighbourhood_retract
1.1656 +        assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
1.1657 +  then have S: "locally path_connected S"
1.1658 +      if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
1.1659 +    using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
1.1660 +  show ?thesis
1.1661 +    using assms
1.1662 +    apply (clarsimp simp: ANR_def)
1.1663 +    apply (drule_tac x=U in spec)
1.1664 +    apply (drule_tac x=T in spec)
1.1665 +    using \<open>S homeomorphic T\<close> \<open>U \<noteq> {}\<close> UT  apply (blast intro: S)
1.1666 +    done
1.1667 +qed
1.1668 +
1.1669 +lemma ANR_imp_locally_connected:
1.1670 +  fixes S :: "'a::euclidean_space set"
1.1671 +  assumes "ANR S"
1.1672 +    shows "locally connected S"
1.1673 +using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto
1.1674 +
1.1675 +lemma AR_imp_locally_path_connected:
1.1676 +  fixes S :: "'a::euclidean_space set"
1.1677 +  assumes "AR S"
1.1678 +    shows "locally path_connected S"
1.1679 +by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms)
1.1680 +
1.1681 +lemma AR_imp_locally_connected:
1.1682 +  fixes S :: "'a::euclidean_space set"
1.1683 +  assumes "AR S"
1.1684 +    shows "locally connected S"
1.1685 +using ANR_imp_locally_connected AR_ANR assms by blast
1.1686 +
1.1687 +lemma ENR_imp_locally_path_connected:
1.1688 +  fixes S :: "'a::euclidean_space set"
1.1689 +  assumes "ENR S"
1.1690 +    shows "locally path_connected S"
1.1691 +by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms)
1.1692 +
1.1693 +lemma ENR_imp_locally_connected:
1.1694 +  fixes S :: "'a::euclidean_space set"
1.1695 +  assumes "ENR S"
1.1696 +    shows "locally connected S"
1.1697 +using ANR_imp_locally_connected ENR_ANR assms by blast
1.1698 +
1.1699 +lemma ANR_Times:
1.1700 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.1701 +  assumes "ANR S" "ANR T" shows "ANR(S \<times> T)"
1.1702 +proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
1.1703 +  fix f :: " ('a \<times> 'b) \<times> real \<Rightarrow> 'a \<times> 'b" and U C
1.1704 +  assume "continuous_on C f" and fim: "f ` C \<subseteq> S \<times> T"
1.1705 +     and cloUC: "closedin (subtopology euclidean U) C"
1.1706 +  have contf1: "continuous_on C (fst \<circ> f)"
1.1707 +    by (simp add: \<open>continuous_on C f\<close> continuous_on_fst)
1.1708 +  obtain W1 g where "C \<subseteq> W1"
1.1709 +               and UW1: "openin (subtopology euclidean U) W1"
1.1710 +               and contg: "continuous_on W1 g"
1.1711 +               and gim: "g ` W1 \<subseteq> S"
1.1712 +               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = (fst \<circ> f) x"
1.1713 +    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> contf1 _ cloUC])
1.1714 +    using fim apply auto
1.1715 +    done
1.1716 +  have contf2: "continuous_on C (snd \<circ> f)"
1.1717 +    by (simp add: \<open>continuous_on C f\<close> continuous_on_snd)
1.1718 +  obtain W2 h where "C \<subseteq> W2"
1.1719 +               and UW2: "openin (subtopology euclidean U) W2"
1.1720 +               and conth: "continuous_on W2 h"
1.1721 +               and him: "h ` W2 \<subseteq> T"
1.1722 +               and heq: "\<And>x. x \<in> C \<Longrightarrow> h x = (snd \<circ> f) x"
1.1723 +    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf2 _ cloUC])
1.1724 +    using fim apply auto
1.1725 +    done
1.1726 +  show "\<exists>V g. C \<subseteq> V \<and>
1.1727 +               openin (subtopology euclidean U) V \<and>
1.1728 +               continuous_on V g \<and> g ` V \<subseteq> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
1.1729 +  proof (intro exI conjI)
1.1730 +    show "C \<subseteq> W1 \<inter> W2"
1.1731 +      by (simp add: \<open>C \<subseteq> W1\<close> \<open>C \<subseteq> W2\<close>)
1.1732 +    show "openin (subtopology euclidean U) (W1 \<inter> W2)"
1.1733 +      by (simp add: UW1 UW2 openin_Int)
1.1734 +    show  "continuous_on (W1 \<inter> W2) (\<lambda>x. (g x, h x))"
1.1735 +      by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
1.1736 +    show  "(\<lambda>x. (g x, h x)) ` (W1 \<inter> W2) \<subseteq> S \<times> T"
1.1737 +      using gim him by blast
1.1738 +    show  "(\<forall>x\<in>C. (g x, h x) = f x)"
1.1739 +      using geq heq by auto
1.1740 +  qed
1.1741 +qed
1.1742 +
1.1743 +lemma AR_Times:
1.1744 +  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.1745 +  assumes "AR S" "AR T" shows "AR(S \<times> T)"
1.1746 +using assms by (simp add: AR_ANR ANR_Times contractible_Times)
1.1747 +
1.1748 +subsection \<open>Kuhn Simplices\<close>
1.1749 +
1.1750  lemma bij_betw_singleton_eq:
1.1751    assumes f: "bij_betw f A B" and g: "bij_betw g A B" and a: "a \<in> A"
1.1752    assumes eq: "(\<And>x. x \<in> A \<Longrightarrow> x \<noteq> a \<Longrightarrow> f x = g x)"
1.1753 @@ -59,6 +1795,7 @@
1.1754      using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
1.1755  qed auto
1.1756
1.1757 +(* FIXME mv *)
1.1758  lemma brouwer_compactness_lemma:
1.1759    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.1760    assumes "compact s"
1.1761 @@ -107,7 +1844,7 @@
1.1762  qed
1.1763
1.1764
1.1765 -subsection \<open>The key "counting" observation, somewhat abstracted\<close>
1.1766 +subsubsection \<open>The key "counting" observation, somewhat abstracted\<close>
1.1767
1.1768  lemma kuhn_counting_lemma:
1.1769    fixes bnd compo compo' face S F
1.1770 @@ -138,7 +1875,7 @@
1.1771      by auto
1.1772  qed
1.1773
1.1774 -subsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
1.1775 +subsubsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
1.1776
1.1777  lemma kuhn_complete_lemma:
1.1778    assumes [simp]: "finite simplices"
1.1779 @@ -1102,7 +2839,7 @@
1.1780        by (subst (asm) eq_commute) auto }
1.1781  qed
1.1782
1.1783 -subsection \<open>Reduced labelling\<close>
1.1784 +subsubsection \<open>Reduced labelling\<close>
1.1785
1.1786  definition reduced :: "nat \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> nat" where "reduced n x = (LEAST k. k = n \<or> x k \<noteq> 0)"
1.1787
1.1788 @@ -1348,7 +3085,7 @@
1.1789    qed
1.1790  qed
1.1791
1.1792 -subsection \<open>The main result for the unit cube\<close>
1.1793 +subsubsection \<open>Main result for the unit cube\<close>
1.1794
1.1795  lemma kuhn_labelling_lemma':
1.1796    assumes "(\<forall>x::nat\<Rightarrow>real. P x \<longrightarrow> P (f x))"
1.1797 @@ -1387,32 +3124,9 @@
1.1798    qed
1.1799  qed
1.1800
1.1801 -definition unit_cube :: "'a::euclidean_space set"
1.1802 -  where "unit_cube = {x. \<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1}"
1.1803 -
1.1804 -lemma mem_unit_cube: "x \<in> unit_cube \<longleftrightarrow> (\<forall>i\<in>Basis. 0 \<le> x \<bullet> i \<and> x \<bullet> i \<le> 1)"
1.1805 -  unfolding unit_cube_def by simp
1.1806 -
1.1807 -lemma bounded_unit_cube: "bounded unit_cube"
1.1808 -  unfolding bounded_def
1.1809 -proof (intro exI ballI)
1.1810 -  fix y :: 'a assume y: "y \<in> unit_cube"
1.1811 -  have "dist 0 y = norm y" by (rule dist_0_norm)
1.1812 -  also have "\<dots> = norm (\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R i)" unfolding euclidean_representation ..
1.1813 -  also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm ((y \<bullet> i) *\<^sub>R i))" by (rule norm_sum)
1.1814 -  also have "\<dots> \<le> (\<Sum>i::'a\<in>Basis. 1)"
1.1815 -    by (rule sum_mono, simp add: y [unfolded mem_unit_cube])
1.1816 -  finally show "dist 0 y \<le> (\<Sum>i::'a\<in>Basis. 1)" .
1.1817 -qed
1.1818 -
1.1819 -lemma closed_unit_cube: "closed unit_cube"
1.1820 -  unfolding unit_cube_def Collect_ball_eq Collect_conj_eq
1.1821 -  by (rule closed_INT, auto intro!: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
1.1822 -
1.1823 -lemma compact_unit_cube: "compact unit_cube" (is "compact ?C")
1.1824 -  unfolding compact_eq_seq_compact_metric
1.1825 -  using bounded_unit_cube closed_unit_cube
1.1826 -  by (rule bounded_closed_imp_seq_compact)
1.1827 +subsection \<open>Brouwer's fixed point theorem\<close>
1.1828 +
1.1829 +text \<open>We start proving Brouwer's fixed point theorem for unit cubes.\<close>
1.1830
1.1831  lemma brouwer_cube:
1.1832    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
1.1833 @@ -1685,94 +3399,7 @@
1.1834      using i by auto
1.1835  qed
1.1836
1.1837 -
1.1838 -subsection \<open>Retractions\<close>
1.1839 -
1.1840 -definition "retraction S T r \<longleftrightarrow> T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
1.1841 -
1.1842 -definition retract_of (infixl "retract'_of" 50)
1.1843 -  where "(T retract_of S) \<longleftrightarrow> (\<exists>r. retraction S T r)"
1.1844 -
1.1845 -lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
1.1846 -  unfolding retraction_def by auto
1.1847 -
1.1848 -subsection \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
1.1849 -
1.1850 -lemma invertible_fixpoint_property:
1.1851 -  fixes S :: "'a::euclidean_space set"
1.1852 -    and T :: "'b::euclidean_space set"
1.1853 -  assumes contt: "continuous_on T i"
1.1854 -    and "i ` T \<subseteq> S"
1.1855 -    and contr: "continuous_on S r"
1.1856 -    and "r ` S \<subseteq> T"
1.1857 -    and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
1.1858 -    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
1.1859 -    and contg: "continuous_on T g"
1.1860 -    and "g ` T \<subseteq> T"
1.1861 -  obtains y where "y \<in> T" and "g y = y"
1.1862 -proof -
1.1863 -  have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
1.1864 -  proof (rule FP)
1.1865 -    show "continuous_on S (i \<circ> g \<circ> r)"
1.1866 -      by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
1.1867 -    show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
1.1868 -      using assms(2,4,8) by force
1.1869 -  qed
1.1870 -  then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
1.1871 -  then have *: "g (r x) \<in> T"
1.1872 -    using assms(4,8) by auto
1.1873 -  have "r ((i \<circ> g \<circ> r) x) = r x"
1.1874 -    using x by auto
1.1875 -  then show ?thesis
1.1876 -    using "*" ri that by auto
1.1877 -qed
1.1878 -
1.1879 -lemma homeomorphic_fixpoint_property:
1.1880 -  fixes S :: "'a::euclidean_space set"
1.1881 -    and T :: "'b::euclidean_space set"
1.1882 -  assumes "S homeomorphic T"
1.1883 -  shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
1.1884 -         (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
1.1885 -         (is "?lhs = ?rhs")
1.1886 -proof -
1.1887 -  obtain r i where r:
1.1888 -      "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
1.1889 -      "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
1.1890 -    using assms unfolding homeomorphic_def homeomorphism_def  by blast
1.1891 -  show ?thesis
1.1892 -  proof
1.1893 -    assume ?lhs
1.1894 -    with r show ?rhs
1.1895 -      by (metis invertible_fixpoint_property[of T i S r] order_refl)
1.1896 -  next
1.1897 -    assume ?rhs
1.1898 -    with r show ?lhs
1.1899 -      by (metis invertible_fixpoint_property[of S r T i] order_refl)
1.1900 -  qed
1.1901 -qed
1.1902 -
1.1903 -lemma retract_fixpoint_property:
1.1904 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.1905 -    and S :: "'a set"
1.1906 -  assumes "T retract_of S"
1.1907 -    and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
1.1908 -    and contg: "continuous_on T g"
1.1909 -    and "g ` T \<subseteq> T"
1.1910 -  obtains y where "y \<in> T" and "g y = y"
1.1911 -proof -
1.1912 -  obtain h where "retraction S T h"
1.1913 -    using assms(1) unfolding retract_of_def ..
1.1914 -  then show ?thesis
1.1915 -    unfolding retraction_def
1.1916 -    using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
1.1917 -    by (metis assms(4) contg image_ident that)
1.1918 -qed
1.1919 -
1.1920 -
1.1921 -subsection \<open>The Brouwer theorem for any set with nonempty interior\<close>
1.1922 -
1.1923 -lemma convex_unit_cube: "convex unit_cube"
1.1924 -  by (rule is_interval_convex) (fastforce simp add: is_interval_def mem_unit_cube)
1.1925 +text \<open>Next step is to prove it for nonempty interiors.\<close>
1.1926
1.1927  lemma brouwer_weak:
1.1928    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
1.1929 @@ -1806,8 +3433,7 @@
1.1930      by (auto intro: that)
1.1931  qed
1.1932
1.1933 -
1.1934 -text \<open>And in particular for a closed ball.\<close>
1.1935 +text \<open>Then the particular case for closed balls.\<close>
1.1936
1.1937  lemma brouwer_ball:
1.1938    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
1.1939 @@ -1819,11 +3445,9 @@
1.1940    unfolding interior_cball ball_eq_empty
1.1941    using assms by auto
1.1942
1.1943 -text \<open>Still more general form; could derive this directly without using the
1.1944 -  rather involved \<open>HOMEOMORPHIC_CONVEX_COMPACT\<close> theorem, just using
1.1945 -  a scaling and translation to put the set inside the unit cube.\<close>
1.1946 -
1.1947 -lemma brouwer:
1.1948 +text \<open>And finally we prove Brouwer's fixed point theorem in its general version.\<close>
1.1949 +
1.1950 +theorem brouwer:
1.1951    fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
1.1952    assumes S: "compact S" "convex S" "S \<noteq> {}"
1.1953      and contf: "continuous_on S f"
1.1954 @@ -1858,9 +3482,11 @@
1.1955    qed
1.1956  qed
1.1957
1.1958 +subsection \<open>Applications\<close>
1.1959 +
1.1960  text \<open>So we get the no-retraction theorem.\<close>
1.1961
1.1962 -theorem no_retraction_cball:
1.1963 +corollary no_retraction_cball:
1.1964    fixes a :: "'a::euclidean_space"
1.1965    assumes "e > 0"
1.1966    shows "\<not> (frontier (cball a e) retract_of (cball a e))"
1.1967 @@ -1900,7 +3526,7 @@
1.1968      using continuous_on_const less_eq_real_def by auto
1.1969  qed
1.1970
1.1971 -lemma connected_sphere_eq:
1.1972 +corollary connected_sphere_eq:
1.1973    fixes a :: "'a :: euclidean_space"
1.1974    shows "connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
1.1975      (is "?lhs = ?rhs")
1.1976 @@ -1934,7 +3560,7 @@
1.1977    qed
1.1978  qed
1.1979
1.1980 -lemma path_connected_sphere_eq:
1.1981 +corollary path_connected_sphere_eq:
1.1982    fixes a :: "'a :: euclidean_space"
1.1983    shows "path_connected(sphere a r) \<longleftrightarrow> 2 \<le> DIM('a) \<or> r \<le> 0"
1.1984           (is "?lhs = ?rhs")
1.1985 @@ -1998,309 +3624,9 @@
1.1986    ultimately show False by simp
1.1987  qed
1.1988
1.1989 -subsection\<open>More Properties of Retractions\<close>
1.1990 -
1.1991 -lemma retraction:
1.1992 -   "retraction S T r \<longleftrightarrow>
1.1993 -    T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
1.1994 -by (force simp: retraction_def)
1.1995 -
1.1996 -lemma retract_of_imp_extensible:
1.1997 -  assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
1.1998 -  obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.1999 -using assms
1.2000 -apply (clarsimp simp add: retract_of_def retraction)
1.2001 -apply (rule_tac g = "f \<circ> r" in that)
1.2002 -apply (auto simp: continuous_on_compose2)
1.2003 -done
1.2004 -
1.2005 -lemma idempotent_imp_retraction:
1.2006 -  assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
1.2007 -    shows "retraction S (f ` S) f"
1.2008 -by (simp add: assms retraction)
1.2009 -
1.2010 -lemma retraction_subset:
1.2011 -  assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
1.2012 -  shows "retraction s' T r"
1.2013 -  unfolding retraction_def
1.2014 -  by (metis assms continuous_on_subset image_mono retraction)
1.2015 -
1.2016 -lemma retract_of_subset:
1.2017 -  assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
1.2018 -    shows "T retract_of s'"
1.2019 -by (meson assms retract_of_def retraction_subset)
1.2020 -
1.2021 -lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
1.2022 -by (simp add: continuous_on_id retraction)
1.2023 -
1.2024 -lemma retract_of_refl [iff]: "S retract_of S"
1.2025 -  unfolding retract_of_def retraction_def
1.2026 -  using continuous_on_id by blast
1.2027 -
1.2028 -lemma retract_of_imp_subset:
1.2029 -   "S retract_of T \<Longrightarrow> S \<subseteq> T"
1.2030 -by (simp add: retract_of_def retraction_def)
1.2031 -
1.2032 -lemma retract_of_empty [simp]:
1.2033 -     "({} retract_of S) \<longleftrightarrow> S = {}"  "(S retract_of {}) \<longleftrightarrow> S = {}"
1.2034 -by (auto simp: retract_of_def retraction_def)
1.2035 -
1.2036 -lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
1.2037 -  unfolding retract_of_def retraction_def by force
1.2038 -
1.2039 -lemma retraction_comp:
1.2040 -   "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
1.2041 -        \<Longrightarrow> retraction S U (g \<circ> f)"
1.2042 -apply (auto simp: retraction_def intro: continuous_on_compose2)
1.2043 -by blast
1.2044 -
1.2045 -lemma retract_of_trans [trans]:
1.2046 -  assumes "S retract_of T" and "T retract_of U"
1.2047 -    shows "S retract_of U"
1.2048 -using assms by (auto simp: retract_of_def intro: retraction_comp)
1.2049 -
1.2050 -lemma closedin_retract:
1.2051 -  fixes S :: "'a :: real_normed_vector set"
1.2052 -  assumes "S retract_of T"
1.2053 -    shows "closedin (subtopology euclidean T) S"
1.2054 -proof -
1.2055 -  obtain r where "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
1.2056 -    using assms by (auto simp: retract_of_def retraction_def)
1.2057 -  then have S: "S = {x \<in> T. (norm(r x - x)) = 0}" by auto
1.2058 -  show ?thesis
1.2059 -    apply (subst S)
1.2060 -    apply (rule continuous_closedin_preimage_constant)
1.2061 -    by (simp add: \<open>continuous_on T r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
1.2062 -qed
1.2063 -
1.2064 -lemma closedin_self [simp]:
1.2065 -    fixes S :: "'a :: real_normed_vector set"
1.2066 -    shows "closedin (subtopology euclidean S) S"
1.2067 -  by (simp add: closedin_retract)
1.2068 -
1.2069 -lemma retract_of_contractible:
1.2070 -  assumes "contractible T" "S retract_of T"
1.2071 -    shows "contractible S"
1.2072 -using assms
1.2073 -apply (clarsimp simp add: retract_of_def contractible_def retraction_def homotopic_with)
1.2074 -apply (rule_tac x="r a" in exI)
1.2075 -apply (rule_tac x="r \<circ> h" in exI)
1.2076 -apply (intro conjI continuous_intros continuous_on_compose)
1.2077 -apply (erule continuous_on_subset | force)+
1.2078 -done
1.2079 -
1.2080 -lemma retract_of_compact:
1.2081 -     "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
1.2082 -  by (metis compact_continuous_image retract_of_def retraction)
1.2083 -
1.2084 -lemma retract_of_closed:
1.2085 -    fixes S :: "'a :: real_normed_vector set"
1.2086 -    shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
1.2087 -  by (metis closedin_retract closedin_closed_eq)
1.2088 -
1.2089 -lemma retract_of_connected:
1.2090 -    "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
1.2091 -  by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
1.2092 -
1.2093 -lemma retract_of_path_connected:
1.2094 -    "\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
1.2095 -  by (metis path_connected_continuous_image retract_of_def retraction)
1.2096 -
1.2097 -lemma retract_of_simply_connected:
1.2098 -    "\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
1.2099 -apply (simp add: retract_of_def retraction_def, clarify)
1.2100 -apply (rule simply_connected_retraction_gen)
1.2101 -apply (force simp: continuous_on_id elim!: continuous_on_subset)+
1.2102 -done
1.2103 -
1.2104 -lemma retract_of_homotopically_trivial:
1.2105 -  assumes ts: "T retract_of S"
1.2106 -      and hom: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
1.2107 -                       continuous_on U g; g ` U \<subseteq> S\<rbrakk>
1.2108 -                       \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
1.2109 -      and "continuous_on U f" "f ` U \<subseteq> T"
1.2110 -      and "continuous_on U g" "g ` U \<subseteq> T"
1.2111 -    shows "homotopic_with (\<lambda>x. True) U T f g"
1.2112 -proof -
1.2113 -  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
1.2114 -    using ts by (auto simp: retract_of_def retraction)
1.2115 -  then obtain k where "Retracts S r T k"
1.2116 -    unfolding Retracts_def
1.2117 -    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
1.2118 -  then show ?thesis
1.2119 -    apply (rule Retracts.homotopically_trivial_retraction_gen)
1.2120 -    using assms
1.2121 -    apply (force simp: hom)+
1.2122 -    done
1.2123 -qed
1.2124 -
1.2125 -lemma retract_of_homotopically_trivial_null:
1.2126 -  assumes ts: "T retract_of S"
1.2127 -      and hom: "\<And>f. \<lbrakk>continuous_on U f; f ` U \<subseteq> S\<rbrakk>
1.2128 -                     \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) U S f (\<lambda>x. c)"
1.2129 -      and "continuous_on U f" "f ` U \<subseteq> T"
1.2130 -  obtains c where "homotopic_with (\<lambda>x. True) U T f (\<lambda>x. c)"
1.2131 -proof -
1.2132 -  obtain r where "r ` S \<subseteq> S" "continuous_on S r" "\<forall>x\<in>S. r (r x) = r x" "T = r ` S"
1.2133 -    using ts by (auto simp: retract_of_def retraction)
1.2134 -  then obtain k where "Retracts S r T k"
1.2135 -    unfolding Retracts_def
1.2136 -    by (metis continuous_on_subset dual_order.trans image_iff image_mono)
1.2137 -  then show ?thesis
1.2138 -    apply (rule Retracts.homotopically_trivial_retraction_null_gen)
1.2139 -    apply (rule TrueI refl assms that | assumption)+
1.2140 -    done
1.2141 -qed
1.2142 -
1.2143 -lemma retraction_imp_quotient_map:
1.2144 -   "retraction S T r
1.2145 -    \<Longrightarrow> U \<subseteq> T
1.2146 -            \<Longrightarrow> (openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow>
1.2147 -                 openin (subtopology euclidean T) U)"
1.2148 -apply (clarsimp simp add: retraction)
1.2149 -apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
1.2150 -apply (auto simp: elim: continuous_on_subset)
1.2151 -done
1.2152 -
1.2153 -lemma retract_of_locally_compact:
1.2154 -    fixes S :: "'a :: {heine_borel,real_normed_vector} set"
1.2155 -    shows  "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T"
1.2156 -  by (metis locally_compact_closedin closedin_retract)
1.2157 -
1.2158 -lemma retract_of_Times:
1.2159 -   "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
1.2160 -apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
1.2161 -apply (rename_tac f g)
1.2162 -apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
1.2163 -apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
1.2164 -done
1.2165 -
1.2166 -lemma homotopic_into_retract:
1.2167 -   "\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
1.2168 -        \<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
1.2169 -apply (subst (asm) homotopic_with_def)
1.2170 -apply (simp add: homotopic_with retract_of_def retraction_def, clarify)
1.2171 -apply (rule_tac x="r \<circ> h" in exI)
1.2172 -apply (rule conjI continuous_intros | erule continuous_on_subset | force simp: image_subset_iff)+
1.2173 -done
1.2174 -
1.2175 -lemma retract_of_locally_connected:
1.2176 -  assumes "locally connected T" "S retract_of T"
1.2177 -    shows "locally connected S"
1.2178 -  using assms
1.2179 -  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image)
1.2180 -
1.2181 -lemma retract_of_locally_path_connected:
1.2182 -  assumes "locally path_connected T" "S retract_of T"
1.2183 -    shows "locally path_connected S"
1.2184 -  using assms
1.2185 -  by (auto simp: retract_of_def retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image)
1.2186 -
1.2187 -subsubsection\<open>A few simple lemmas about deformation retracts\<close>
1.2188 -
1.2189 -lemma deformation_retract_imp_homotopy_eqv:
1.2190 -  fixes S :: "'a::euclidean_space set"
1.2191 -  assumes "homotopic_with (\<lambda>x. True) S S id r" and r: "retraction S T r"
1.2192 -  shows "S homotopy_eqv T"
1.2193 -proof -
1.2194 -  have "homotopic_with (\<lambda>x. True) S S (id \<circ> r) id"
1.2195 -    by (simp add: assms(1) homotopic_with_symD)
1.2196 -  moreover have "homotopic_with (\<lambda>x. True) T T (r \<circ> id) id"
1.2197 -    using r unfolding retraction_def
1.2198 -    by (metis (no_types, lifting) comp_id continuous_on_id' homotopic_with_equal homotopic_with_symD id_def image_id order_refl)
1.2199 -  ultimately
1.2200 -  show ?thesis
1.2201 -    unfolding homotopy_eqv_def
1.2202 -    by (metis continuous_on_id' id_def image_id r retraction_def)
1.2203 -qed
1.2204 -
1.2205 -lemma deformation_retract:
1.2206 -  fixes S :: "'a::euclidean_space set"
1.2207 -    shows "(\<exists>r. homotopic_with (\<lambda>x. True) S S id r \<and> retraction S T r) \<longleftrightarrow>
1.2208 -           T retract_of S \<and> (\<exists>f. homotopic_with (\<lambda>x. True) S S id f \<and> f ` S \<subseteq> T)"
1.2209 -    (is "?lhs = ?rhs")
1.2210 -proof
1.2211 -  assume ?lhs
1.2212 -  then show ?rhs
1.2213 -    by (auto simp: retract_of_def retraction_def)
1.2214 -next
1.2215 -  assume ?rhs
1.2216 -  then show ?lhs
1.2217 -    apply (clarsimp simp add: retract_of_def retraction_def)
1.2218 -    apply (rule_tac x=r in exI, simp)
1.2219 -     apply (rule homotopic_with_trans, assumption)
1.2220 -     apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
1.2221 -        apply (rule_tac Y=S in homotopic_compose_continuous_left)
1.2222 -         apply (auto simp: homotopic_with_sym)
1.2223 -    done
1.2224 -qed
1.2225 -
1.2226 -lemma deformation_retract_of_contractible_sing:
1.2227 -  fixes S :: "'a::euclidean_space set"
1.2228 -  assumes "contractible S" "a \<in> S"
1.2229 -  obtains r where "homotopic_with (\<lambda>x. True) S S id r" "retraction S {a} r"
1.2230 -proof -
1.2231 -  have "{a} retract_of S"
1.2232 -    by (simp add: \<open>a \<in> S\<close>)
1.2233 -  moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
1.2234 -      using assms
1.2235 -      by (auto simp: contractible_def continuous_on_const continuous_on_id homotopic_into_contractible image_subset_iff)
1.2236 -  moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
1.2237 -    by (simp add: image_subsetI)
1.2238 -  ultimately show ?thesis
1.2239 -    using that deformation_retract  by metis
1.2240 -qed
1.2241 -
1.2242 -
1.2243 -subsection\<open>Punctured affine hulls, etc\<close>
1.2244 -
1.2245 -lemma continuous_on_compact_surface_projection_aux:
1.2246 -  fixes S :: "'a::t2_space set"
1.2247 -  assumes "compact S" "S \<subseteq> T" "image q T \<subseteq> S"
1.2248 -      and contp: "continuous_on T p"
1.2249 -      and "\<And>x. x \<in> S \<Longrightarrow> q x = x"
1.2250 -      and [simp]: "\<And>x. x \<in> T \<Longrightarrow> q(p x) = q x"
1.2251 -      and "\<And>x. x \<in> T \<Longrightarrow> p(q x) = p x"
1.2252 -    shows "continuous_on T q"
1.2253 -proof -
1.2254 -  have *: "image p T = image p S"
1.2255 -    using assms by auto (metis imageI subset_iff)
1.2256 -  have contp': "continuous_on S p"
1.2257 -    by (rule continuous_on_subset [OF contp \<open>S \<subseteq> T\<close>])
1.2258 -  have "continuous_on (p ` T) q"
1.2259 -    by (simp add: "*" assms(1) assms(2) assms(5) continuous_on_inv contp' rev_subsetD)
1.2260 -  then have "continuous_on T (q \<circ> p)"
1.2261 -    by (rule continuous_on_compose [OF contp])
1.2262 -  then show ?thesis
1.2263 -    by (rule continuous_on_eq [of _ "q \<circ> p"]) (simp add: o_def)
1.2264 -qed
1.2265 -
1.2266 -lemma continuous_on_compact_surface_projection:
1.2267 -  fixes S :: "'a::real_normed_vector set"
1.2268 -  assumes "compact S"
1.2269 -      and S: "S \<subseteq> V - {0}" and "cone V"
1.2270 -      and iff: "\<And>x k. x \<in> V - {0} \<Longrightarrow> 0 < k \<and> (k *\<^sub>R x) \<in> S \<longleftrightarrow> d x = k"
1.2271 -  shows "continuous_on (V - {0}) (\<lambda>x. d x *\<^sub>R x)"
1.2272 -proof (rule continuous_on_compact_surface_projection_aux [OF \<open>compact S\<close> S])
1.2273 -  show "(\<lambda>x. d x *\<^sub>R x) ` (V - {0}) \<subseteq> S"
1.2274 -    using iff by auto
1.2275 -  show "continuous_on (V - {0}) (\<lambda>x. inverse(norm x) *\<^sub>R x)"
1.2276 -    by (intro continuous_intros) force
1.2277 -  show "\<And>x. x \<in> S \<Longrightarrow> d x *\<^sub>R x = x"
1.2278 -    by (metis S zero_less_one local.iff scaleR_one subset_eq)
1.2279 -  show "d (x /\<^sub>R norm x) *\<^sub>R (x /\<^sub>R norm x) = d x *\<^sub>R x" if "x \<in> V - {0}" for x
1.2280 -    using iff [of "inverse(norm x) *\<^sub>R x" "norm x * d x", symmetric] iff that \<open>cone V\<close>
1.2281 -    by (simp add: field_simps cone_def zero_less_mult_iff)
1.2282 -  show "d x *\<^sub>R x /\<^sub>R norm (d x *\<^sub>R x) = x /\<^sub>R norm x" if "x \<in> V - {0}" for x
1.2283 -  proof -
1.2284 -    have "0 < d x"
1.2285 -      using local.iff that by blast
1.2286 -    then show ?thesis
1.2287 -      by simp
1.2288 -  qed
1.2289 -qed
1.2290 -
1.2291 -proposition rel_frontier_deformation_retract_of_punctured_convex:
1.2292 +subsubsection \<open>Punctured affine hulls, etc\<close>
1.2293 +
1.2294 +lemma rel_frontier_deformation_retract_of_punctured_convex:
1.2295    fixes S :: "'a::euclidean_space set"
1.2296    assumes "convex S" "convex T" "bounded S"
1.2297        and arelS: "a \<in> rel_interior S"
1.2298 @@ -2502,7 +3828,7 @@
1.2299    shows "connected(rel_frontier S)"
1.2300    by (simp add: assms path_connected_imp_connected path_connected_sphere_gen)
1.2301
1.2302 -subsection\<open>Borsuk-style characterization of separation\<close>
1.2303 +subsubsection\<open>Borsuk-style characterization of separation\<close>
1.2304
1.2305  lemma continuous_on_Borsuk_map:
1.2306     "a \<notin> s \<Longrightarrow>  continuous_on s (\<lambda>x. inverse(norm (x - a)) *\<^sub>R (x - a))"
1.2307 @@ -2595,1327 +3921,7 @@
1.2308      by blast
1.2309  qed
1.2310
1.2311 -subsection\<open>Absolute retracts, etc\<close>
1.2312 -
1.2313 -text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
1.2314 - Euclidean neighbourhood retracts (ENR). We define AR and ANR by
1.2315 - specializing the standard definitions for a set to embedding in
1.2316 -spaces of higher dimension. \<close>
1.2317 -
1.2318 -(*This turns out to be sufficient (since any set in
1.2319 -R^n can be embedded as a closed subset of a convex subset of R^{n+1}) to
1.2320 -derive the usual definitions, but we need to split them into two
1.2321 -implications because of the lack of type quantifiers. Then ENR turns out
1.2322 -to be equivalent to ANR plus local compactness. -- JRH*)
1.2323 -
1.2324 -definition AR :: "'a::topological_space set => bool"
1.2325 -  where
1.2326 -   "AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
1.2327 -                \<longrightarrow> S' retract_of U"
1.2328 -
1.2329 -definition ANR :: "'a::topological_space set => bool"
1.2330 -  where
1.2331 -   "ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
1.2332 -                \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and>
1.2333 -                        S' retract_of T)"
1.2334 -
1.2335 -definition ENR :: "'a::topological_space set => bool"
1.2336 -  where "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
1.2337 -
1.2338 -text\<open> First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
1.2339 -
1.2340 -proposition AR_imp_absolute_extensor:
1.2341 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.2342 -  assumes "AR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
1.2343 -      and cloUT: "closedin (subtopology euclidean U) T"
1.2344 -  obtains g where "continuous_on U g" "g ` U \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
1.2345 -proof -
1.2346 -  have "aff_dim S < int (DIM('b \<times> real))"
1.2347 -    using aff_dim_le_DIM [of S] by simp
1.2348 -  then obtain C and S' :: "('b * real) set"
1.2349 -          where C: "convex C" "C \<noteq> {}"
1.2350 -            and cloCS: "closedin (subtopology euclidean C) S'"
1.2351 -            and hom: "S homeomorphic S'"
1.2352 -    by (metis that homeomorphic_closedin_convex)
1.2353 -  then have "S' retract_of C"
1.2354 -    using \<open>AR S\<close> by (simp add: AR_def)
1.2355 -  then obtain r where "S' \<subseteq> C" and contr: "continuous_on C r"
1.2356 -                  and "r ` C \<subseteq> S'" and rid: "\<And>x. x\<in>S' \<Longrightarrow> r x = x"
1.2357 -    by (auto simp: retraction_def retract_of_def)
1.2358 -  obtain g h where "homeomorphism S S' g h"
1.2359 -    using hom by (force simp: homeomorphic_def)
1.2360 -  then have "continuous_on (f ` T) g"
1.2361 -    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
1.2362 -  then have contgf: "continuous_on T (g \<circ> f)"
1.2363 -    by (metis continuous_on_compose contf)
1.2364 -  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
1.2365 -  proof -
1.2366 -    have "g ` S = S'"
1.2367 -      by (metis (no_types) \<open>homeomorphism S S' g h\<close> homeomorphism_def)
1.2368 -    with \<open>S' \<subseteq> C\<close> \<open>f ` T \<subseteq> S\<close> show ?thesis by force
1.2369 -  qed
1.2370 -  obtain f' where f': "continuous_on U f'"  "f' ` U \<subseteq> C"
1.2371 -                      "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
1.2372 -    by (metis Dugundji [OF C cloUT contgf gfTC])
1.2373 -  show ?thesis
1.2374 -  proof (rule_tac g = "h \<circ> r \<circ> f'" in that)
1.2375 -    show "continuous_on U (h \<circ> r \<circ> f')"
1.2376 -      apply (intro continuous_on_compose f')
1.2377 -       using continuous_on_subset contr f' apply blast
1.2378 -      by (meson \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> continuous_on_subset \<open>f' ` U \<subseteq> C\<close> homeomorphism_def image_mono)
1.2379 -    show "(h \<circ> r \<circ> f') ` U \<subseteq> S"
1.2380 -      using \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> \<open>f' ` U \<subseteq> C\<close>
1.2381 -      by (fastforce simp: homeomorphism_def)
1.2382 -    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
1.2383 -      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> f'
1.2384 -      by (auto simp: rid homeomorphism_def)
1.2385 -  qed
1.2386 -qed
1.2387 -
1.2388 -lemma AR_imp_absolute_retract:
1.2389 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2390 -  assumes "AR S" "S homeomorphic S'"
1.2391 -      and clo: "closedin (subtopology euclidean U) S'"
1.2392 -    shows "S' retract_of U"
1.2393 -proof -
1.2394 -  obtain g h where hom: "homeomorphism S S' g h"
1.2395 -    using assms by (force simp: homeomorphic_def)
1.2396 -  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
1.2397 -    using hom homeomorphism_def apply blast
1.2398 -    apply (metis hom equalityE homeomorphism_def)
1.2399 -    done
1.2400 -  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
1.2401 -              and h'h: "\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
1.2402 -    by (blast intro: AR_imp_absolute_extensor [OF \<open>AR S\<close> h clo])
1.2403 -  have [simp]: "S' \<subseteq> U" using clo closedin_limpt by blast
1.2404 -  show ?thesis
1.2405 -  proof (simp add: retraction_def retract_of_def, intro exI conjI)
1.2406 -    show "continuous_on U (g \<circ> h')"
1.2407 -      apply (intro continuous_on_compose h')
1.2408 -      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.2409 -      done
1.2410 -    show "(g \<circ> h') ` U \<subseteq> S'"
1.2411 -      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.2412 -    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
1.2413 -      by clarsimp (metis h'h hom homeomorphism_def)
1.2414 -  qed
1.2415 -qed
1.2416 -
1.2417 -lemma AR_imp_absolute_retract_UNIV:
1.2418 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2419 -  assumes "AR S" and hom: "S homeomorphic S'"
1.2420 -      and clo: "closed S'"
1.2421 -    shows "S' retract_of UNIV"
1.2422 -apply (rule AR_imp_absolute_retract [OF \<open>AR S\<close> hom])
1.2423 -using clo closed_closedin by auto
1.2424 -
1.2425 -lemma absolute_extensor_imp_AR:
1.2426 -  fixes S :: "'a::euclidean_space set"
1.2427 -  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
1.2428 -           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
1.2429 -                  closedin (subtopology euclidean U) T\<rbrakk>
1.2430 -                 \<Longrightarrow> \<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
1.2431 -  shows "AR S"
1.2432 -proof (clarsimp simp: AR_def)
1.2433 -  fix U and T :: "('a * real) set"
1.2434 -  assume "S homeomorphic T" and clo: "closedin (subtopology euclidean U) T"
1.2435 -  then obtain g h where hom: "homeomorphism S T g h"
1.2436 -    by (force simp: homeomorphic_def)
1.2437 -  have h: "continuous_on T h" " h ` T \<subseteq> S"
1.2438 -    using hom homeomorphism_def apply blast
1.2439 -    apply (metis hom equalityE homeomorphism_def)
1.2440 -    done
1.2441 -  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
1.2442 -              and h'h: "\<forall>x\<in>T. h' x = h x"
1.2443 -    using assms [OF h clo] by blast
1.2444 -  have [simp]: "T \<subseteq> U"
1.2445 -    using clo closedin_imp_subset by auto
1.2446 -  show "T retract_of U"
1.2447 -  proof (simp add: retraction_def retract_of_def, intro exI conjI)
1.2448 -    show "continuous_on U (g \<circ> h')"
1.2449 -      apply (intro continuous_on_compose h')
1.2450 -      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.2451 -      done
1.2452 -    show "(g \<circ> h') ` U \<subseteq> T"
1.2453 -      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.2454 -    show "\<forall>x\<in>T. (g \<circ> h') x = x"
1.2455 -      by clarsimp (metis h'h hom homeomorphism_def)
1.2456 -  qed
1.2457 -qed
1.2458 -
1.2459 -lemma AR_eq_absolute_extensor:
1.2460 -  fixes S :: "'a::euclidean_space set"
1.2461 -  shows "AR S \<longleftrightarrow>
1.2462 -       (\<forall>f :: 'a * real \<Rightarrow> 'a.
1.2463 -        \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
1.2464 -               closedin (subtopology euclidean U) T \<longrightarrow>
1.2465 -                (\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
1.2466 -apply (rule iffI)
1.2467 - apply (metis AR_imp_absolute_extensor)
1.2469 -done
1.2470 -
1.2471 -lemma AR_imp_retract:
1.2472 -  fixes S :: "'a::euclidean_space set"
1.2473 -  assumes "AR S \<and> closedin (subtopology euclidean U) S"
1.2474 -    shows "S retract_of U"
1.2475 -using AR_imp_absolute_retract assms homeomorphic_refl by blast
1.2476 -
1.2477 -lemma AR_homeomorphic_AR:
1.2478 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.2479 -  assumes "AR T" "S homeomorphic T"
1.2480 -    shows "AR S"
1.2481 -unfolding AR_def
1.2482 -by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym)
1.2483 -
1.2484 -lemma homeomorphic_AR_iff_AR:
1.2485 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.2486 -  shows "S homeomorphic T \<Longrightarrow> AR S \<longleftrightarrow> AR T"
1.2487 -by (metis AR_homeomorphic_AR homeomorphic_sym)
1.2488 -
1.2489 -
1.2490 -proposition ANR_imp_absolute_neighbourhood_extensor:
1.2491 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.2492 -  assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
1.2493 -      and cloUT: "closedin (subtopology euclidean U) T"
1.2494 -  obtains V g where "T \<subseteq> V" "openin (subtopology euclidean U) V"
1.2495 -                    "continuous_on V g"
1.2496 -                    "g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
1.2497 -proof -
1.2498 -  have "aff_dim S < int (DIM('b \<times> real))"
1.2499 -    using aff_dim_le_DIM [of S] by simp
1.2500 -  then obtain C and S' :: "('b * real) set"
1.2501 -          where C: "convex C" "C \<noteq> {}"
1.2502 -            and cloCS: "closedin (subtopology euclidean C) S'"
1.2503 -            and hom: "S homeomorphic S'"
1.2504 -    by (metis that homeomorphic_closedin_convex)
1.2505 -  then obtain D where opD: "openin (subtopology euclidean C) D" and "S' retract_of D"
1.2506 -    using \<open>ANR S\<close> by (auto simp: ANR_def)
1.2507 -  then obtain r where "S' \<subseteq> D" and contr: "continuous_on D r"
1.2508 -                  and "r ` D \<subseteq> S'" and rid: "\<And>x. x \<in> S' \<Longrightarrow> r x = x"
1.2509 -    by (auto simp: retraction_def retract_of_def)
1.2510 -  obtain g h where homgh: "homeomorphism S S' g h"
1.2511 -    using hom by (force simp: homeomorphic_def)
1.2512 -  have "continuous_on (f ` T) g"
1.2513 -    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
1.2514 -  then have contgf: "continuous_on T (g \<circ> f)"
1.2515 -    by (intro continuous_on_compose contf)
1.2516 -  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
1.2517 -  proof -
1.2518 -    have "g ` S = S'"
1.2519 -      by (metis (no_types) homeomorphism_def homgh)
1.2520 -    then show ?thesis
1.2521 -      by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology)
1.2522 -  qed
1.2523 -  obtain f' where contf': "continuous_on U f'"
1.2524 -              and "f' ` U \<subseteq> C"
1.2525 -              and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
1.2526 -    by (metis Dugundji [OF C cloUT contgf gfTC])
1.2527 -  show ?thesis
1.2528 -  proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
1.2529 -    show "T \<subseteq> U \<inter> f' -` D"
1.2530 -      using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
1.2531 -      by fastforce
1.2532 -    show ope: "openin (subtopology euclidean U) (U \<inter> f' -` D)"
1.2533 -      using  \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
1.2534 -    have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
1.2535 -      apply (rule continuous_on_subset [of S'])
1.2536 -      using homeomorphism_def homgh apply blast
1.2537 -      using \<open>r ` D \<subseteq> S'\<close> by blast
1.2538 -    show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
1.2539 -      apply (intro continuous_on_compose conth
1.2540 -                   continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
1.2541 -      done
1.2542 -    show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
1.2543 -      using \<open>homeomorphism S S' g h\<close>  \<open>f' ` U \<subseteq> C\<close>  \<open>r ` D \<subseteq> S'\<close>
1.2544 -      by (auto simp: homeomorphism_def)
1.2545 -    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
1.2546 -      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> eq
1.2547 -      by (auto simp: rid homeomorphism_def)
1.2548 -  qed
1.2549 -qed
1.2550 -
1.2551 -
1.2552 -corollary ANR_imp_absolute_neighbourhood_retract:
1.2553 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2554 -  assumes "ANR S" "S homeomorphic S'"
1.2555 -      and clo: "closedin (subtopology euclidean U) S'"
1.2556 -  obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
1.2557 -proof -
1.2558 -  obtain g h where hom: "homeomorphism S S' g h"
1.2559 -    using assms by (force simp: homeomorphic_def)
1.2560 -  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
1.2561 -    using hom homeomorphism_def apply blast
1.2562 -    apply (metis hom equalityE homeomorphism_def)
1.2563 -    done
1.2564 -    from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
1.2565 -  obtain V h' where "S' \<subseteq> V" and opUV: "openin (subtopology euclidean U) V"
1.2566 -                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
1.2567 -                and h'h:"\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
1.2568 -    by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
1.2569 -  have "S' retract_of V"
1.2570 -  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
1.2571 -    show "continuous_on V (g \<circ> h')"
1.2572 -      apply (intro continuous_on_compose h')
1.2573 -      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.2574 -      done
1.2575 -    show "(g \<circ> h') ` V \<subseteq> S'"
1.2576 -      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.2577 -    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
1.2578 -      by clarsimp (metis h'h hom homeomorphism_def)
1.2579 -  qed
1.2580 -  then show ?thesis
1.2581 -    by (rule that [OF opUV])
1.2582 -qed
1.2583 -
1.2584 -corollary ANR_imp_absolute_neighbourhood_retract_UNIV:
1.2585 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2586 -  assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'"
1.2587 -  obtains V where "open V" "S' retract_of V"
1.2588 -  using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
1.2589 -by (metis clo closed_closedin open_openin subtopology_UNIV)
1.2590 -
1.2591 -corollary neighbourhood_extension_into_ANR:
1.2592 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.2593 -  assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
1.2594 -  obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
1.2595 -                    "g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
1.2596 -  using ANR_imp_absolute_neighbourhood_extensor [OF  \<open>ANR T\<close> contf fim]
1.2597 -  by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
1.2598 -
1.2599 -lemma absolute_neighbourhood_extensor_imp_ANR:
1.2600 -  fixes S :: "'a::euclidean_space set"
1.2601 -  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
1.2602 -           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
1.2603 -                  closedin (subtopology euclidean U) T\<rbrakk>
1.2604 -                 \<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
1.2605 -                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
1.2606 -  shows "ANR S"
1.2607 -proof (clarsimp simp: ANR_def)
1.2608 -  fix U and T :: "('a * real) set"
1.2609 -  assume "S homeomorphic T" and clo: "closedin (subtopology euclidean U) T"
1.2610 -  then obtain g h where hom: "homeomorphism S T g h"
1.2611 -    by (force simp: homeomorphic_def)
1.2612 -  have h: "continuous_on T h" " h ` T \<subseteq> S"
1.2613 -    using hom homeomorphism_def apply blast
1.2614 -    apply (metis hom equalityE homeomorphism_def)
1.2615 -    done
1.2616 -  obtain V h' where "T \<subseteq> V" and opV: "openin (subtopology euclidean U) V"
1.2617 -                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
1.2618 -              and h'h: "\<forall>x\<in>T. h' x = h x"
1.2619 -    using assms [OF h clo] by blast
1.2620 -  have [simp]: "T \<subseteq> U"
1.2621 -    using clo closedin_imp_subset by auto
1.2622 -  have "T retract_of V"
1.2623 -  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
1.2624 -    show "continuous_on V (g \<circ> h')"
1.2625 -      apply (intro continuous_on_compose h')
1.2626 -      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
1.2627 -      done
1.2628 -    show "(g \<circ> h') ` V \<subseteq> T"
1.2629 -      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
1.2630 -    show "\<forall>x\<in>T. (g \<circ> h') x = x"
1.2631 -      by clarsimp (metis h'h hom homeomorphism_def)
1.2632 -  qed
1.2633 -  then show "\<exists>V. openin (subtopology euclidean U) V \<and> T retract_of V"
1.2634 -    using opV by blast
1.2635 -qed
1.2636 -
1.2637 -lemma ANR_eq_absolute_neighbourhood_extensor:
1.2638 -  fixes S :: "'a::euclidean_space set"
1.2639 -  shows "ANR S \<longleftrightarrow>
1.2640 -         (\<forall>f :: 'a * real \<Rightarrow> 'a.
1.2641 -          \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
1.2642 -                closedin (subtopology euclidean U) T \<longrightarrow>
1.2643 -               (\<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
1.2644 -                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
1.2645 -apply (rule iffI)
1.2646 - apply (metis ANR_imp_absolute_neighbourhood_extensor)
1.2648 -done
1.2649 -
1.2650 -lemma ANR_imp_neighbourhood_retract:
1.2651 -  fixes S :: "'a::euclidean_space set"
1.2652 -  assumes "ANR S" "closedin (subtopology euclidean U) S"
1.2653 -  obtains V where "openin (subtopology euclidean U) V" "S retract_of V"
1.2654 -using ANR_imp_absolute_neighbourhood_retract assms homeomorphic_refl by blast
1.2655 -
1.2656 -lemma ANR_imp_absolute_closed_neighbourhood_retract:
1.2657 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2658 -  assumes "ANR S" "S homeomorphic S'" and US': "closedin (subtopology euclidean U) S'"
1.2659 -  obtains V W
1.2660 -    where "openin (subtopology euclidean U) V"
1.2661 -          "closedin (subtopology euclidean U) W"
1.2662 -          "S' \<subseteq> V" "V \<subseteq> W" "S' retract_of W"
1.2663 -proof -
1.2664 -  obtain Z where "openin (subtopology euclidean U) Z" and S'Z: "S' retract_of Z"
1.2665 -    by (blast intro: assms ANR_imp_absolute_neighbourhood_retract)
1.2666 -  then have UUZ: "closedin (subtopology euclidean U) (U - Z)"
1.2667 -    by auto
1.2668 -  have "S' \<inter> (U - Z) = {}"
1.2669 -    using \<open>S' retract_of Z\<close> closedin_retract closedin_subtopology by fastforce
1.2670 -  then obtain V W
1.2671 -      where "openin (subtopology euclidean U) V"
1.2672 -        and "openin (subtopology euclidean U) W"
1.2673 -        and "S' \<subseteq> V" "U - Z \<subseteq> W" "V \<inter> W = {}"
1.2674 -      using separation_normal_local [OF US' UUZ]  by auto
1.2675 -  moreover have "S' retract_of U - W"
1.2676 -    apply (rule retract_of_subset [OF S'Z])
1.2677 -    using US' \<open>S' \<subseteq> V\<close> \<open>V \<inter> W = {}\<close> closedin_subset apply fastforce
1.2678 -    using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
1.2679 -  ultimately show ?thesis
1.2680 -    apply (rule_tac V=V and W = "U-W" in that)
1.2681 -    using openin_imp_subset apply force+
1.2682 -    done
1.2683 -qed
1.2684 -
1.2685 -lemma ANR_imp_closed_neighbourhood_retract:
1.2686 -  fixes S :: "'a::euclidean_space set"
1.2687 -  assumes "ANR S" "closedin (subtopology euclidean U) S"
1.2688 -  obtains V W where "openin (subtopology euclidean U) V"
1.2689 -                    "closedin (subtopology euclidean U) W"
1.2690 -                    "S \<subseteq> V" "V \<subseteq> W" "S retract_of W"
1.2691 -by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl)
1.2692 -
1.2693 -lemma ANR_homeomorphic_ANR:
1.2694 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.2695 -  assumes "ANR T" "S homeomorphic T"
1.2696 -    shows "ANR S"
1.2697 -unfolding ANR_def
1.2698 -by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym)
1.2699 -
1.2700 -lemma homeomorphic_ANR_iff_ANR:
1.2701 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.2702 -  shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
1.2703 -by (metis ANR_homeomorphic_ANR homeomorphic_sym)
1.2704 -
1.2705 -subsection\<open> Analogous properties of ENRs\<close>
1.2706 -
1.2707 -proposition ENR_imp_absolute_neighbourhood_retract:
1.2708 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2709 -  assumes "ENR S" and hom: "S homeomorphic S'"
1.2710 -      and "S' \<subseteq> U"
1.2711 -  obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
1.2712 -proof -
1.2713 -  obtain X where "open X" "S retract_of X"
1.2714 -    using \<open>ENR S\<close> by (auto simp: ENR_def)
1.2715 -  then obtain r where "retraction X S r"
1.2716 -    by (auto simp: retract_of_def)
1.2717 -  have "locally compact S'"
1.2718 -    using retract_of_locally_compact open_imp_locally_compact
1.2719 -          homeomorphic_local_compactness \<open>S retract_of X\<close> \<open>open X\<close> hom by blast
1.2720 -  then obtain W where UW: "openin (subtopology euclidean U) W"
1.2721 -                  and WS': "closedin (subtopology euclidean W) S'"
1.2722 -    apply (rule locally_compact_closedin_open)
1.2723 -    apply (rename_tac W)
1.2724 -    apply (rule_tac W = "U \<inter> W" in that, blast)
1.2725 -    by (simp add: \<open>S' \<subseteq> U\<close> closedin_limpt)
1.2726 -  obtain f g where hom: "homeomorphism S S' f g"
1.2727 -    using assms by (force simp: homeomorphic_def)
1.2728 -  have contg: "continuous_on S' g"
1.2729 -    using hom homeomorphism_def by blast
1.2730 -  moreover have "g ` S' \<subseteq> S" by (metis hom equalityE homeomorphism_def)
1.2731 -  ultimately obtain h where conth: "continuous_on W h" and hg: "\<And>x. x \<in> S' \<Longrightarrow> h x = g x"
1.2732 -    using Tietze_unbounded [of S' g W] WS' by blast
1.2733 -  have "W \<subseteq> U" using UW openin_open by auto
1.2734 -  have "S' \<subseteq> W" using WS' closedin_closed by auto
1.2735 -  have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
1.2736 -    by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
1.2737 -  have "S' retract_of (W \<inter> h -` X)"
1.2738 -  proof (simp add: retraction_def retract_of_def, intro exI conjI)
1.2739 -    show "S' \<subseteq> W" "S' \<subseteq> h -` X"
1.2740 -      using him WS' closedin_imp_subset by blast+
1.2741 -    show "continuous_on (W \<inter> h -` X) (f \<circ> r \<circ> h)"
1.2742 -    proof (intro continuous_on_compose)
1.2743 -      show "continuous_on (W \<inter> h -` X) h"
1.2744 -        by (meson conth continuous_on_subset inf_le1)
1.2745 -      show "continuous_on (h ` (W \<inter> h -` X)) r"
1.2746 -      proof -
1.2747 -        have "h ` (W \<inter> h -` X) \<subseteq> X"
1.2748 -          by blast
1.2749 -        then show "continuous_on (h ` (W \<inter> h -` X)) r"
1.2750 -          by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
1.2751 -      qed
1.2752 -      show "continuous_on (r ` h ` (W \<inter> h -` X)) f"
1.2753 -        apply (rule continuous_on_subset [of S])
1.2754 -         using hom homeomorphism_def apply blast
1.2755 -        apply clarify
1.2756 -        apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
1.2757 -        done
1.2758 -    qed
1.2759 -    show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
1.2760 -      using \<open>retraction X S r\<close> hom
1.2761 -      by (auto simp: retraction_def homeomorphism_def)
1.2762 -    show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
1.2763 -      using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
1.2764 -  qed
1.2765 -  then show ?thesis
1.2766 -    apply (rule_tac V = "W \<inter> h -` X" in that)
1.2767 -     apply (rule openin_trans [OF _ UW])
1.2768 -     using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
1.2769 -     done
1.2770 -qed
1.2771 -
1.2772 -corollary ENR_imp_absolute_neighbourhood_retract_UNIV:
1.2773 -  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
1.2774 -  assumes "ENR S" "S homeomorphic S'"
1.2775 -  obtains T' where "open T'" "S' retract_of T'"
1.2776 -by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV)
1.2777 -
1.2778 -lemma ENR_homeomorphic_ENR:
1.2779 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.2780 -  assumes "ENR T" "S homeomorphic T"
1.2781 -    shows "ENR S"
1.2782 -unfolding ENR_def
1.2783 -by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym)
1.2784 -
1.2785 -lemma homeomorphic_ENR_iff_ENR:
1.2786 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.2787 -  assumes "S homeomorphic T"
1.2788 -    shows "ENR S \<longleftrightarrow> ENR T"
1.2789 -by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)
1.2790 -
1.2791 -lemma ENR_translation:
1.2792 -  fixes S :: "'a::euclidean_space set"
1.2793 -  shows "ENR(image (\<lambda>x. a + x) S) \<longleftrightarrow> ENR S"
1.2794 -by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)
1.2795 -
1.2796 -lemma ENR_linear_image_eq:
1.2797 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.2798 -  assumes "linear f" "inj f"
1.2799 -  shows "ENR (image f S) \<longleftrightarrow> ENR S"
1.2800 -apply (rule homeomorphic_ENR_iff_ENR)
1.2801 -using assms homeomorphic_sym linear_homeomorphic_image by auto
1.2802 -
1.2803 -subsection\<open>Some relations among the concepts\<close>
1.2804 -
1.2805 -text\<open>We also relate AR to being a retract of UNIV, which is often a more convenient proxy in the closed case.\<close>
1.2806 -
1.2807 -lemma AR_imp_ANR: "AR S \<Longrightarrow> ANR S"
1.2808 -  using ANR_def AR_def by fastforce
1.2809 -
1.2810 -lemma ENR_imp_ANR:
1.2811 -  fixes S :: "'a::euclidean_space set"
1.2812 -  shows "ENR S \<Longrightarrow> ANR S"
1.2814 -by (metis ENR_imp_absolute_neighbourhood_retract closedin_imp_subset)
1.2815 -
1.2816 -lemma ENR_ANR:
1.2817 -  fixes S :: "'a::euclidean_space set"
1.2818 -  shows "ENR S \<longleftrightarrow> ANR S \<and> locally compact S"
1.2819 -proof
1.2820 -  assume "ENR S"
1.2821 -  then have "locally compact S"
1.2822 -    using ENR_def open_imp_locally_compact retract_of_locally_compact by auto
1.2823 -  then show "ANR S \<and> locally compact S"
1.2824 -    using ENR_imp_ANR \<open>ENR S\<close> by blast
1.2825 -next
1.2826 -  assume "ANR S \<and> locally compact S"
1.2827 -  then have "ANR S" "locally compact S" by auto
1.2828 -  then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T"
1.2829 -    using locally_compact_homeomorphic_closed
1.2830 -    by (metis DIM_prod DIM_real Suc_eq_plus1 lessI)
1.2831 -  then show "ENR S"
1.2832 -    using \<open>ANR S\<close>
1.2833 -    apply (simp add: ANR_def)
1.2834 -    apply (drule_tac x=UNIV in spec)
1.2835 -    apply (drule_tac x=T in spec, clarsimp)
1.2836 -    apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
1.2837 -    done
1.2838 -qed
1.2839 -
1.2840 -
1.2841 -proposition AR_ANR:
1.2842 -  fixes S :: "'a::euclidean_space set"
1.2843 -  shows "AR S \<longleftrightarrow> ANR S \<and> contractible S \<and> S \<noteq> {}"
1.2844 -        (is "?lhs = ?rhs")
1.2845 -proof
1.2846 -  assume ?lhs
1.2847 -  obtain C and S' :: "('a * real) set"
1.2848 -    where "convex C" "C \<noteq> {}" "closedin (subtopology euclidean C) S'" "S homeomorphic S'"
1.2849 -      apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"])
1.2850 -      using aff_dim_le_DIM [of S] by auto
1.2851 -  with \<open>AR S\<close> have "contractible S"
1.2852 -    apply (simp add: AR_def)
1.2853 -    apply (drule_tac x=C in spec)
1.2854 -    apply (drule_tac x="S'" in spec, simp)
1.2855 -    using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce
1.2856 -  with \<open>AR S\<close> show ?rhs
1.2857 -    apply (auto simp: AR_imp_ANR)
1.2858 -    apply (force simp: AR_def)
1.2859 -    done
1.2860 -next
1.2861 -  assume ?rhs
1.2862 -  then obtain a and h:: "real \<times> 'a \<Rightarrow> 'a"
1.2863 -      where conth: "continuous_on ({0..1} \<times> S) h"
1.2864 -        and hS: "h ` ({0..1} \<times> S) \<subseteq> S"
1.2865 -        and [simp]: "\<And>x. h(0, x) = x"
1.2866 -        and [simp]: "\<And>x. h(1, x) = a"
1.2867 -        and "ANR S" "S \<noteq> {}"
1.2868 -    by (auto simp: contractible_def homotopic_with_def)
1.2869 -  then have "a \<in> S"
1.2870 -    by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
1.2871 -  have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
1.2872 -         if      f: "continuous_on T f" "f ` T \<subseteq> S"
1.2873 -            and WT: "closedin (subtopology euclidean W) T"
1.2874 -         for W T and f :: "'a \<times> real \<Rightarrow> 'a"
1.2875 -  proof -
1.2876 -    obtain U g
1.2877 -      where "T \<subseteq> U" and WU: "openin (subtopology euclidean W) U"
1.2878 -        and contg: "continuous_on U g"
1.2879 -        and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
1.2880 -      using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, rule_format, OF f WT]
1.2881 -      by auto
1.2882 -    have WWU: "closedin (subtopology euclidean W) (W - U)"
1.2883 -      using WU closedin_diff by fastforce
1.2884 -    moreover have "(W - U) \<inter> T = {}"
1.2885 -      using \<open>T \<subseteq> U\<close> by auto
1.2886 -    ultimately obtain V V'
1.2887 -      where WV': "openin (subtopology euclidean W) V'"
1.2888 -        and WV: "openin (subtopology euclidean W) V"
1.2889 -        and "W - U \<subseteq> V'" "T \<subseteq> V" "V' \<inter> V = {}"
1.2890 -      using separation_normal_local [of W "W-U" T] WT by blast
1.2891 -    then have WVT: "T \<inter> (W - V) = {}"
1.2892 -      by auto
1.2893 -    have WWV: "closedin (subtopology euclidean W) (W - V)"
1.2894 -      using WV closedin_diff by fastforce
1.2895 -    obtain j :: " 'a \<times> real \<Rightarrow> real"
1.2896 -      where contj: "continuous_on W j"
1.2897 -        and j:  "\<And>x. x \<in> W \<Longrightarrow> j x \<in> {0..1}"
1.2898 -        and j0: "\<And>x. x \<in> W - V \<Longrightarrow> j x = 1"
1.2899 -        and j1: "\<And>x. x \<in> T \<Longrightarrow> j x = 0"
1.2900 -      by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
1.2901 -    have Weq: "W = (W - V) \<union> (W - V')"
1.2902 -      using \<open>V' \<inter> V = {}\<close> by force
1.2903 -    show ?thesis
1.2904 -    proof (intro conjI exI)
1.2905 -      have *: "continuous_on (W - V') (\<lambda>x. h (j x, g x))"
1.2906 -        apply (rule continuous_on_compose2 [OF conth continuous_on_Pair])
1.2907 -          apply (rule continuous_on_subset [OF contj Diff_subset])
1.2908 -         apply (rule continuous_on_subset [OF contg])
1.2909 -         apply (metis Diff_subset_conv Un_commute \<open>W - U \<subseteq> V'\<close>)
1.2910 -        using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> apply fastforce
1.2911 -        done
1.2912 -      show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
1.2913 -        apply (subst Weq)
1.2914 -        apply (rule continuous_on_cases_local)
1.2915 -            apply (simp_all add: Weq [symmetric] WWV continuous_on_const *)
1.2916 -          using WV' closedin_diff apply fastforce
1.2917 -         apply (auto simp: j0 j1)
1.2918 -        done
1.2919 -    next
1.2920 -      have "h (j (x, y), g (x, y)) \<in> S" if "(x, y) \<in> W" "(x, y) \<in> V" for x y
1.2921 -      proof -
1.2922 -        have "j(x, y) \<in> {0..1}"
1.2923 -          using j that by blast
1.2924 -        moreover have "g(x, y) \<in> S"
1.2925 -          using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
1.2926 -        ultimately show ?thesis
1.2927 -          using hS by blast
1.2928 -      qed
1.2929 -      with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
1.2930 -      show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"
1.2931 -        by auto
1.2932 -    next
1.2933 -      show "\<forall>x\<in>T. (if x \<in> W - V then a else h (j x, g x)) = f x"
1.2934 -        using \<open>T \<subseteq> V\<close> by (auto simp: j0 j1 gf)
1.2935 -    qed
1.2936 -  qed
1.2937 -  then show ?lhs
1.2938 -    by (simp add: AR_eq_absolute_extensor)
1.2939 -qed
1.2940 -
1.2941 -
1.2942 -lemma ANR_retract_of_ANR:
1.2943 -  fixes S :: "'a::euclidean_space set"
1.2944 -  assumes "ANR T" "S retract_of T"
1.2945 -  shows "ANR S"
1.2946 -using assms
1.2947 -apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def)
1.2948 -apply (clarsimp elim!: all_forward)
1.2949 -apply (erule impCE, metis subset_trans)
1.2950 -apply (clarsimp elim!: ex_forward)
1.2951 -apply (rule_tac x="r \<circ> g" in exI)
1.2952 -by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans)
1.2953 -
1.2954 -lemma AR_retract_of_AR:
1.2955 -  fixes S :: "'a::euclidean_space set"
1.2956 -  shows "\<lbrakk>AR T; S retract_of T\<rbrakk> \<Longrightarrow> AR S"
1.2957 -using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce
1.2958 -
1.2959 -lemma ENR_retract_of_ENR:
1.2960 -   "\<lbrakk>ENR T; S retract_of T\<rbrakk> \<Longrightarrow> ENR S"
1.2961 -by (meson ENR_def retract_of_trans)
1.2962 -
1.2963 -lemma retract_of_UNIV:
1.2964 -  fixes S :: "'a::euclidean_space set"
1.2965 -  shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> closed S"
1.2966 -by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV)
1.2967 -
1.2968 -lemma compact_AR:
1.2969 -  fixes S :: "'a::euclidean_space set"
1.2970 -  shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
1.2971 -using compact_imp_closed retract_of_UNIV by blast
1.2972 -
1.2973 -subsection\<open>More properties of ARs, ANRs and ENRs\<close>
1.2974 -
1.2975 -lemma not_AR_empty [simp]: "~ AR({})"
1.2976 -  by (auto simp: AR_def)
1.2977 -
1.2978 -lemma ENR_empty [simp]: "ENR {}"
1.2979 -  by (simp add: ENR_def)
1.2980 -
1.2981 -lemma ANR_empty [simp]: "ANR ({} :: 'a::euclidean_space set)"
1.2982 -  by (simp add: ENR_imp_ANR)
1.2983 -
1.2984 -lemma convex_imp_AR:
1.2985 -  fixes S :: "'a::euclidean_space set"
1.2986 -  shows "\<lbrakk>convex S; S \<noteq> {}\<rbrakk> \<Longrightarrow> AR S"
1.2987 -apply (rule absolute_extensor_imp_AR)
1.2988 -apply (rule Dugundji, assumption+)
1.2989 -by blast
1.2990 -
1.2991 -lemma convex_imp_ANR:
1.2992 -  fixes S :: "'a::euclidean_space set"
1.2993 -  shows "convex S \<Longrightarrow> ANR S"
1.2994 -using ANR_empty AR_imp_ANR convex_imp_AR by blast
1.2995 -
1.2996 -lemma ENR_convex_closed:
1.2997 -  fixes S :: "'a::euclidean_space set"
1.2998 -  shows "\<lbrakk>closed S; convex S\<rbrakk> \<Longrightarrow> ENR S"
1.2999 -using ENR_def ENR_empty convex_imp_AR retract_of_UNIV by blast
1.3000 -
1.3001 -lemma AR_UNIV [simp]: "AR (UNIV :: 'a::euclidean_space set)"
1.3002 -  using retract_of_UNIV by auto
1.3003 -
1.3004 -lemma ANR_UNIV [simp]: "ANR (UNIV :: 'a::euclidean_space set)"
1.3005 -  by (simp add: AR_imp_ANR)
1.3006 -
1.3007 -lemma ENR_UNIV [simp]:"ENR UNIV"
1.3008 -  using ENR_def by blast
1.3009 -
1.3010 -lemma AR_singleton:
1.3011 -    fixes a :: "'a::euclidean_space"
1.3012 -    shows "AR {a}"
1.3013 -  using retract_of_UNIV by blast
1.3014 -
1.3015 -lemma ANR_singleton:
1.3016 -    fixes a :: "'a::euclidean_space"
1.3017 -    shows "ANR {a}"
1.3018 -  by (simp add: AR_imp_ANR AR_singleton)
1.3019 -
1.3020 -lemma ENR_singleton: "ENR {a}"
1.3021 -  using ENR_def by blast
1.3022 -
1.3023 -subsection\<open>ARs closed under union\<close>
1.3024 -
1.3025 -lemma AR_closed_Un_local_aux:
1.3026 -  fixes U :: "'a::euclidean_space set"
1.3027 -  assumes "closedin (subtopology euclidean U) S"
1.3028 -          "closedin (subtopology euclidean U) T"
1.3029 -          "AR S" "AR T" "AR(S \<inter> T)"
1.3030 -  shows "(S \<union> T) retract_of U"
1.3031 -proof -
1.3032 -  have "S \<inter> T \<noteq> {}"
1.3033 -    using assms AR_def by fastforce
1.3034 -  have "S \<subseteq> U" "T \<subseteq> U"
1.3035 -    using assms by (auto simp: closedin_imp_subset)
1.3036 -  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
1.3037 -  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
1.3038 -  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
1.3039 -  have US': "closedin (subtopology euclidean U) S'"
1.3040 -    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
1.3041 -    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.3042 -  have UT': "closedin (subtopology euclidean U) T'"
1.3043 -    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
1.3044 -    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.3045 -  have "S \<subseteq> S'"
1.3046 -    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.3047 -  have "T \<subseteq> T'"
1.3048 -    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.3049 -  have "S \<inter> T \<subseteq> W" "W \<subseteq> U"
1.3050 -    using \<open>S \<subseteq> U\<close> by (auto simp: W_def setdist_sing_in_set)
1.3051 -  have "(S \<inter> T) retract_of W"
1.3052 -    apply (rule AR_imp_absolute_retract [OF \<open>AR(S \<inter> T)\<close>])
1.3053 -     apply (simp add: homeomorphic_refl)
1.3054 -    apply (rule closedin_subset_trans [of U])
1.3055 -    apply (simp_all add: assms closedin_Int \<open>S \<inter> T \<subseteq> W\<close> \<open>W \<subseteq> U\<close>)
1.3056 -    done
1.3057 -  then obtain r0
1.3058 -    where "S \<inter> T \<subseteq> W" and contr0: "continuous_on W r0"
1.3059 -      and "r0 ` W \<subseteq> S \<inter> T"
1.3060 -      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
1.3061 -      by (auto simp: retract_of_def retraction_def)
1.3062 -  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
1.3063 -    using setdist_eq_0_closedin \<open>S \<inter> T \<noteq> {}\<close> assms
1.3064 -    by (force simp: W_def setdist_sing_in_set)
1.3065 -  have "S' \<inter> T' = W"
1.3066 -    by (auto simp: S'_def T'_def W_def)
1.3067 -  then have cloUW: "closedin (subtopology euclidean U) W"
1.3068 -    using closedin_Int US' UT' by blast
1.3069 -  define r where "r \<equiv> \<lambda>x. if x \<in> W then r0 x else x"
1.3070 -  have "r ` (W \<union> S) \<subseteq> S" "r ` (W \<union> T) \<subseteq> T"
1.3071 -    using \<open>r0 ` W \<subseteq> S \<inter> T\<close> r_def by auto
1.3072 -  have contr: "continuous_on (W \<union> (S \<union> T)) r"
1.3073 -  unfolding r_def
1.3074 -  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
1.3075 -    show "closedin (subtopology euclidean (W \<union> (S \<union> T))) W"
1.3076 -      using \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> \<open>closedin (subtopology euclidean U) W\<close> closedin_subset_trans by fastforce
1.3077 -    show "closedin (subtopology euclidean (W \<union> (S \<union> T))) (S \<union> T)"
1.3078 -      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
1.3079 -    show "\<And>x. x \<in> W \<and> x \<notin> W \<or> x \<in> S \<union> T \<and> x \<in> W \<Longrightarrow> r0 x = x"
1.3080 -      by (auto simp: ST)
1.3081 -  qed
1.3082 -  have cloUWS: "closedin (subtopology euclidean U) (W \<union> S)"
1.3083 -    by (simp add: cloUW assms closedin_Un)
1.3084 -  obtain g where contg: "continuous_on U g"
1.3085 -             and "g ` U \<subseteq> S" and geqr: "\<And>x. x \<in> W \<union> S \<Longrightarrow> g x = r x"
1.3086 -    apply (rule AR_imp_absolute_extensor [OF \<open>AR S\<close> _ _ cloUWS])
1.3087 -      apply (rule continuous_on_subset [OF contr])
1.3088 -      using \<open>r ` (W \<union> S) \<subseteq> S\<close> apply auto
1.3089 -    done
1.3090 -  have cloUWT: "closedin (subtopology euclidean U) (W \<union> T)"
1.3091 -    by (simp add: cloUW assms closedin_Un)
1.3092 -  obtain h where conth: "continuous_on U h"
1.3093 -             and "h ` U \<subseteq> T" and heqr: "\<And>x. x \<in> W \<union> T \<Longrightarrow> h x = r x"
1.3094 -    apply (rule AR_imp_absolute_extensor [OF \<open>AR T\<close> _ _ cloUWT])
1.3095 -      apply (rule continuous_on_subset [OF contr])
1.3096 -      using \<open>r ` (W \<union> T) \<subseteq> T\<close> apply auto
1.3097 -    done
1.3098 -  have "U = S' \<union> T'"
1.3099 -    by (force simp: S'_def T'_def)
1.3100 -  then have cont: "continuous_on U (\<lambda>x. if x \<in> S' then g x else h x)"
1.3101 -    apply (rule ssubst)
1.3102 -    apply (rule continuous_on_cases_local)
1.3103 -    using US' UT' \<open>S' \<inter> T' = W\<close> \<open>U = S' \<union> T'\<close>
1.3104 -          contg conth continuous_on_subset geqr heqr apply auto
1.3105 -    done
1.3106 -  have UST: "(\<lambda>x. if x \<in> S' then g x else h x) ` U \<subseteq> S \<union> T"
1.3107 -    using \<open>g ` U \<subseteq> S\<close> \<open>h ` U \<subseteq> T\<close> by auto
1.3108 -  show ?thesis
1.3109 -    apply (simp add: retract_of_def retraction_def \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close>)
1.3110 -    apply (rule_tac x="\<lambda>x. if x \<in> S' then g x else h x" in exI)
1.3111 -    apply (intro conjI cont UST)
1.3112 -    by (metis IntI ST Un_iff \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> subsetD geqr heqr r0 r_def)
1.3113 -qed
1.3114 -
1.3115 -
1.3116 -proposition AR_closed_Un_local:
1.3117 -  fixes S :: "'a::euclidean_space set"
1.3118 -  assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
1.3119 -      and STT: "closedin (subtopology euclidean (S \<union> T)) T"
1.3120 -      and "AR S" "AR T" "AR(S \<inter> T)"
1.3121 -    shows "AR(S \<union> T)"
1.3122 -proof -
1.3123 -  have "C retract_of U"
1.3124 -       if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
1.3125 -       for U and C :: "('a * real) set"
1.3126 -  proof -
1.3127 -    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
1.3128 -      using hom by (force simp: homeomorphic_def)
1.3129 -    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
1.3130 -      apply (rule closedin_trans [OF _ UC])
1.3131 -      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
1.3132 -      using hom homeomorphism_def apply blast
1.3133 -      apply (metis hom homeomorphism_def set_eq_subset)
1.3134 -      done
1.3135 -    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
1.3136 -      apply (rule closedin_trans [OF _ UC])
1.3137 -      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
1.3138 -      using hom homeomorphism_def apply blast
1.3139 -      apply (metis hom homeomorphism_def set_eq_subset)
1.3140 -      done
1.3141 -    have ARS: "AR (C \<inter> g -` S)"
1.3142 -      apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
1.3143 -      apply (simp add: homeomorphic_def)
1.3144 -      apply (rule_tac x=g in exI)
1.3145 -      apply (rule_tac x=f in exI)
1.3146 -      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.3147 -      apply (rule_tac x="f x" in image_eqI, auto)
1.3148 -      done
1.3149 -    have ART: "AR (C \<inter> g -` T)"
1.3150 -      apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
1.3151 -      apply (simp add: homeomorphic_def)
1.3152 -      apply (rule_tac x=g in exI)
1.3153 -      apply (rule_tac x=f in exI)
1.3154 -      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.3155 -      apply (rule_tac x="f x" in image_eqI, auto)
1.3156 -      done
1.3157 -    have ARI: "AR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
1.3158 -      apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
1.3159 -      apply (simp add: homeomorphic_def)
1.3160 -      apply (rule_tac x=g in exI)
1.3161 -      apply (rule_tac x=f in exI)
1.3162 -      using hom
1.3163 -      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.3164 -      apply (rule_tac x="f x" in image_eqI, auto)
1.3165 -      done
1.3166 -    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
1.3167 -      using hom  by (auto simp: homeomorphism_def)
1.3168 -    then show ?thesis
1.3169 -      by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
1.3170 -  qed
1.3171 -  then show ?thesis
1.3172 -    by (force simp: AR_def)
1.3173 -qed
1.3174 -
1.3175 -corollary AR_closed_Un:
1.3176 -  fixes S :: "'a::euclidean_space set"
1.3177 -  shows "\<lbrakk>closed S; closed T; AR S; AR T; AR (S \<inter> T)\<rbrakk> \<Longrightarrow> AR (S \<union> T)"
1.3178 -by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV)
1.3179 -
1.3180 -subsection\<open>ANRs closed under union\<close>
1.3181 -
1.3182 -lemma ANR_closed_Un_local_aux:
1.3183 -  fixes U :: "'a::euclidean_space set"
1.3184 -  assumes US: "closedin (subtopology euclidean U) S"
1.3185 -      and UT: "closedin (subtopology euclidean U) T"
1.3186 -      and "ANR S" "ANR T" "ANR(S \<inter> T)"
1.3187 -  obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
1.3188 -proof (cases "S = {} \<or> T = {}")
1.3189 -  case True with assms that show ?thesis
1.3190 -    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
1.3191 -next
1.3192 -  case False
1.3193 -  then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
1.3194 -  have "S \<subseteq> U" "T \<subseteq> U"
1.3195 -    using assms by (auto simp: closedin_imp_subset)
1.3196 -  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
1.3197 -  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
1.3198 -  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
1.3199 -  have cloUS': "closedin (subtopology euclidean U) S'"
1.3200 -    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
1.3201 -    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.3202 -  have cloUT': "closedin (subtopology euclidean U) T'"
1.3203 -    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
1.3204 -    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
1.3205 -  have "S \<subseteq> S'"
1.3206 -    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.3207 -  have "T \<subseteq> T'"
1.3208 -    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
1.3209 -  have "S' \<union> T' = U"
1.3210 -    by (auto simp: S'_def T'_def)
1.3211 -  have "W \<subseteq> S'"
1.3212 -    by (simp add: Collect_mono S'_def W_def)
1.3213 -  have "W \<subseteq> T'"
1.3214 -    by (simp add: Collect_mono T'_def W_def)
1.3215 -  have ST_W: "S \<inter> T \<subseteq> W" and "W \<subseteq> U"
1.3216 -    using \<open>S \<subseteq> U\<close> by (force simp: W_def setdist_sing_in_set)+
1.3217 -  have "S' \<inter> T' = W"
1.3218 -    by (auto simp: S'_def T'_def W_def)
1.3219 -  then have cloUW: "closedin (subtopology euclidean U) W"
1.3220 -    using closedin_Int cloUS' cloUT' by blast
1.3221 -  obtain W' W0 where "openin (subtopology euclidean W) W'"
1.3222 -                 and cloWW0: "closedin (subtopology euclidean W) W0"
1.3223 -                 and "S \<inter> T \<subseteq> W'" "W' \<subseteq> W0"
1.3224 -                 and ret: "(S \<inter> T) retract_of W0"
1.3225 -    apply (rule ANR_imp_closed_neighbourhood_retract [OF \<open>ANR(S \<inter> T)\<close>])
1.3226 -    apply (rule closedin_subset_trans [of U, OF _ ST_W \<open>W \<subseteq> U\<close>])
1.3227 -    apply (blast intro: assms)+
1.3228 -    done
1.3229 -  then obtain U0 where opeUU0: "openin (subtopology euclidean U) U0"
1.3230 -                   and U0: "S \<inter> T \<subseteq> U0" "U0 \<inter> W \<subseteq> W0"
1.3231 -    unfolding openin_open  using \<open>W \<subseteq> U\<close> by blast
1.3232 -  have "W0 \<subseteq> U"
1.3233 -    using \<open>W \<subseteq> U\<close> cloWW0 closedin_subset by fastforce
1.3234 -  obtain r0
1.3235 -    where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
1.3236 -      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
1.3237 -    using ret  by (force simp: retract_of_def retraction_def)
1.3238 -  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
1.3239 -    using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
1.3240 -  define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
1.3241 -  have "r ` (W0 \<union> S) \<subseteq> S" "r ` (W0 \<union> T) \<subseteq> T"
1.3242 -    using \<open>r0 ` W0 \<subseteq> S \<inter> T\<close> r_def by auto
1.3243 -  have contr: "continuous_on (W0 \<union> (S \<union> T)) r"
1.3244 -  unfolding r_def
1.3245 -  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
1.3246 -    show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) W0"
1.3247 -      apply (rule closedin_subset_trans [of U])
1.3248 -      using cloWW0 cloUW closedin_trans \<open>W0 \<subseteq> U\<close> \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> apply blast+
1.3249 -      done
1.3250 -    show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) (S \<union> T)"
1.3251 -      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W0 \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
1.3252 -    show "\<And>x. x \<in> W0 \<and> x \<notin> W0 \<or> x \<in> S \<union> T \<and> x \<in> W0 \<Longrightarrow> r0 x = x"
1.3253 -      using ST cloWW0 closedin_subset by fastforce
1.3254 -  qed
1.3255 -  have cloS'WS: "closedin (subtopology euclidean S') (W0 \<union> S)"
1.3256 -    by (meson closedin_subset_trans US cloUS' \<open>S \<subseteq> S'\<close> \<open>W \<subseteq> S'\<close> cloUW cloWW0
1.3257 -              closedin_Un closedin_imp_subset closedin_trans)
1.3258 -  obtain W1 g where "W0 \<union> S \<subseteq> W1" and contg: "continuous_on W1 g"
1.3259 -                and opeSW1: "openin (subtopology euclidean S') W1"
1.3260 -                and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
1.3261 -    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
1.3262 -     apply (rule continuous_on_subset [OF contr], blast+)
1.3263 -    done
1.3264 -  have cloT'WT: "closedin (subtopology euclidean T') (W0 \<union> T)"
1.3265 -    by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0
1.3266 -              closedin_Un closedin_imp_subset closedin_trans)
1.3267 -  obtain W2 h where "W0 \<union> T \<subseteq> W2" and conth: "continuous_on W2 h"
1.3268 -                and opeSW2: "openin (subtopology euclidean T') W2"
1.3269 -                and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
1.3270 -    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
1.3271 -     apply (rule continuous_on_subset [OF contr], blast+)
1.3272 -    done
1.3273 -  have "S' \<inter> T' = W"
1.3274 -    by (force simp: S'_def T'_def W_def)
1.3275 -  obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
1.3276 -    using opeSW1 opeSW2 by (force simp: openin_open)
1.3277 -  show ?thesis
1.3278 -  proof
1.3279 -    have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
1.3280 -         ((U - T') \<inter> O1 \<union> (U - S') \<inter> O2 \<union> U \<inter> O1 \<inter> O2) - (W - U0)"
1.3281 -     using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close>
1.3282 -      by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
1.3283 -    show "openin (subtopology euclidean U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
1.3284 -      apply (subst eq)
1.3285 -      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>, simp_all)
1.3286 -      done
1.3287 -    have cloW1: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
1.3288 -      using cloUS' apply (simp add: closedin_closed)
1.3289 -      apply (erule ex_forward)
1.3290 -      using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
1.3291 -      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
1.3292 -      done
1.3293 -    have cloW2: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
1.3294 -      using cloUT' apply (simp add: closedin_closed)
1.3295 -      apply (erule ex_forward)
1.3296 -      using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
1.3297 -      apply (auto simp: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
1.3298 -      done
1.3299 -    have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
1.3300 -      using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr
1.3301 -      apply (auto simp: r_def, fastforce)
1.3302 -      using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close>  by auto
1.3303 -    have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
1.3304 -              r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and>
1.3305 -              (\<forall>x\<in>S \<union> T. r x = x)"
1.3306 -      apply (rule_tac x = "\<lambda>x. if  x \<in> S' then g x else h x" in exI)
1.3307 -      apply (intro conjI *)
1.3308 -      apply (rule continuous_on_cases_local
1.3309 -                  [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]])
1.3310 -      using \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close>
1.3311 -            \<open>g ` W1 \<subseteq> S\<close> \<open>h ` W2 \<subseteq> T\<close> apply auto
1.3312 -      using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> apply (fastforce simp add: geqr heqr)+
1.3313 -      done
1.3314 -    then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
1.3315 -      using  \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
1.3316 -      by (auto simp: retract_of_def retraction_def)
1.3317 -  qed
1.3318 -qed
1.3319 -
1.3320 -
1.3321 -proposition ANR_closed_Un_local:
1.3322 -  fixes S :: "'a::euclidean_space set"
1.3323 -  assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
1.3324 -      and STT: "closedin (subtopology euclidean (S \<union> T)) T"
1.3325 -      and "ANR S" "ANR T" "ANR(S \<inter> T)"
1.3326 -    shows "ANR(S \<union> T)"
1.3327 -proof -
1.3328 -  have "\<exists>T. openin (subtopology euclidean U) T \<and> C retract_of T"
1.3329 -       if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
1.3330 -       for U and C :: "('a * real) set"
1.3331 -  proof -
1.3332 -    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
1.3333 -      using hom by (force simp: homeomorphic_def)
1.3334 -    have US: "closedin (subtopology euclidean U) (C \<inter> g -` S)"
1.3335 -      apply (rule closedin_trans [OF _ UC])
1.3336 -      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
1.3337 -      using hom [unfolded homeomorphism_def] apply blast
1.3338 -      apply (metis hom homeomorphism_def set_eq_subset)
1.3339 -      done
1.3340 -    have UT: "closedin (subtopology euclidean U) (C \<inter> g -` T)"
1.3341 -      apply (rule closedin_trans [OF _ UC])
1.3342 -      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
1.3343 -      using hom [unfolded homeomorphism_def] apply blast
1.3344 -      apply (metis hom homeomorphism_def set_eq_subset)
1.3345 -      done
1.3346 -    have ANRS: "ANR (C \<inter> g -` S)"
1.3347 -      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
1.3348 -      apply (simp add: homeomorphic_def)
1.3349 -      apply (rule_tac x=g in exI)
1.3350 -      apply (rule_tac x=f in exI)
1.3351 -      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.3352 -      apply (rule_tac x="f x" in image_eqI, auto)
1.3353 -      done
1.3354 -    have ANRT: "ANR (C \<inter> g -` T)"
1.3355 -      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
1.3356 -      apply (simp add: homeomorphic_def)
1.3357 -      apply (rule_tac x=g in exI)
1.3358 -      apply (rule_tac x=f in exI)
1.3359 -      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.3360 -      apply (rule_tac x="f x" in image_eqI, auto)
1.3361 -      done
1.3362 -    have ANRI: "ANR ((C \<inter> g -` S) \<inter> (C \<inter> g -` T))"
1.3363 -      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
1.3364 -      apply (simp add: homeomorphic_def)
1.3365 -      apply (rule_tac x=g in exI)
1.3366 -      apply (rule_tac x=f in exI)
1.3367 -      using hom
1.3368 -      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
1.3369 -      apply (rule_tac x="f x" in image_eqI, auto)
1.3370 -      done
1.3371 -    have "C = (C \<inter> g -` S) \<union> (C \<inter> g -` T)"
1.3372 -      using hom by (auto simp: homeomorphism_def)
1.3373 -    then show ?thesis
1.3374 -      by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
1.3375 -  qed
1.3376 -  then show ?thesis
1.3377 -    by (auto simp: ANR_def)
1.3378 -qed
1.3379 -
1.3380 -corollary ANR_closed_Un:
1.3381 -  fixes S :: "'a::euclidean_space set"
1.3382 -  shows "\<lbrakk>closed S; closed T; ANR S; ANR T; ANR (S \<inter> T)\<rbrakk> \<Longrightarrow> ANR (S \<union> T)"
1.3383 -by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int)
1.3384 -
1.3385 -lemma ANR_openin:
1.3386 -  fixes S :: "'a::euclidean_space set"
1.3387 -  assumes "ANR T" and opeTS: "openin (subtopology euclidean T) S"
1.3388 -  shows "ANR S"
1.3389 -proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
1.3390 -  fix f :: "'a \<times> real \<Rightarrow> 'a" and U C
1.3391 -  assume contf: "continuous_on C f" and fim: "f ` C \<subseteq> S"
1.3392 -     and cloUC: "closedin (subtopology euclidean U) C"
1.3393 -  have "f ` C \<subseteq> T"
1.3394 -    using fim opeTS openin_imp_subset by blast
1.3395 -  obtain W g where "C \<subseteq> W"
1.3396 -               and UW: "openin (subtopology euclidean U) W"
1.3397 -               and contg: "continuous_on W g"
1.3398 -               and gim: "g ` W \<subseteq> T"
1.3399 -               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = f x"
1.3400 -    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf \<open>f ` C \<subseteq> T\<close> cloUC])
1.3401 -    using fim by auto
1.3402 -  show "\<exists>V g. C \<subseteq> V \<and> openin (subtopology euclidean U) V \<and> continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x\<in>C. g x = f x)"
1.3403 -  proof (intro exI conjI)
1.3404 -    show "C \<subseteq> W \<inter> g -` S"
1.3405 -      using \<open>C \<subseteq> W\<close> fim geq by blast
1.3406 -    show "openin (subtopology euclidean U) (W \<inter> g -` S)"
1.3407 -      by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
1.3408 -    show "continuous_on (W \<inter> g -` S) g"
1.3409 -      by (blast intro: continuous_on_subset [OF contg])
1.3410 -    show "g ` (W \<inter> g -` S) \<subseteq> S"
1.3411 -      using gim by blast
1.3412 -    show "\<forall>x\<in>C. g x = f x"
1.3413 -      using geq by blast
1.3414 -  qed
1.3415 -qed
1.3416 -
1.3417 -lemma ENR_openin:
1.3418 -    fixes S :: "'a::euclidean_space set"
1.3419 -    assumes "ENR T" and opeTS: "openin (subtopology euclidean T) S"
1.3420 -    shows "ENR S"
1.3421 -  using assms apply (simp add: ENR_ANR)
1.3422 -  using ANR_openin locally_open_subset by blast
1.3423 -
1.3424 -lemma ANR_neighborhood_retract:
1.3425 -    fixes S :: "'a::euclidean_space set"
1.3426 -    assumes "ANR U" "S retract_of T" "openin (subtopology euclidean U) T"
1.3427 -    shows "ANR S"
1.3428 -  using ANR_openin ANR_retract_of_ANR assms by blast
1.3429 -
1.3430 -lemma ENR_neighborhood_retract:
1.3431 -    fixes S :: "'a::euclidean_space set"
1.3432 -    assumes "ENR U" "S retract_of T" "openin (subtopology euclidean U) T"
1.3433 -    shows "ENR S"
1.3434 -  using ENR_openin ENR_retract_of_ENR assms by blast
1.3435 -
1.3436 -lemma ANR_rel_interior:
1.3437 -  fixes S :: "'a::euclidean_space set"
1.3438 -  shows "ANR S \<Longrightarrow> ANR(rel_interior S)"
1.3439 -   by (blast intro: ANR_openin openin_set_rel_interior)
1.3440 -
1.3441 -lemma ANR_delete:
1.3442 -  fixes S :: "'a::euclidean_space set"
1.3443 -  shows "ANR S \<Longrightarrow> ANR(S - {a})"
1.3444 -   by (blast intro: ANR_openin openin_delete openin_subtopology_self)
1.3445 -
1.3446 -lemma ENR_rel_interior:
1.3447 -  fixes S :: "'a::euclidean_space set"
1.3448 -  shows "ENR S \<Longrightarrow> ENR(rel_interior S)"
1.3449 -   by (blast intro: ENR_openin openin_set_rel_interior)
1.3450 -
1.3451 -lemma ENR_delete:
1.3452 -  fixes S :: "'a::euclidean_space set"
1.3453 -  shows "ENR S \<Longrightarrow> ENR(S - {a})"
1.3454 -   by (blast intro: ENR_openin openin_delete openin_subtopology_self)
1.3455 -
1.3456 -lemma open_imp_ENR: "open S \<Longrightarrow> ENR S"
1.3457 -    using ENR_def by blast
1.3458 -
1.3459 -lemma open_imp_ANR:
1.3460 -    fixes S :: "'a::euclidean_space set"
1.3461 -    shows "open S \<Longrightarrow> ANR S"
1.3462 -  by (simp add: ENR_imp_ANR open_imp_ENR)
1.3463 -
1.3464 -lemma ANR_ball [iff]:
1.3465 -    fixes a :: "'a::euclidean_space"
1.3466 -    shows "ANR(ball a r)"
1.3467 -  by (simp add: convex_imp_ANR)
1.3468 -
1.3469 -lemma ENR_ball [iff]: "ENR(ball a r)"
1.3470 -  by (simp add: open_imp_ENR)
1.3471 -
1.3472 -lemma AR_ball [simp]:
1.3473 -    fixes a :: "'a::euclidean_space"
1.3474 -    shows "AR(ball a r) \<longleftrightarrow> 0 < r"
1.3475 -  by (auto simp: AR_ANR convex_imp_contractible)
1.3476 -
1.3477 -lemma ANR_cball [iff]:
1.3478 -    fixes a :: "'a::euclidean_space"
1.3479 -    shows "ANR(cball a r)"
1.3480 -  by (simp add: convex_imp_ANR)
1.3481 -
1.3482 -lemma ENR_cball:
1.3483 -    fixes a :: "'a::euclidean_space"
1.3484 -    shows "ENR(cball a r)"
1.3485 -  using ENR_convex_closed by blast
1.3486 -
1.3487 -lemma AR_cball [simp]:
1.3488 -    fixes a :: "'a::euclidean_space"
1.3489 -    shows "AR(cball a r) \<longleftrightarrow> 0 \<le> r"
1.3490 -  by (auto simp: AR_ANR convex_imp_contractible)
1.3491 -
1.3492 -lemma ANR_box [iff]:
1.3493 -    fixes a :: "'a::euclidean_space"
1.3494 -    shows "ANR(cbox a b)" "ANR(box a b)"
1.3495 -  by (auto simp: convex_imp_ANR open_imp_ANR)
1.3496 -
1.3497 -lemma ENR_box [iff]:
1.3498 -    fixes a :: "'a::euclidean_space"
1.3499 -    shows "ENR(cbox a b)" "ENR(box a b)"
1.3500 -apply (simp add: ENR_convex_closed closed_cbox)
1.3501 -by (simp add: open_box open_imp_ENR)
1.3502 -
1.3503 -lemma AR_box [simp]:
1.3504 -    "AR(cbox a b) \<longleftrightarrow> cbox a b \<noteq> {}" "AR(box a b) \<longleftrightarrow> box a b \<noteq> {}"
1.3505 -  by (auto simp: AR_ANR convex_imp_contractible)
1.3506 -
1.3507 -lemma ANR_interior:
1.3508 -     fixes S :: "'a::euclidean_space set"
1.3509 -     shows "ANR(interior S)"
1.3510 -  by (simp add: open_imp_ANR)
1.3511 -
1.3512 -lemma ENR_interior:
1.3513 -     fixes S :: "'a::euclidean_space set"
1.3514 -     shows "ENR(interior S)"
1.3515 -  by (simp add: open_imp_ENR)
1.3516 -
1.3517 -lemma AR_imp_contractible:
1.3518 -    fixes S :: "'a::euclidean_space set"
1.3519 -    shows "AR S \<Longrightarrow> contractible S"
1.3520 -  by (simp add: AR_ANR)
1.3521 -
1.3522 -lemma ENR_imp_locally_compact:
1.3523 -    fixes S :: "'a::euclidean_space set"
1.3524 -    shows "ENR S \<Longrightarrow> locally compact S"
1.3525 -  by (simp add: ENR_ANR)
1.3526 -
1.3527 -lemma ANR_imp_locally_path_connected:
1.3528 -  fixes S :: "'a::euclidean_space set"
1.3529 -  assumes "ANR S"
1.3530 -    shows "locally path_connected S"
1.3531 -proof -
1.3532 -  obtain U and T :: "('a \<times> real) set"
1.3533 -     where "convex U" "U \<noteq> {}"
1.3534 -       and UT: "closedin (subtopology euclidean U) T"
1.3535 -       and "S homeomorphic T"
1.3536 -    apply (rule homeomorphic_closedin_convex [of S])
1.3537 -    using aff_dim_le_DIM [of S] apply auto
1.3538 -    done
1.3539 -  then have "locally path_connected T"
1.3540 -    by (meson ANR_imp_absolute_neighbourhood_retract
1.3541 -        assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
1.3542 -  then have S: "locally path_connected S"
1.3543 -      if "openin (subtopology euclidean U) V" "T retract_of V" "U \<noteq> {}" for V
1.3544 -    using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
1.3545 -  show ?thesis
1.3546 -    using assms
1.3547 -    apply (clarsimp simp: ANR_def)
1.3548 -    apply (drule_tac x=U in spec)
1.3549 -    apply (drule_tac x=T in spec)
1.3550 -    using \<open>S homeomorphic T\<close> \<open>U \<noteq> {}\<close> UT  apply (blast intro: S)
1.3551 -    done
1.3552 -qed
1.3553 -
1.3554 -lemma ANR_imp_locally_connected:
1.3555 -  fixes S :: "'a::euclidean_space set"
1.3556 -  assumes "ANR S"
1.3557 -    shows "locally connected S"
1.3558 -using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto
1.3559 -
1.3560 -lemma AR_imp_locally_path_connected:
1.3561 -  fixes S :: "'a::euclidean_space set"
1.3562 -  assumes "AR S"
1.3563 -    shows "locally path_connected S"
1.3564 -by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms)
1.3565 -
1.3566 -lemma AR_imp_locally_connected:
1.3567 -  fixes S :: "'a::euclidean_space set"
1.3568 -  assumes "AR S"
1.3569 -    shows "locally connected S"
1.3570 -using ANR_imp_locally_connected AR_ANR assms by blast
1.3571 -
1.3572 -lemma ENR_imp_locally_path_connected:
1.3573 -  fixes S :: "'a::euclidean_space set"
1.3574 -  assumes "ENR S"
1.3575 -    shows "locally path_connected S"
1.3576 -by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms)
1.3577 -
1.3578 -lemma ENR_imp_locally_connected:
1.3579 -  fixes S :: "'a::euclidean_space set"
1.3580 -  assumes "ENR S"
1.3581 -    shows "locally connected S"
1.3582 -using ANR_imp_locally_connected ENR_ANR assms by blast
1.3583 -
1.3584 -lemma ANR_Times:
1.3585 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.3586 -  assumes "ANR S" "ANR T" shows "ANR(S \<times> T)"
1.3587 -proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
1.3588 -  fix f :: " ('a \<times> 'b) \<times> real \<Rightarrow> 'a \<times> 'b" and U C
1.3589 -  assume "continuous_on C f" and fim: "f ` C \<subseteq> S \<times> T"
1.3590 -     and cloUC: "closedin (subtopology euclidean U) C"
1.3591 -  have contf1: "continuous_on C (fst \<circ> f)"
1.3592 -    by (simp add: \<open>continuous_on C f\<close> continuous_on_fst)
1.3593 -  obtain W1 g where "C \<subseteq> W1"
1.3594 -               and UW1: "openin (subtopology euclidean U) W1"
1.3595 -               and contg: "continuous_on W1 g"
1.3596 -               and gim: "g ` W1 \<subseteq> S"
1.3597 -               and geq: "\<And>x. x \<in> C \<Longrightarrow> g x = (fst \<circ> f) x"
1.3598 -    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> contf1 _ cloUC])
1.3599 -    using fim apply auto
1.3600 -    done
1.3601 -  have contf2: "continuous_on C (snd \<circ> f)"
1.3602 -    by (simp add: \<open>continuous_on C f\<close> continuous_on_snd)
1.3603 -  obtain W2 h where "C \<subseteq> W2"
1.3604 -               and UW2: "openin (subtopology euclidean U) W2"
1.3605 -               and conth: "continuous_on W2 h"
1.3606 -               and him: "h ` W2 \<subseteq> T"
1.3607 -               and heq: "\<And>x. x \<in> C \<Longrightarrow> h x = (snd \<circ> f) x"
1.3608 -    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf2 _ cloUC])
1.3609 -    using fim apply auto
1.3610 -    done
1.3611 -  show "\<exists>V g. C \<subseteq> V \<and>
1.3612 -               openin (subtopology euclidean U) V \<and>
1.3613 -               continuous_on V g \<and> g ` V \<subseteq> S \<times> T \<and> (\<forall>x\<in>C. g x = f x)"
1.3614 -  proof (intro exI conjI)
1.3615 -    show "C \<subseteq> W1 \<inter> W2"
1.3616 -      by (simp add: \<open>C \<subseteq> W1\<close> \<open>C \<subseteq> W2\<close>)
1.3617 -    show "openin (subtopology euclidean U) (W1 \<inter> W2)"
1.3618 -      by (simp add: UW1 UW2 openin_Int)
1.3619 -    show  "continuous_on (W1 \<inter> W2) (\<lambda>x. (g x, h x))"
1.3620 -      by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
1.3621 -    show  "(\<lambda>x. (g x, h x)) ` (W1 \<inter> W2) \<subseteq> S \<times> T"
1.3622 -      using gim him by blast
1.3623 -    show  "(\<forall>x\<in>C. (g x, h x) = f x)"
1.3624 -      using geq heq by auto
1.3625 -  qed
1.3626 -qed
1.3627 -
1.3628 -lemma AR_Times:
1.3629 -  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
1.3630 -  assumes "AR S" "AR T" shows "AR(S \<times> T)"
1.3631 -using assms by (simp add: AR_ANR ANR_Times contractible_Times)
1.3632 +subsubsection  \<open>We continue with ANRs and ENRs\<close>
1.3633
1.3634  lemma ENR_rel_frontier_convex:
1.3635    fixes S :: "'a::euclidean_space set"
1.3636 @@ -4065,7 +4071,7 @@
1.3637    shows "ANR S"
1.3638    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.3639
1.3640 -proposition ANR_finite_Union_convex_closed:
1.3641 +lemma ANR_finite_Union_convex_closed:
1.3642    fixes \<T> :: "'a::euclidean_space set set"
1.3643    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.3644    shows "ANR(\<Union>\<T>)"
1.3645 @@ -4149,7 +4155,7 @@
1.3646    shows "ANR c"
1.3647    by (metis ANR_connected_component_ANR assms componentsE)
1.3648
1.3649 -subsection\<open>Original ANR material, now for ENRs\<close>
1.3650 +subsubsection\<open>Original ANR material, now for ENRs\<close>
1.3651
1.3652  lemma ENR_bounded:
1.3653    fixes S :: "'a::euclidean_space set"
1.3654 @@ -4258,7 +4264,7 @@
1.3655    SIMP_TAC[ENR_ANR; ANR_PCROSS; LOCALLY_COMPACT_PCROSS]);;
1.3656  *)
1.3657
1.3658 -subsection\<open>Finally, spheres are ANRs and ENRs\<close>
1.3659 +subsubsection\<open>Finally, spheres are ANRs and ENRs\<close>
1.3660
1.3661  lemma absolute_retract_homeomorphic_convex_compact:
1.3662    fixes S :: "'a::euclidean_space set" and U :: "'b::euclidean_space set"
1.3663 @@ -4291,7 +4297,7 @@
1.3664    shows "sphere a r retract_of (- {a})"
1.3665    by (simp add: assms sphere_retract_of_punctured_universe_gen)
1.3666
1.3667 -proposition ENR_sphere:
1.3668 +lemma ENR_sphere:
1.3669    fixes a :: "'a::euclidean_space"
1.3670    shows "ENR(sphere a r)"
1.3671  proof (cases "0 < r")
1.3672 @@ -4307,13 +4313,12 @@
1.3673      by (metis finite_insert infinite_imp_nonempty less_linear sphere_eq_empty sphere_trivial)
1.3674  qed
1.3675
1.3676 -corollary ANR_sphere:
1.3677 +corollary%unimportant ANR_sphere:
1.3678    fixes a :: "'a::euclidean_space"
1.3679    shows "ANR(sphere a r)"
1.3680    by (simp add: ENR_imp_ANR ENR_sphere)
1.3681
1.3682 -
1.3683 -subsection\<open>Spheres are connected, etc\<close>
1.3684 +subsubsection\<open>Spheres are connected, etc\<close>
1.3685
1.3686  lemma locally_path_connected_sphere_gen:
1.3687    fixes S :: "'a::euclidean_space set"
1.3688 @@ -4352,8 +4357,7 @@
1.3689    shows "locally connected(sphere a r)"
1.3690    using ANR_imp_locally_connected ANR_sphere by blast
1.3691
1.3692 -
1.3693 -subsection\<open>Borsuk homotopy extension theorem\<close>
1.3694 +subsubsection\<open>Borsuk homotopy extension theorem\<close>
1.3695
1.3696  text\<open>It's only this late so we can use the concept of retraction,
1.3697    saying that the domain sets or range set are ENRs.\<close>
1.3698 @@ -4491,7 +4495,7 @@
1.3699  qed
1.3700
1.3701
1.3702 -corollary nullhomotopic_into_ANR_extension:
1.3703 +corollary%unimportant nullhomotopic_into_ANR_extension:
1.3704    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.3705    assumes "closed S"
1.3706        and contf: "continuous_on S f"
1.3707 @@ -4527,7 +4531,7 @@
1.3708      done
1.3709  qed
1.3710
1.3711 -corollary nullhomotopic_into_rel_frontier_extension:
1.3712 +corollary%unimportant nullhomotopic_into_rel_frontier_extension:
1.3713    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.3714    assumes "closed S"
1.3715        and contf: "continuous_on S f"
1.3716 @@ -4538,7 +4542,7 @@
1.3717            (\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> (\<forall>x \<in> S. g x = f x))"
1.3718  by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex)
1.3719
1.3720 -corollary nullhomotopic_into_sphere_extension:
1.3721 +corollary%unimportant nullhomotopic_into_sphere_extension:
1.3722    fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: euclidean_space"
1.3723    assumes "closed S" and contf: "continuous_on S f"
1.3724        and "S \<noteq> {}" and fim: "f ` S \<subseteq> sphere a r"
1.3725 @@ -4560,7 +4564,7 @@
1.3726      done
1.3727  qed
1.3728
1.3729 -proposition Borsuk_map_essential_bounded_component:
1.3730 +proposition%unimportant Borsuk_map_essential_bounded_component:
1.3731    fixes a :: "'a :: euclidean_space"
1.3732    assumes "compact S" and "a \<notin> S"
1.3733     shows "bounded (connected_component_set (- S) a) \<longleftrightarrow>
1.3734 @@ -4700,8 +4704,7 @@
1.3736  qed
1.3737
1.3738 -
1.3739 -subsection\<open>More extension theorems\<close>
1.3740 +subsubsection\<open>More extension theorems\<close>
1.3741
1.3742  lemma extension_from_clopen:
1.3743    assumes ope: "openin (subtopology euclidean S) T"
1.3744 @@ -4819,7 +4822,7 @@
1.3745    qed
1.3746  qed
1.3747
1.3748 -proposition homotopic_neighbourhood_extension:
1.3749 +proposition%unimportant homotopic_neighbourhood_extension:
1.3750    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
1.3751    assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> U"
1.3752        and contg: "continuous_on S g" and gim: "g ` S \<subseteq> U"
1.3753 @@ -4884,7 +4887,7 @@
1.3754  qed
1.3755
1.3756  text\<open> Homotopy on a union of closed-open sets.\<close>
1.3757 -proposition homotopic_on_clopen_Union:
1.3758 +proposition%unimportant homotopic_on_clopen_Union:
1.3759    fixes \<F> :: "'a::euclidean_space set set"
1.3760    assumes "\<And>S. S \<in> \<F> \<Longrightarrow> closedin (subtopology euclidean (\<Union>\<F>)) S"
1.3761        and "\<And>S. S \<in> \<F> \<Longrightarrow> openin (subtopology euclidean (\<Union>\<F>)) S"
1.3762 @@ -4957,7 +4960,7 @@
1.3763    qed
1.3764  qed
1.3765
1.3766 -proposition homotopic_on_components_eq:
1.3767 +lemma homotopic_on_components_eq:
1.3768    fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set"
1.3769    assumes S: "locally connected S \<or> compact S" and "ANR T"
1.3770    shows "homotopic_with (\<lambda>x. True) S T f g \<longleftrightarrow>
1.3771 @@ -5080,8 +5083,7 @@
1.3772    qed
1.3773  qed
1.3774
1.3775 -
1.3776 -subsection\<open>The complement of a set and path-connectedness\<close>
1.3777 +subsubsection\<open>The complement of a set and path-connectedness\<close>
1.3778
1.3779  text\<open>Complement in dimension N > 1 of set homeomorphic to any interval in
1.3780   any dimension is (path-)connected. This naively generalizes the argument
```
```     2.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Wed Jul 11 23:24:25 2018 +0100
2.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Jul 12 11:23:46 2018 +0200
2.3 @@ -12,7 +12,7 @@
2.4
2.5  subsection \<open>Type class of Euclidean spaces\<close>
2.6
2.7 -class%important euclidean_space = real_inner +
2.8 +class euclidean_space = real_inner +
2.9    fixes Basis :: "'a set"
2.10    assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
2.11    assumes finite_Basis [simp]: "finite Basis"
2.12 @@ -224,7 +224,7 @@
2.13
2.14  subsubsection%unimportant \<open>Type @{typ real}\<close>
2.15
2.16 -instantiation%important real :: euclidean_space
2.17 +instantiation real :: euclidean_space
2.18  begin
2.19
2.20  definition
2.21 @@ -240,7 +240,7 @@
2.22
2.23  subsubsection%unimportant \<open>Type @{typ complex}\<close>
2.24
2.25 -instantiation%important complex :: euclidean_space
2.26 +instantiation complex :: euclidean_space
2.27  begin
2.28
2.29  definition Basis_complex_def: "Basis = {1, \<i>}"
2.30 @@ -261,7 +261,7 @@
2.31
2.32  subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
2.33
2.34 -instantiation%important prod :: (euclidean_space, euclidean_space) euclidean_space
2.35 +instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
2.36  begin
2.37
2.38  definition
```
```     3.1 --- a/src/HOL/Analysis/Inner_Product.thy	Wed Jul 11 23:24:25 2018 +0100
3.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Thu Jul 12 11:23:46 2018 +0200
3.3 @@ -274,7 +274,7 @@
3.4
3.5  subsection \<open>Class instances\<close>
3.6
3.7 -instantiation%important real :: real_inner
3.8 +instantiation real :: real_inner
3.9  begin
3.10
3.11  definition inner_real_def [simp]: "inner = ( * )"
3.12 @@ -303,7 +303,7 @@
3.13      and real_inner_1_right[simp]: "inner x 1 = x"
3.14    by simp_all
3.15
3.16 -instantiation%important complex :: real_inner
3.17 +instantiation complex :: real_inner
3.18  begin
3.19
3.20  definition inner_complex_def:
```
```     4.1 --- a/src/HOL/Analysis/Measure_Space.thy	Wed Jul 11 23:24:25 2018 +0100
4.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Jul 12 11:23:46 2018 +0200
4.3 @@ -2834,7 +2834,7 @@
4.4    of the lexicographical order are point-wise ordered.
4.5  \<close>
4.6
4.7 -instantiation%important measure :: (type) order_bot
4.8 +instantiation measure :: (type) order_bot
4.9  begin
4.10
4.11  inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
4.12 @@ -3028,7 +3028,7 @@
4.13       (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def
4.14                      sigma_sets_superset_generator sigma_sets_le_sets_iff)
4.15
4.16 -instantiation%important measure :: (type) semilattice_sup
4.17 +instantiation measure :: (type) semilattice_sup
4.18  begin
4.19
4.20  definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
4.21 @@ -3159,7 +3159,7 @@
4.23  qed
4.24
4.25 -instantiation%important measure :: (type) complete_lattice
4.26 +instantiation measure :: (type) complete_lattice
4.27  begin
4.28
4.29  interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
```
```     5.1 --- a/src/HOL/Analysis/Product_Vector.thy	Wed Jul 11 23:24:25 2018 +0100
5.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Thu Jul 12 11:23:46 2018 +0200
5.3 @@ -58,7 +58,7 @@
5.4
5.5  subsection \<open>Product is a real vector space\<close>
5.6
5.7 -instantiation%important prod :: (real_vector, real_vector) real_vector
5.8 +instantiation prod :: (real_vector, real_vector) real_vector
5.9  begin
5.10
5.11  definition scaleR_prod_def:
5.12 @@ -113,7 +113,7 @@
5.13
5.14  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
5.15
5.16 -instantiation%important prod :: (metric_space, metric_space) dist
5.17 +instantiation prod :: (metric_space, metric_space) dist
5.18  begin
5.19
5.20  definition%important dist_prod_def[code del]:
5.21 @@ -135,7 +135,7 @@
5.22
5.23  declare uniformity_Abort[where 'a="'a :: metric_space \<times> 'b :: metric_space", code]
5.24
5.25 -instantiation%important prod :: (metric_space, metric_space) metric_space
5.26 +instantiation prod :: (metric_space, metric_space) metric_space
5.27  begin
5.28
5.29  lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
5.30 @@ -270,7 +270,7 @@
5.31
5.32  subsection \<open>Product is a normed vector space\<close>
5.33
5.34 -instantiation%important prod :: (real_normed_vector, real_normed_vector) real_normed_vector
5.35 +instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector
5.36  begin
5.37
5.38  definition norm_prod_def[code del]:
5.39 @@ -398,7 +398,7 @@
5.40
5.41  subsection \<open>Product is an inner product space\<close>
5.42
5.43 -instantiation%important prod :: (real_inner, real_inner) real_inner
5.44 +instantiation prod :: (real_inner, real_inner) real_inner
5.45  begin
5.46
5.47  definition inner_prod_def:
```
```     6.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Jul 11 23:24:25 2018 +0100
6.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jul 12 11:23:46 2018 +0200
6.3 @@ -603,7 +603,7 @@
6.4  text \<open>Textbooks define Polish spaces as completely metrizable.
6.5    We assume the topology to be complete for a given metric.\<close>
6.6
6.7 -class%important polish_space = complete_space + second_countable_topology
6.8 +class polish_space = complete_space + second_countable_topology
6.9
6.10  subsection \<open>General notion of a topology as a value\<close>
6.11
6.12 @@ -4573,7 +4573,7 @@
6.13    Heine-Borel property if every closed and bounded subset is compact.
6.14  \<close>
6.15
6.16 -class%important heine_borel = metric_space +
6.17 +class heine_borel = metric_space +
6.18    assumes bounded_imp_convergent_subsequence:
6.19      "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
6.20
```
```     7.1 --- a/src/HOL/ROOT	Wed Jul 11 23:24:25 2018 +0100
7.2 +++ b/src/HOL/ROOT	Thu Jul 12 11:23:46 2018 +0200
7.3 @@ -58,7 +58,7 @@
7.4    document_files "root.bib" "root.tex"
7.5
7.6  session "HOL-Analysis" (main timing) in Analysis = HOL +
7.7 -  options [document_tags = "theorem%important,corollary%important,proposition%important,%unimportant",
7.8 +  options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant",
7.9      document_variants = "document:manual=-proof,-ML,-unimportant"]
7.10    sessions
7.11      "HOL-Library"
```