more economic tagging
authornipkow
Thu Jul 12 11:23:46 2018 +0200 (13 months ago)
changeset 6861775129a73aca3
parent 68616 cedf3480fdad
child 68619 79abf4201e8d
more economic tagging
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/ROOT
     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.584 +apply (simp add: absolute_extensor_imp_AR)
   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.763 +apply (simp add: absolute_neighbourhood_extensor_imp_ANR)
   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.928 +apply (simp add: ANR_def)
   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.2468 -apply (simp add: absolute_extensor_imp_AR)
  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.2647 -apply (simp add: absolute_neighbourhood_extensor_imp_ANR)
  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.2813 -apply (simp add: ANR_def)
  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.3735      by (simp add: Borsuk_maps_homotopic_in_path_component)
  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.22      by (simp add: A(3))
    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"