section ‹Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts› theory Retracts imports Brouwer_Fixpoint Continuous_Extension begin text ‹Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding in spaces of higher dimension. John Harrison writes: "This turns out to be sufficient (since any set in ‹ℝ⇧^{n}› can be embedded as a closed subset of a convex subset of ‹ℝ⇧^{n}⇧^{+}⇧^{1}›) to derive the usual definitions, but we need to split them into two implications because of the lack of type quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."› definition✐‹tag important› AR :: "'a::topological_space set ⇒ bool" where "AR S ≡ ∀U. ∀S'::('a * real) set. S homeomorphic S' ∧ closedin (top_of_set U) S' ⟶ S' retract_of U" definition✐‹tag important› ANR :: "'a::topological_space set ⇒ bool" where "ANR S ≡ ∀U. ∀S'::('a * real) set. S homeomorphic S' ∧ closedin (top_of_set U) S' ⟶ (∃T. openin (top_of_set U) T ∧ S' retract_of T)" definition✐‹tag important› ENR :: "'a::topological_space set ⇒ bool" where "ENR S ≡ ∃U. open U ∧ S retract_of U" text ‹First, show that we do indeed get the "usual" properties of ARs and ANRs.› lemma AR_imp_absolute_extensor: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "AR S" and contf: "continuous_on T f" and "f ` T ⊆ S" and cloUT: "closedin (top_of_set U) T" obtains g where "continuous_on U g" "g ` U ⊆ S" "⋀x. x ∈ T ⟹ g x = f x" proof - have "aff_dim S < int (DIM('b × real))" using aff_dim_le_DIM [of S] by simp then obtain C and S' :: "('b * real) set" where C: "convex C" "C ≠ {}" and cloCS: "closedin (top_of_set C) S'" and hom: "S homeomorphic S'" by (metis that homeomorphic_closedin_convex) then have "S' retract_of C" using ‹AR S› by (simp add: AR_def) then obtain r where "S' ⊆ C" and contr: "continuous_on C r" and "r ` C ⊆ S'" and rid: "⋀x. x∈S' ⟹ r x = x" by (auto simp: retraction_def retract_of_def) obtain g h where "homeomorphism S S' g h" using hom by (force simp: homeomorphic_def) then have "continuous_on (f ` T) g" by (meson ‹f ` T ⊆ S› continuous_on_subset homeomorphism_def) then have contgf: "continuous_on T (g ∘ f)" by (metis continuous_on_compose contf) have gfTC: "(g ∘ f) ` T ⊆ C" proof - have "g ` S = S'" by (metis (no_types) ‹homeomorphism S S' g h› homeomorphism_def) with ‹S' ⊆ C› ‹f ` T ⊆ S› show ?thesis by force qed obtain f' where f': "continuous_on U f'" "f' ` U ⊆ C" "⋀x. x ∈ T ⟹ f' x = (g ∘ f) x" by (metis Dugundji [OF C cloUT contgf gfTC]) show ?thesis proof (rule_tac g = "h ∘ r ∘ f'" in that) show "continuous_on U (h ∘ r ∘ f')" proof (intro continuous_on_compose f') show "continuous_on (f' ` U) r" using continuous_on_subset contr f' by blast show "continuous_on (r ` f' ` U) h" using ‹homeomorphism S S' g h› ‹f' ` U ⊆ C› unfolding homeomorphism_def by (metis ‹r ` C ⊆ S'› continuous_on_subset image_mono) qed show "(h ∘ r ∘ f') ` U ⊆ S" using ‹homeomorphism S S' g h› ‹r ` C ⊆ S'› ‹f' ` U ⊆ C› by (fastforce simp: homeomorphism_def) show "⋀x. x ∈ T ⟹ (h ∘ r ∘ f') x = f x" using ‹homeomorphism S S' g h› ‹f ` T ⊆ S› f' by (auto simp: rid homeomorphism_def) qed qed lemma AR_imp_absolute_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "AR S" "S homeomorphic S'" and clo: "closedin (top_of_set U) S'" shows "S' retract_of U" proof - obtain g h where hom: "homeomorphism S S' g h" using assms by (force simp: homeomorphic_def) obtain h: "continuous_on S' h" " h ` S' ⊆ S" using hom homeomorphism_def by blast obtain h' where h': "continuous_on U h'" "h' ` U ⊆ S" and h'h: "⋀x. x ∈ S' ⟹ h' x = h x" by (blast intro: AR_imp_absolute_extensor [OF ‹AR S› h clo]) have [simp]: "S' ⊆ U" using clo closedin_limpt by blast show ?thesis proof (simp add: retraction_def retract_of_def, intro exI conjI) show "continuous_on U (g ∘ h')" by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1) show "(g ∘ h') ∈ U → S'" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈S'. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed qed lemma AR_imp_absolute_retract_UNIV: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "AR S" "S homeomorphic S'" "closed S'" shows "S' retract_of UNIV" using AR_imp_absolute_retract assms by fastforce lemma absolute_extensor_imp_AR: fixes S :: "'a::euclidean_space set" assumes "⋀f :: 'a * real ⇒ 'a. ⋀U T. ⟦continuous_on T f; f ` T ⊆ S; closedin (top_of_set U) T⟧ ⟹ ∃g. continuous_on U g ∧ g ` U ⊆ S ∧ (∀x ∈ T. g x = f x)" shows "AR S" proof (clarsimp simp: AR_def) fix U and T :: "('a * real) set" assume "S homeomorphic T" and clo: "closedin (top_of_set U) T" then obtain g h where hom: "homeomorphism S T g h" by (force simp: homeomorphic_def) obtain h: "continuous_on T h" " h ` T ⊆ S" using hom homeomorphism_def by blast obtain h' where h': "continuous_on U h'" "h' ` U ⊆ S" and h'h: "∀x∈T. h' x = h x" using assms [OF h clo] by blast have [simp]: "T ⊆ U" using clo closedin_imp_subset by auto show "T retract_of U" proof (simp add: retraction_def retract_of_def, intro exI conjI) show "continuous_on U (g ∘ h')" by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1) show "(g ∘ h') ∈ U → T" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈T. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed qed lemma AR_eq_absolute_extensor: fixes S :: "'a::euclidean_space set" shows "AR S ⟷ (∀f :: 'a * real ⇒ 'a. ∀U T. continuous_on T f ⟶ f ` T ⊆ S ⟶ closedin (top_of_set U) T ⟶ (∃g. continuous_on U g ∧ g ` U ⊆ S ∧ (∀x ∈ T. g x = f x)))" by (metis (mono_tags, opaque_lifting) AR_imp_absolute_extensor absolute_extensor_imp_AR) lemma AR_imp_retract: fixes S :: "'a::euclidean_space set" assumes "AR S ∧ closedin (top_of_set U) S" shows "S retract_of U" using AR_imp_absolute_retract assms homeomorphic_refl by blast lemma AR_homeomorphic_AR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "AR T" "S homeomorphic T" shows "AR S" unfolding AR_def by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym) lemma homeomorphic_AR_iff_AR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" shows "S homeomorphic T ⟹ AR S ⟷ AR T" by (metis AR_homeomorphic_AR homeomorphic_sym) lemma ANR_imp_absolute_neighbourhood_extensor: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "ANR S" and contf: "continuous_on T f" and "f ∈ T → S" and cloUT: "closedin (top_of_set U) T" obtains V g where "T ⊆ V" "openin (top_of_set U) V" "continuous_on V g" "g ∈ V → S" "⋀x. x ∈ T ⟹ g x = f x" proof - have "aff_dim S < int (DIM('b × real))" using aff_dim_le_DIM [of S] by simp then obtain C and S' :: "('b * real) set" where C: "convex C" "C ≠ {}" and cloCS: "closedin (top_of_set C) S'" and hom: "S homeomorphic S'" by (metis that homeomorphic_closedin_convex) then obtain D where opD: "openin (top_of_set C) D" and "S' retract_of D" using ‹ANR S› by (auto simp: ANR_def) then obtain r where "S' ⊆ D" and contr: "continuous_on D r" and "r ` D ⊆ S'" and rid: "⋀x. x ∈ S' ⟹ r x = x" by (auto simp: retraction_def retract_of_def) obtain g h where homgh: "homeomorphism S S' g h" using hom by (force simp: homeomorphic_def) have "continuous_on (f ` T) g" by (metis PiE assms(3) continuous_on_subset homeomorphism_cont1 homgh image_subset_iff) then have contgf: "continuous_on T (g ∘ f)" by (intro continuous_on_compose contf) have gfTC: "(g ∘ f) ` T ⊆ C" proof - have "g ` S = S'" by (metis (no_types) homeomorphism_def homgh) then show ?thesis by (metis PiE assms(3) cloCS closedin_def image_comp image_mono image_subset_iff order.trans topspace_euclidean_subtopology) qed obtain f' where contf': "continuous_on U f'" and "f' ` U ⊆ C" and eq: "⋀x. x ∈ T ⟹ f' x = (g ∘ f) x" by (metis Dugundji [OF C cloUT contgf gfTC]) show ?thesis proof (rule_tac V = "U ∩ f' -` D" and g = "h ∘ r ∘ f'" in that) show "T ⊆ U ∩ f' -` D" using cloUT closedin_imp_subset ‹S' ⊆ D› ‹f ∈ T → S› eq homeomorphism_image1 homgh by fastforce show ope: "openin (top_of_set U) (U ∩ f' -` D)" by (meson ‹f' ` U ⊆ C› contf' continuous_openin_preimage image_subset_iff_funcset opD) have conth: "continuous_on (r ` f' ` (U ∩ f' -` D)) h" proof (rule continuous_on_subset [of S']) show "continuous_on S' h" using homeomorphism_def homgh by blast qed (use ‹r ` D ⊆ S'› in blast) show "continuous_on (U ∩ f' -` D) (h ∘ r ∘ f')" by (blast intro: continuous_on_compose conth continuous_on_subset [OF contr] continuous_on_subset [OF contf']) show "(h ∘ r ∘ f') ∈ (U ∩ f' -` D) → S" using ‹homeomorphism S S' g h› ‹f' ` U ⊆ C› ‹r ` D ⊆ S'› by (auto simp: homeomorphism_def) show "⋀x. x ∈ T ⟹ (h ∘ r ∘ f') x = f x" using ‹homeomorphism S S' g h› ‹f ∈ T → S› eq by (metis PiE comp_apply homeomorphism_def image_iff rid) qed qed corollary ANR_imp_absolute_neighbourhood_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ANR S" "S homeomorphic S'" and clo: "closedin (top_of_set U) S'" obtains V where "openin (top_of_set U) V" "S' retract_of V" proof - obtain g h where hom: "homeomorphism S S' g h" using assms by (force simp: homeomorphic_def) obtain h: "continuous_on S' h" " h ∈ S' → S" using hom homeomorphism_def by blast from ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› h clo] obtain V h' where "S' ⊆ V" and opUV: "openin (top_of_set U) V" and h': "continuous_on V h'" "h' ` V ⊆ S" and h'h:"⋀x. x ∈ S' ⟹ h' x = h x" by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› h clo]) have "S' retract_of V" proof (simp add: retraction_def retract_of_def, intro exI conjI ‹S' ⊆ V›) show "continuous_on V (g ∘ h')" by (meson continuous_on_compose continuous_on_subset h'(1) h'(2) hom homeomorphism_cont1) show "(g ∘ h') ∈ V → S'" using h' by clarsimp (metis hom subsetD homeomorphism_def imageI) show "∀x∈S'. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed then show ?thesis by (rule that [OF opUV]) qed corollary ANR_imp_absolute_neighbourhood_retract_UNIV: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'" obtains V where "open V" "S' retract_of V" using ANR_imp_absolute_neighbourhood_retract [OF ‹ANR S› hom] by (metis clo closed_closedin open_openin subtopology_UNIV) corollary neighbourhood_extension_into_ANR: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes contf: "continuous_on S f" and fim: "f ∈ S → T" and "ANR T" "closed S" obtains V g where "S ⊆ V" "open V" "continuous_on V g" "g ∈ V → T" "⋀x. x ∈ S ⟹ g x = f x" using ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf fim] by (metis ‹closed S› closed_closedin open_openin subtopology_UNIV) lemma absolute_neighbourhood_extensor_imp_ANR: fixes S :: "'a::euclidean_space set" assumes "⋀f :: 'a * real ⇒ 'a. ⋀U T. ⟦continuous_on T f; f ∈ T → S; closedin (top_of_set U) T⟧ ⟹ ∃V g. T ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ∈ V → S ∧ (∀x ∈ T. g x = f x)" shows "ANR S" proof (clarsimp simp: ANR_def) fix U and T :: "('a * real) set" assume "S homeomorphic T" and clo: "closedin (top_of_set U) T" then obtain g h where hom: "homeomorphism S T g h" by (force simp: homeomorphic_def) obtain h: "continuous_on T h" " h ∈ T → S" using hom homeomorphism_def by blast obtain V h' where "T ⊆ V" and opV: "openin (top_of_set U) V" and h': "continuous_on V h'" "h' ∈ V → S" and h'h: "∀x∈T. h' x = h x" using assms [OF h clo] by blast have [simp]: "T ⊆ U" using clo closedin_imp_subset by auto have "T retract_of V" proof (simp add: retraction_def retract_of_def, intro exI conjI ‹T ⊆ V›) show "continuous_on V (g ∘ h')" by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_def image_subset_iff_funcset) show "(g ∘ h') ∈ V → T" using h' hom homeomorphism_image1 by fastforce show "∀x∈T. (g ∘ h') x = x" by clarsimp (metis h'h hom homeomorphism_def) qed then show "∃V. openin (top_of_set U) V ∧ T retract_of V" using opV by blast qed lemma ANR_eq_absolute_neighbourhood_extensor: fixes S :: "'a::euclidean_space set" shows "ANR S ⟷ (∀f :: 'a * real ⇒ 'a. ∀U T. continuous_on T f ⟶ f ∈ T → S ⟶ closedin (top_of_set U) T ⟶ (∃V g. T ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ∈ V → S ∧ (∀x ∈ T. g x = f x)))" (is "_ = ?rhs") proof assume "ANR S" then show ?rhs by (metis ANR_imp_absolute_neighbourhood_extensor) qed (simp add: absolute_neighbourhood_extensor_imp_ANR) lemma ANR_imp_neighbourhood_retract: fixes S :: "'a::euclidean_space set" assumes "ANR S" "closedin (top_of_set U) S" obtains V where "openin (top_of_set U) V" "S retract_of V" using ANR_imp_absolute_neighbourhood_retract assms homeomorphic_refl by blast lemma ANR_imp_absolute_closed_neighbourhood_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ANR S" "S homeomorphic S'" and US': "closedin (top_of_set U) S'" obtains V W where "openin (top_of_set U) V" "closedin (top_of_set U) W" "S' ⊆ V" "V ⊆ W" "S' retract_of W" proof - obtain Z where "openin (top_of_set U) Z" and S'Z: "S' retract_of Z" by (blast intro: assms ANR_imp_absolute_neighbourhood_retract) then have UUZ: "closedin (top_of_set U) (U - Z)" by auto have "S' ∩ (U - Z) = {}" using ‹S' retract_of Z› closedin_retract closedin_subtopology by fastforce then obtain V W where "openin (top_of_set U) V" and "openin (top_of_set U) W" and "S' ⊆ V" "U - Z ⊆ W" "V ∩ W = {}" using separation_normal_local [OF US' UUZ] by auto moreover have "S' retract_of U - W" proof (rule retract_of_subset [OF S'Z]) show "S' ⊆ U - W" using US' ‹S' ⊆ V› ‹V ∩ W = {}› closedin_subset by fastforce show "U - W ⊆ Z" using Diff_subset_conv ‹U - Z ⊆ W› by blast qed ultimately show ?thesis by (metis Diff_subset_conv Diff_triv Int_Diff_Un Int_absorb1 openin_closedin_eq that topspace_euclidean_subtopology) qed lemma ANR_imp_closed_neighbourhood_retract: fixes S :: "'a::euclidean_space set" assumes "ANR S" "closedin (top_of_set U) S" obtains V W where "openin (top_of_set U) V" "closedin (top_of_set U) W" "S ⊆ V" "V ⊆ W" "S retract_of W" by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl) lemma ANR_homeomorphic_ANR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "ANR T" "S homeomorphic T" shows "ANR S" unfolding ANR_def by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym) lemma homeomorphic_ANR_iff_ANR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" shows "S homeomorphic T ⟹ ANR S ⟷ ANR T" by (metis ANR_homeomorphic_ANR homeomorphic_sym) subsection ‹Analogous properties of ENRs› lemma ENR_imp_absolute_neighbourhood_retract: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ENR S" and hom: "S homeomorphic S'" and "S' ⊆ U" obtains V where "openin (top_of_set U) V" "S' retract_of V" proof - obtain X where "open X" "S retract_of X" using ‹ENR S› by (auto simp: ENR_def) then obtain r where "retraction X S r" by (auto simp: retract_of_def) have "locally compact S'" using retract_of_locally_compact open_imp_locally_compact homeomorphic_local_compactness ‹S retract_of X› ‹open X› hom by blast then obtain W where UW: "openin (top_of_set U) W" and WS': "closedin (top_of_set W) S'" apply (rule locally_compact_closedin_open) by (meson Int_lower2 assms(3) closedin_imp_subset closedin_subset_trans le_inf_iff openin_open) obtain f g where hom: "homeomorphism S S' f g" using assms by (force simp: homeomorphic_def) have contg: "continuous_on S' g" using hom homeomorphism_def by blast moreover have "g ` S' ⊆ S" by (metis hom equalityE homeomorphism_def) ultimately obtain h where conth: "continuous_on W h" and hg: "⋀x. x ∈ S' ⟹ h x = g x" using Tietze_unbounded [of S' g W] WS' by blast have "W ⊆ U" using UW openin_open by auto have "S' ⊆ W" using WS' closedin_closed by auto have him: "⋀x. x ∈ S' ⟹ h x ∈ X" by (metis (no_types) ‹S retract_of X› hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq) have "S' retract_of (W ∩ h -` X)" proof (simp add: retraction_def retract_of_def, intro exI conjI) show "S' ⊆ W" "S' ⊆ h -` X" using him WS' closedin_imp_subset by blast+ show "continuous_on (W ∩ h -` X) (f ∘ r ∘ h)" proof (intro continuous_on_compose) show "continuous_on (W ∩ h -` X) h" by (meson conth continuous_on_subset inf_le1) show "continuous_on (h ` (W ∩ h -` X)) r" proof - have "h ` (W ∩ h -` X) ⊆ X" by blast then show "continuous_on (h ` (W ∩ h -` X)) r" by (meson ‹retraction X S r› continuous_on_subset retraction) qed show "continuous_on (r ` h ` (W ∩ h -` X)) f" proof (rule continuous_on_subset [of S]) show "continuous_on S f" using hom homeomorphism_def by blast show "r ` h ` (W ∩ h -` X) ⊆ S" by (metis ‹retraction X S r› image_mono image_subset_iff_subset_vimage inf_le2 retraction) qed qed show "(f ∘ r ∘ h) ∈ (W ∩ h -` X) → S'" using ‹retraction X S r› hom by (auto simp: retraction_def homeomorphism_def) show "∀x∈S'. (f ∘ r ∘ h) x = x" using ‹retraction X S r› hom by (auto simp: retraction_def homeomorphism_def hg) qed then show ?thesis using UW ‹open X› conth continuous_openin_preimage_eq openin_trans that by blast qed corollary ENR_imp_absolute_neighbourhood_retract_UNIV: fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" assumes "ENR S" "S homeomorphic S'" obtains T' where "open T'" "S' retract_of T'" by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV) lemma ENR_homeomorphic_ENR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "ENR T" "S homeomorphic T" shows "ENR S" unfolding ENR_def by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym) lemma homeomorphic_ENR_iff_ENR: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "S homeomorphic T" shows "ENR S ⟷ ENR T" by (meson ENR_homeomorphic_ENR assms homeomorphic_sym) lemma ENR_translation: fixes S :: "'a::euclidean_space set" shows "ENR(image (λx. a + x) S) ⟷ ENR S" by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR) lemma ENR_linear_image_eq: fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space" assumes "linear f" "inj f" shows "ENR (image f S) ⟷ ENR S" by (meson assms homeomorphic_ENR_iff_ENR linear_homeomorphic_image) text ‹Some relations among the concepts. We also relate AR to being a retract of UNIV, which is often a more convenient proxy in the closed case.› lemma AR_imp_ANR: "AR S ⟹ ANR S" using ANR_def AR_def by fastforce lemma ENR_imp_ANR: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ ANR S" by (meson ANR_def ENR_imp_absolute_neighbourhood_retract closedin_imp_subset) lemma ENR_ANR: fixes S :: "'a::euclidean_space set" shows "ENR S ⟷ ANR S ∧ locally compact S" proof assume "ENR S" then have "locally compact S" using ENR_def open_imp_locally_compact retract_of_locally_compact by auto then show "ANR S ∧ locally compact S" using ENR_imp_ANR ‹ENR S› by blast next assume "ANR S ∧ locally compact S" then have "ANR S" "locally compact S" by auto then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T" using locally_compact_homeomorphic_closed by (metis DIM_prod DIM_real Suc_eq_plus1 lessI) then show "ENR S" using ‹ANR S› by (meson ANR_imp_absolute_neighbourhood_retract_UNIV ENR_def ENR_homeomorphic_ENR) qed lemma AR_ANR: fixes S :: "'a::euclidean_space set" shows "AR S ⟷ ANR S ∧ contractible S ∧ S ≠ {}" (is "?lhs = ?rhs") proof assume ?lhs have "aff_dim S < int DIM('a × real)" using aff_dim_le_DIM [of S] by auto then obtain C and S' :: "('a * real) set" where "convex C" "C ≠ {}" "closedin (top_of_set C) S'" "S homeomorphic S'" using homeomorphic_closedin_convex by blast with ‹AR S› have "contractible S" by (meson AR_def convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible) with ‹AR S› show ?rhs using AR_imp_ANR AR_imp_retract by fastforce next assume ?rhs then obtain a and h:: "real × 'a ⇒ 'a" where conth: "continuous_on ({0..1} × S) h" and hS: "h ` ({0..1} × S) ⊆ S" and [simp]: "⋀x. h(0, x) = x" and [simp]: "⋀x. h(1, x) = a" and "ANR S" "S ≠ {}" by (auto simp: contractible_def homotopic_with_def) then have "a ∈ S" by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one) have "∃g. continuous_on W g ∧ g ∈ W → S ∧ (∀x∈T. g x = f x)" if f: "continuous_on T f" "f ∈ T → S" and WT: "closedin (top_of_set W) T" for W T and f :: "'a × real ⇒ 'a" proof - obtain U g where "T ⊆ U" and WU: "openin (top_of_set W) U" and contg: "continuous_on U g" and "g ∈ U → S" and gf: "⋀x. x ∈ T ⟹ g x = f x" using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor ‹ANR S›, rule_format, OF f WT] by auto have WWU: "closedin (top_of_set W) (W - U)" using WU closedin_diff by fastforce moreover have "(W - U) ∩ T = {}" using ‹T ⊆ U› by auto ultimately obtain V V' where WV': "openin (top_of_set W) V'" and WV: "openin (top_of_set W) V" and "W - U ⊆ V'" "T ⊆ V" "V' ∩ V = {}" using separation_normal_local [of W "W-U" T] WT by blast then have WVT: "T ∩ (W - V) = {}" by auto have WWV: "closedin (top_of_set W) (W - V)" using WV closedin_diff by fastforce obtain j :: " 'a × real ⇒ real" where contj: "continuous_on W j" and j: "⋀x. x ∈ W ⟹ j x ∈ {0..1}" and j0: "⋀x. x ∈ W - V ⟹ j x = 1" and j1: "⋀x. x ∈ T ⟹ j x = 0" by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment) have Weq: "W = (W - V) ∪ (W - V')" using ‹V' ∩ V = {}› by force show ?thesis proof (intro conjI exI) have *: "continuous_on (W - V') (λx. h (j x, g x))" proof (rule continuous_on_compose2 [OF conth continuous_on_Pair]) show "continuous_on (W - V') j" by (rule continuous_on_subset [OF contj Diff_subset]) show "continuous_on (W - V') g" by (metis Diff_subset_conv ‹W - U ⊆ V'› contg continuous_on_subset Un_commute) show "(λx. (j x, g x)) ` (W - V') ⊆ {0..1} × S" using j ‹g ∈ U → S› ‹W - U ⊆ V'› by fastforce qed show "continuous_on W (λx. if x ∈ W - V then a else h (j x, g x))" proof (subst Weq, rule continuous_on_cases_local) show "continuous_on (W - V') (λx. h (j x, g x))" using "*" by blast qed (use WWV WV' Weq j0 j1 in auto) next have "h (j (x, y), g (x, y)) ∈ S" if "(x, y) ∈ W" "(x, y) ∈ V" for x y proof - have "j(x, y) ∈ {0..1}" using j that by blast moreover have "g(x, y) ∈ S" using ‹V' ∩ V = {}› ‹W - U ⊆ V'› ‹g ∈ U → S› that by fastforce ultimately show ?thesis using hS by blast qed with ‹a ∈ S› ‹g ∈ U → S› show "(λx. if x ∈ W - V then a else h (j x, g x)) ∈ W → S" by auto next show "∀x∈T. (if x ∈ W - V then a else h (j x, g x)) = f x" using ‹T ⊆ V› by (auto simp: j0 j1 gf) qed qed then show ?lhs by (simp add: AR_eq_absolute_extensor image_subset_iff_funcset) qed lemma ANR_retract_of_ANR: fixes S :: "'a::euclidean_space set" assumes "ANR T" and ST: "S retract_of T" shows "ANR S" proof (clarsimp simp add: ANR_eq_absolute_neighbourhood_extensor) fix f::"'a × real ⇒ 'a" and U W assume W: "continuous_on W f" "f ∈ W → S" "closedin (top_of_set U) W" then obtain r where "S ⊆ T" and r: "continuous_on T r" "r ∈ T → S" "∀x∈S. r x = x" "continuous_on W f" "f ∈ W → S" "closedin (top_of_set U) W" by (metis ST retract_of_def retraction_def) then have "f ` W ⊆ T" by blast with W obtain V g where V: "W ⊆ V" "openin (top_of_set U) V" "continuous_on V g" "g ∈ V → T" "∀x∈W. g x = f x" by (smt (verit) ANR_imp_absolute_neighbourhood_extensor Pi_I assms(1) funcset_mem image_subset_iff_funcset) with r have "continuous_on V (r ∘ g) ∧ (r ∘ g) ∈ V → S ∧ (∀x∈W. (r ∘ g) x = f x)" by (smt (verit, del_insts) Pi_iff comp_apply continuous_on_compose continuous_on_subset image_subset_iff_funcset) then show "∃V. W ⊆ V ∧ openin (top_of_set U) V ∧ (∃g. continuous_on V g ∧ g ∈ V → S ∧ (∀x∈W. g x = f x))" by (meson V) qed lemma AR_retract_of_AR: fixes S :: "'a::euclidean_space set" shows "⟦AR T; S retract_of T⟧ ⟹ AR S" using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce lemma ENR_retract_of_ENR: "⟦ENR T; S retract_of T⟧ ⟹ ENR S" by (meson ENR_def retract_of_trans) lemma retract_of_UNIV: fixes S :: "'a::euclidean_space set" shows "S retract_of UNIV ⟷ AR S ∧ closed S" 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) lemma compact_AR: fixes S :: "'a::euclidean_space set" shows "compact S ∧ AR S ⟷ compact S ∧ S retract_of UNIV" using compact_imp_closed retract_of_UNIV by blast text ‹More properties of ARs, ANRs and ENRs› lemma not_AR_empty [simp]: "¬ AR({})" by (auto simp: AR_def) lemma ENR_empty [simp]: "ENR {}" by (simp add: ENR_def) lemma ANR_empty [simp]: "ANR ({} :: 'a::euclidean_space set)" by (simp add: ENR_imp_ANR) lemma convex_imp_AR: fixes S :: "'a::euclidean_space set" shows "⟦convex S; S ≠ {}⟧ ⟹ AR S" by (metis (mono_tags, lifting) Dugundji absolute_extensor_imp_AR) lemma convex_imp_ANR: fixes S :: "'a::euclidean_space set" shows "convex S ⟹ ANR S" using ANR_empty AR_imp_ANR convex_imp_AR by blast lemma ENR_convex_closed: fixes S :: "'a::euclidean_space set" shows "⟦closed S; convex S⟧ ⟹ ENR S" using ENR_def ENR_empty convex_imp_AR retract_of_UNIV by blast lemma AR_UNIV [simp]: "AR (UNIV :: 'a::euclidean_space set)" using retract_of_UNIV by auto lemma ANR_UNIV [simp]: "ANR (UNIV :: 'a::euclidean_space set)" by (simp add: AR_imp_ANR) lemma ENR_UNIV [simp]:"ENR UNIV" using ENR_def by blast lemma AR_singleton: fixes a :: "'a::euclidean_space" shows "AR {a}" using retract_of_UNIV by blast lemma ANR_singleton: fixes a :: "'a::euclidean_space" shows "ANR {a}" by (simp add: AR_imp_ANR AR_singleton) lemma ENR_singleton: "ENR {a}" using ENR_def by blast text ‹ARs closed under union› lemma AR_closed_Un_local_aux: fixes U :: "'a::euclidean_space set" assumes "closedin (top_of_set U) S" "closedin (top_of_set U) T" "AR S" "AR T" "AR(S ∩ T)" shows "(S ∪ T) retract_of U" proof - have "S ∩ T ≠ {}" using assms AR_def by fastforce have "S ⊆ U" "T ⊆ U" using assms by (auto simp: closedin_imp_subset) define S' where "S' ≡ {x ∈ U. setdist {x} S ≤ setdist {x} T}" define T' where "T' ≡ {x ∈ U. setdist {x} T ≤ setdist {x} S}" define W where "W ≡ {x ∈ U. setdist {x} S = setdist {x} T}" have US': "closedin (top_of_set U) S'" using continuous_closedin_preimage [of U "λx. setdist {x} S - setdist {x} T" "{..0}"] by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have UT': "closedin (top_of_set U) T'" using continuous_closedin_preimage [of U "λx. setdist {x} T - setdist {x} S" "{..0}"] by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have "S ⊆ S'" using S'_def ‹S ⊆ U› setdist_sing_in_set by fastforce have "T ⊆ T'" using T'_def ‹T ⊆ U› setdist_sing_in_set by fastforce have "S ∩ T ⊆ W" "W ⊆ U" using ‹S ⊆ U› by (auto simp: W_def setdist_sing_in_set) have "(S ∩ T) retract_of W" proof (rule AR_imp_absolute_retract [OF ‹AR(S ∩ T)›]) show "S ∩ T homeomorphic S ∩ T" by (simp add: homeomorphic_refl) show "closedin (top_of_set W) (S ∩ T)" by (meson ‹S ∩ T ⊆ W› ‹W ⊆ U› assms closedin_Int closedin_subset_trans) qed then obtain r0 where "S ∩ T ⊆ W" and contr0: "continuous_on W r0" and "r0 ` W ⊆ S ∩ T" and r0 [simp]: "⋀x. x ∈ S ∩ T ⟹ r0 x = x" by (auto simp: retract_of_def retraction_def) have ST: "x ∈ W ⟹ x ∈ S ⟷ x ∈ T" for x using setdist_eq_0_closedin ‹S ∩ T ≠ {}› assms by (force simp: W_def setdist_sing_in_set) have "S' ∩ T' = W" by (auto simp: S'_def T'_def W_def) then have cloUW: "closedin (top_of_set U) W" using closedin_Int US' UT' by blast define r where "r ≡ λx. if x ∈ W then r0 x else x" have contr: "continuous_on (W ∪ (S ∪ T)) r" unfolding r_def proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id]) show "closedin (top_of_set (W ∪ (S ∪ T))) W" using ‹S ⊆ U› ‹T ⊆ U› ‹W ⊆ U› ‹closedin (top_of_set U) W› closedin_subset_trans by fastforce show "closedin (top_of_set (W ∪ (S ∪ T))) (S ∪ T)" by (meson ‹S ⊆ U› ‹T ⊆ U› ‹W ⊆ U› assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2) show "⋀x. x ∈ W ∧ x ∉ W ∨ x ∈ S ∪ T ∧ x ∈ W ⟹ r0 x = x" by (auto simp: ST) qed have rim: "r ` (W ∪ S) ⊆ S" "r ` (W ∪ T) ⊆ T" using ‹r0 ` W ⊆ S ∩ T› r_def by auto have cloUWS: "closedin (top_of_set U) (W ∪ S)" by (simp add: cloUW assms closedin_Un) obtain g where contg: "continuous_on U g" and "g ` U ⊆ S" and geqr: "⋀x. x ∈ W ∪ S ⟹ g x = r x" proof (rule AR_imp_absolute_extensor [OF ‹AR S› _ _ cloUWS]) show "continuous_on (W ∪ S) r" using continuous_on_subset contr sup_assoc by blast qed (use rim in auto) have cloUWT: "closedin (top_of_set U) (W ∪ T)" by (simp add: cloUW assms closedin_Un) obtain h where conth: "continuous_on U h" and "h ` U ⊆ T" and heqr: "⋀x. x ∈ W ∪ T ⟹ h x = r x" proof (rule AR_imp_absolute_extensor [OF ‹AR T› _ _ cloUWT]) show "continuous_on (W ∪ T) r" using continuous_on_subset contr sup_assoc by blast qed (use rim in auto) have U: "U = S' ∪ T'" by (force simp: S'_def T'_def) have cont: "continuous_on U (λx. if x ∈ S' then g x else h x)" unfolding U apply (rule continuous_on_cases_local) using US' UT' ‹S' ∩ T' = W› ‹U = S' ∪ T'› contg conth continuous_on_subset geqr heqr by auto have UST: "(λx. if x ∈ S' then g x else h x) ` U ⊆ S ∪ T" using ‹g ` U ⊆ S› ‹h ` U ⊆ T› by auto show ?thesis apply (simp add: retract_of_def retraction_def ‹S ⊆ U› ‹T ⊆ U›) apply (rule_tac x="λx. if x ∈ S' then g x else h x" in exI) using ST UST ‹S ⊆ S'› ‹S' ∩ T' = W› ‹T ⊆ T'› cont geqr heqr r_def by (smt (verit, del_insts) IntI Pi_I Un_iff image_subset_iff r0 subsetD) qed lemma AR_closed_Un_local: fixes S :: "'a::euclidean_space set" assumes STS: "closedin (top_of_set (S ∪ T)) S" and STT: "closedin (top_of_set (S ∪ T)) T" and "AR S" "AR T" "AR(S ∩ T)" shows "AR(S ∪ T)" proof - have "C retract_of U" if hom: "S ∪ T homeomorphic C" and UC: "closedin (top_of_set U) C" for U and C :: "('a * real) set" proof - obtain f g where hom: "homeomorphism (S ∪ T) C f g" using hom by (force simp: homeomorphic_def) have US: "closedin (top_of_set U) (C ∩ g -` S)" by (metis STS continuous_on_imp_closedin hom homeomorphism_def closedin_trans [OF _ UC]) have UT: "closedin (top_of_set U) (C ∩ g -` T)" by (metis STT continuous_on_closed hom homeomorphism_def closedin_trans [OF _ UC]) have "homeomorphism (C ∩ g -` S) S g f" using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done then have ARS: "AR (C ∩ g -` S)" using ‹AR S› homeomorphic_AR_iff_AR homeomorphic_def by blast have "homeomorphism (C ∩ g -` T) T g f" using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done then have ART: "AR (C ∩ g -` T)" using ‹AR T› homeomorphic_AR_iff_AR homeomorphic_def by blast have "homeomorphism (C ∩ g -` S ∩ (C ∩ g -` T)) (S ∩ T) g f" using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) apply (rule_tac x="f x" in image_eqI, auto) done then have ARI: "AR ((C ∩ g -` S) ∩ (C ∩ g -` T))" using ‹AR (S ∩ T)› homeomorphic_AR_iff_AR homeomorphic_def by blast have "C = (C ∩ g -` S) ∪ (C ∩ g -` T)" using hom by (auto simp: homeomorphism_def) then show ?thesis by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI]) qed then show ?thesis by (force simp: AR_def) qed corollary AR_closed_Un: fixes S :: "'a::euclidean_space set" shows "⟦closed S; closed T; AR S; AR T; AR (S ∩ T)⟧ ⟹ AR (S ∪ T)" by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV) text ‹ANRs closed under union› lemma ANR_closed_Un_local_aux: fixes U :: "'a::euclidean_space set" assumes US: "closedin (top_of_set U) S" and UT: "closedin (top_of_set U) T" and "ANR S" "ANR T" "ANR(S ∩ T)" obtains V where "openin (top_of_set U) V" "(S ∪ T) retract_of V" proof (cases "S = {} ∨ T = {}") case True with assms that show ?thesis by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb) next case False then have [simp]: "S ≠ {}" "T ≠ {}" by auto have "S ⊆ U" "T ⊆ U" using assms by (auto simp: closedin_imp_subset) define S' where "S' ≡ {x ∈ U. setdist {x} S ≤ setdist {x} T}" define T' where "T' ≡ {x ∈ U. setdist {x} T ≤ setdist {x} S}" define W where "W ≡ {x ∈ U. setdist {x} S = setdist {x} T}" have cloUS': "closedin (top_of_set U) S'" using continuous_closedin_preimage [of U "λx. setdist {x} S - setdist {x} T" "{..0}"] by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have cloUT': "closedin (top_of_set U) T'" using continuous_closedin_preimage [of U "λx. setdist {x} T - setdist {x} S" "{..0}"] by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist) have "S ⊆ S'" using S'_def ‹S ⊆ U› setdist_sing_in_set by fastforce have "T ⊆ T'" using T'_def ‹T ⊆ U› setdist_sing_in_set by fastforce have "S' ∪ T' = U" by (auto simp: S'_def T'_def) have "W ⊆ S'" by (simp add: Collect_mono S'_def W_def) have "W ⊆ T'" by (simp add: Collect_mono T'_def W_def) have ST_W: "S ∩ T ⊆ W" and "W ⊆ U" using ‹S ⊆ U› by (force simp: W_def setdist_sing_in_set)+ have "S' ∩ T' = W" by (auto simp: S'_def T'_def W_def) then have cloUW: "closedin (top_of_set U) W" using closedin_Int cloUS' cloUT' by blast obtain W' W0 where "openin (top_of_set W) W'" and cloWW0: "closedin (top_of_set W) W0" and "S ∩ T ⊆ W'" "W' ⊆ W0" and ret: "(S ∩ T) retract_of W0" by (meson ANR_imp_closed_neighbourhood_retract ST_W US UT ‹W ⊆ U› ‹ANR(S ∩ T)› closedin_Int closedin_subset_trans) then obtain U0 where opeUU0: "openin (top_of_set U) U0" and U0: "S ∩ T ⊆ U0" "U0 ∩ W ⊆ W0" unfolding openin_open using ‹W ⊆ U› by blast have "W0 ⊆ U" using ‹W ⊆ U› cloWW0 closedin_subset by fastforce obtain r0 where "S ∩ T ⊆ W0" and contr0: "continuous_on W0 r0" and "r0 ∈ W0 → S ∩ T" and r0 [simp]: "⋀x. x ∈ S ∩ T ⟹ r0 x = x" using ret by (force simp: retract_of_def retraction_def) have ST: "x ∈ W ⟹ x ∈ S ⟷ x ∈ T" for x using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin) define r where "r ≡ λx. if x ∈ W0 then r0 x else x" have "r ` (W0 ∪ S) ⊆ S" "r ` (W0 ∪ T) ⊆ T" using ‹r0 ∈ W0 → S ∩ T› r_def by auto have contr: "continuous_on (W0 ∪ (S ∪ T)) r" unfolding r_def proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id]) show "closedin (top_of_set (W0 ∪ (S ∪ T))) W0" using closedin_subset_trans [of U] by (metis le_sup_iff order_refl cloWW0 cloUW closedin_trans ‹W0 ⊆ U› ‹S ⊆ U› ‹T ⊆ U›) show "closedin (top_of_set (W0 ∪ (S ∪ T))) (S ∪ T)" by (meson ‹S ⊆ U› ‹T ⊆ U› ‹W0 ⊆ U› assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2) show "⋀x. x ∈ W0 ∧ x ∉ W0 ∨ x ∈ S ∪ T ∧ x ∈ W0 ⟹ r0 x = x" using ST cloWW0 closedin_subset by fastforce qed have cloS'WS: "closedin (top_of_set S') (W0 ∪ S)" by (meson closedin_subset_trans US cloUS' ‹S ⊆ S'› ‹W ⊆ S'› cloUW cloWW0 closedin_Un closedin_imp_subset closedin_trans) obtain W1 g where "W0 ∪ S ⊆ W1" and contg: "continuous_on W1 g" and opeSW1: "openin (top_of_set S') W1" and "g ∈ W1 → S" and geqr: "⋀x. x ∈ W0 ∪ S ⟹ g x = r x" proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› _ _ cloS'WS]) show "continuous_on (W0 ∪ S) r" using continuous_on_subset contr sup_assoc by blast qed (use ‹r ` (W0 ∪ S) ⊆ S› in auto) have cloT'WT: "closedin (top_of_set T') (W0 ∪ T)" by (meson closedin_subset_trans UT cloUT' ‹T ⊆ T'› ‹W ⊆ T'› cloUW cloWW0 closedin_Un closedin_imp_subset closedin_trans) obtain W2 h where "W0 ∪ T ⊆ W2" and conth: "continuous_on W2 h" and opeSW2: "openin (top_of_set T') W2" and "h ` W2 ⊆ T" and heqr: "⋀x. x ∈ W0 ∪ T ⟹ h x = r x" proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› _ _ cloT'WT]) show "continuous_on (W0 ∪ T) r" using continuous_on_subset contr sup_assoc by blast qed (use ‹r ` (W0 ∪ T) ⊆ T› in auto) have "S' ∩ T' = W" by (force simp: S'_def T'_def W_def) obtain O1 O2 where O12: "open O1" "W1 = S' ∩ O1" "open O2" "W2 = T' ∩ O2" using opeSW1 opeSW2 by (force simp: openin_open) show ?thesis proof have eq: "W1 - (W - U0) ∪ (W2 - (W - U0)) = ((U - T') ∩ O1 ∪ (U - S') ∩ O2 ∪ U ∩ O1 ∩ O2) - (W - U0)" (is "?WW1 ∪ ?WW2 = ?rhs") using ‹U0 ∩ W ⊆ W0› ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› by (auto simp: ‹S' ∪ T' = U› [symmetric] ‹S' ∩ T' = W› [symmetric] ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2›) show "openin (top_of_set U) (?WW1 ∪ ?WW2)" by (simp add: eq ‹open O1› ‹open O2› cloUS' cloUT' cloUW closedin_diff opeUU0 openin_Int_open openin_Un openin_diff) obtain SU' where "closed SU'" "S' = U ∩ SU'" using cloUS' by (auto simp add: closedin_closed) moreover have "?WW1 = (?WW1 ∪ ?WW2) ∩ SU'" using ‹S' = U ∩ SU'› ‹W1 = S' ∩ O1› ‹S' ∪ T' = U› ‹W2 = T' ∩ O2› ‹S' ∩ T' = W› ‹W0 ∪ S ⊆ W1› U0 by auto ultimately have cloW1: "closedin (top_of_set (W1 - (W - U0) ∪ (W2 - (W - U0)))) (W1 - (W - U0))" by (metis closedin_closed_Int) obtain TU' where "closed TU'" "T' = U ∩ TU'" using cloUT' by (auto simp add: closedin_closed) moreover have "?WW2 = (?WW1 ∪ ?WW2) ∩ TU'" using ‹T' = U ∩ TU'› ‹W1 = S' ∩ O1› ‹S' ∪ T' = U› ‹W2 = T' ∩ O2› ‹S' ∩ T' = W› ‹W0 ∪ T ⊆ W2› U0 by auto ultimately have cloW2: "closedin (top_of_set (?WW1 ∪ ?WW2)) ?WW2" by (metis closedin_closed_Int) let ?gh = "λx. if x ∈ S' then g x else h x" have "∃r. continuous_on (?WW1 ∪ ?WW2) r ∧ r ` (?WW1 ∪ ?WW2) ⊆ S ∪ T ∧ (∀x∈S ∪ T. r x = x)" proof (intro exI conjI) show "∀x∈S ∪ T. ?gh x = x" using ST ‹S' ∩ T' = W› geqr heqr O12 by (metis Int_iff Un_iff ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› r0 r_def sup.order_iff) have "⋀x. x ∈ ?WW1 ∧ x ∉ S' ∨ x ∈ ?WW2 ∧ x ∈ S' ⟹ g x = h x" using O12 by (metis (full_types) DiffD1 DiffD2 DiffI IntE IntI U0(2) UnCI ‹S' ∩ T' = W› geqr heqr in_mono) then show "continuous_on (?WW1 ∪ ?WW2) ?gh" using continuous_on_cases_local [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]] by simp show "?gh ` (?WW1 ∪ ?WW2) ⊆ S ∪ T" using ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2› ‹S' ∩ T' = W› ‹g ∈ W1 → S› ‹h ` W2 ⊆ T› ‹U0 ∩ W ⊆ W0› ‹W0 ∪ S ⊆ W1› by (auto simp add: image_subset_iff) qed then show "S ∪ T retract_of ?WW1 ∪ ?WW2" using ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› ST opeUU0 U0 by (auto simp: retract_of_def retraction_def image_subset_iff_funcset) qed qed lemma ANR_closed_Un_local: fixes S :: "'a::euclidean_space set" assumes STS: "closedin (top_of_set (S ∪ T)) S" and STT: "closedin (top_of_set (S ∪ T)) T" and "ANR S" "ANR T" "ANR(S ∩ T)" shows "ANR(S ∪ T)" proof - have "∃T. openin (top_of_set U) T ∧ C retract_of T" if hom: "S ∪ T homeomorphic C" and UC: "closedin (top_of_set U) C" for U and C :: "('a * real) set" proof - obtain f g where hom: "homeomorphism (S ∪ T) C f g" using hom by (force simp: homeomorphic_def) have US: "closedin (top_of_set U) (C ∩ g -` S)" by (metis STS UC closedin_trans continuous_on_imp_closedin hom homeomorphism_def) have UT: "closedin (top_of_set U) (C ∩ g -` T)" by (metis STT UC closedin_trans continuous_on_imp_closedin hom homeomorphism_def) have "homeomorphism (C ∩ g -` S) S g f" using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) by (rule_tac x="f x" in image_eqI, auto) then have ANRS: "ANR (C ∩ g -` S)" using ‹ANR S› homeomorphic_ANR_iff_ANR homeomorphic_def by blast have "homeomorphism (C ∩ g -` T) T g f" using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) by (rule_tac x="f x" in image_eqI, auto) then have ANRT: "ANR (C ∩ g -` T)" using ‹ANR T› homeomorphic_ANR_iff_ANR homeomorphic_def by blast have "homeomorphism (C ∩ g -` S ∩ (C ∩ g -` T)) (S ∩ T) g f" using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) by (rule_tac x="f x" in image_eqI, auto) then have ANRI: "ANR ((C ∩ g -` S) ∩ (C ∩ g -` T))" using ‹ANR (S ∩ T)› homeomorphic_ANR_iff_ANR homeomorphic_def by blast have "C = (C ∩ g -` S) ∪ (C ∩ g -` T)" using hom by (auto simp: homeomorphism_def) then show ?thesis by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI]) qed then show ?thesis by (auto simp: ANR_def) qed corollary ANR_closed_Un: fixes S :: "'a::euclidean_space set" shows "⟦closed S; closed T; ANR S; ANR T; ANR (S ∩ T)⟧ ⟹ ANR (S ∪ T)" by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int) lemma ANR_openin: fixes S :: "'a::euclidean_space set" assumes "ANR T" and opeTS: "openin (top_of_set T) S" shows "ANR S" proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor) fix f :: "'a × real ⇒ 'a" and U C assume contf: "continuous_on C f" and fim: "f ∈ C → S" and cloUC: "closedin (top_of_set U) C" have "f ∈ C → T" using fim opeTS openin_imp_subset by blast obtain W g where "C ⊆ W" and UW: "openin (top_of_set U) W" and contg: "continuous_on W g" and gim: "g ∈ W → T" and geq: "⋀x. x ∈ C ⟹ g x = f x" using ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf ‹f ∈ C → T› cloUC] fim by auto show "∃V g. C ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ∈ V → S ∧ (∀x∈C. g x = f x)" proof (intro exI conjI) show "C ⊆ W ∩ g -` S" using ‹C ⊆ W› fim geq by blast show "openin (top_of_set U) (W ∩ g -` S)" by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans) show "continuous_on (W ∩ g -` S) g" by (blast intro: continuous_on_subset [OF contg]) show "g ∈ (W ∩ g -` S) → S" using gim by blast show "∀x∈C. g x = f x" using geq by blast qed qed lemma ENR_openin: fixes S :: "'a::euclidean_space set" assumes "ENR T" "openin (top_of_set T) S" shows "ENR S" by (meson ANR_openin ENR_ANR assms locally_open_subset) lemma ANR_neighborhood_retract: fixes S :: "'a::euclidean_space set" assumes "ANR U" "S retract_of T" "openin (top_of_set U) T" shows "ANR S" using ANR_openin ANR_retract_of_ANR assms by blast lemma ENR_neighborhood_retract: fixes S :: "'a::euclidean_space set" assumes "ENR U" "S retract_of T" "openin (top_of_set U) T" shows "ENR S" using ENR_openin ENR_retract_of_ENR assms by blast lemma ANR_rel_interior: fixes S :: "'a::euclidean_space set" shows "ANR S ⟹ ANR(rel_interior S)" by (blast intro: ANR_openin openin_set_rel_interior) lemma ANR_delete: fixes S :: "'a::euclidean_space set" shows "ANR S ⟹ ANR(S - {a})" by (blast intro: ANR_openin openin_delete openin_subtopology_self) lemma ENR_rel_interior: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ ENR(rel_interior S)" by (blast intro: ENR_openin openin_set_rel_interior) lemma ENR_delete: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ ENR(S - {a})" by (blast intro: ENR_openin openin_delete openin_subtopology_self) lemma open_imp_ENR: "open S ⟹ ENR S" using ENR_def by blast lemma open_imp_ANR: fixes S :: "'a::euclidean_space set" shows "open S ⟹ ANR S" by (simp add: ENR_imp_ANR open_imp_ENR) lemma ANR_ball [iff]: fixes a :: "'a::euclidean_space" shows "ANR(ball a r)" by (simp add: convex_imp_ANR) lemma ENR_ball [iff]: "ENR(ball a r)" by (simp add: open_imp_ENR) lemma AR_ball [simp]: fixes a :: "'a::euclidean_space" shows "AR(ball a r) ⟷ 0 < r" by (auto simp: AR_ANR convex_imp_contractible) lemma ANR_cball [iff]: fixes a :: "'a::euclidean_space" shows "ANR(cball a r)" by (simp add: convex_imp_ANR) lemma ENR_cball: fixes a :: "'a::euclidean_space" shows "ENR(cball a r)" using ENR_convex_closed by blast lemma AR_cball [simp]: fixes a :: "'a::euclidean_space" shows "AR(cball a r) ⟷ 0 ≤ r" by (auto simp: AR_ANR convex_imp_contractible) lemma ANR_box [iff]: fixes a :: "'a::euclidean_space" shows "ANR(cbox a b)" "ANR(box a b)" by (auto simp: convex_imp_ANR open_imp_ANR) lemma ENR_box [iff]: fixes a :: "'a::euclidean_space" shows "ENR(cbox a b)" "ENR(box a b)" by (simp_all add: ENR_convex_closed closed_cbox open_box open_imp_ENR) lemma AR_box [simp]: "AR(cbox a b) ⟷ cbox a b ≠ {}" "AR(box a b) ⟷ box a b ≠ {}" by (auto simp: AR_ANR convex_imp_contractible) lemma ANR_interior: fixes S :: "'a::euclidean_space set" shows "ANR(interior S)" by (simp add: open_imp_ANR) lemma ENR_interior: fixes S :: "'a::euclidean_space set" shows "ENR(interior S)" by (simp add: open_imp_ENR) lemma AR_imp_contractible: fixes S :: "'a::euclidean_space set" shows "AR S ⟹ contractible S" by (simp add: AR_ANR) lemma ENR_imp_locally_compact: fixes S :: "'a::euclidean_space set" shows "ENR S ⟹ locally compact S" by (simp add: ENR_ANR) lemma ANR_imp_locally_path_connected: fixes S :: "'a::euclidean_space set" assumes "ANR S" shows "locally path_connected S" proof - obtain U and T :: "('a × real) set" where "convex U" "U ≠ {}" and UT: "closedin (top_of_set U) T" and "S homeomorphic T" proof (rule homeomorphic_closedin_convex) show "aff_dim S < int DIM('a × real)" using aff_dim_le_DIM [of S] by auto qed auto then have "locally path_connected T" by (meson ANR_imp_absolute_neighbourhood_retract assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected) then have S: "locally path_connected S" if "openin (top_of_set U) V" "T retract_of V" "U ≠ {}" for V using ‹S homeomorphic T› homeomorphic_locally homeomorphic_path_connectedness by blast obtain Ta where "(openin (top_of_set U) Ta ∧ T retract_of Ta)" using ANR_def UT ‹S homeomorphic T› assms by atomize_elim (auto simp: choice) then show ?thesis using S ‹U ≠ {}› by blast qed lemma ANR_imp_locally_connected: fixes S :: "'a::euclidean_space set" assumes "ANR S" shows "locally connected S" using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto lemma AR_imp_locally_path_connected: fixes S :: "'a::euclidean_space set" assumes "AR S" shows "locally path_connected S" by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms) lemma AR_imp_locally_connected: fixes S :: "'a::euclidean_space set" assumes "AR S" shows "locally connected S" using ANR_imp_locally_connected AR_ANR assms by blast lemma ENR_imp_locally_path_connected: fixes S :: "'a::euclidean_space set" assumes "ENR S" shows "locally path_connected S" by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms) lemma ENR_imp_locally_connected: fixes S :: "'a::euclidean_space set" assumes "ENR S" shows "locally connected S" using ANR_imp_locally_connected ENR_ANR assms by blast lemma ANR_Times: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "ANR S" "ANR T" shows "ANR(S × T)" proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor) fix f :: " ('a × 'b) × real ⇒ 'a × 'b" and U C assume "continuous_on C f" and fim: "f ∈ C → S × T" and cloUC: "closedin (top_of_set U) C" have contf1: "continuous_on C (fst ∘ f)" by (simp add: ‹continuous_on C f› continuous_on_fst) obtain W1 g where "C ⊆ W1" and UW1: "openin (top_of_set U) W1" and contg: "continuous_on W1 g" and gim: "g ` W1 ⊆ S" and geq: "⋀x. x ∈ C ⟹ g x = (fst ∘ f) x" proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› contf1 _ cloUC]) show "(fst ∘ f) ∈ C → S" using fim by force qed auto have contf2: "continuous_on C (snd ∘ f)" by (simp add: ‹continuous_on C f› continuous_on_snd) obtain W2 h where "C ⊆ W2" and UW2: "openin (top_of_set U) W2" and conth: "continuous_on W2 h" and him: "h ∈ W2 → T" and heq: "⋀x. x ∈ C ⟹ h x = (snd ∘ f) x" proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf2 _ cloUC]) show "(snd ∘ f) ∈ C → T" using fim by force qed auto show "∃V g. C ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ∈ V → S × T ∧ (∀x∈C. g x = f x)" proof (intro exI conjI) show "C ⊆ W1 ∩ W2" by (simp add: ‹C ⊆ W1› ‹C ⊆ W2›) show "openin (top_of_set U) (W1 ∩ W2)" by (simp add: UW1 UW2 openin_Int) show "continuous_on (W1 ∩ W2) (λx. (g x, h x))" by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1) show "(λx. (g x, h x)) ∈ (W1 ∩ W2) → S × T" using gim him by blast show "(∀x∈C. (g x, h x) = f x)" using geq heq by auto qed qed lemma AR_Times: fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" assumes "AR S" "AR T" shows "AR(S × T)" using assms by (simp add: AR_ANR ANR_Times contractible_Times) (* Unused and requires ordered_euclidean_space subsection✐‹tag unimportant›‹Retracts and intervals in ordered euclidean space› lemma ANR_interval [iff]: fixes a :: "'a::ordered_euclidean_space" shows "ANR{a..b}" by (simp add: interval_cbox) lemma ENR_interval [iff]: fixes a :: "'a::ordered_euclidean_space" shows "ENR{a..b}" by (auto simp: interval_cbox) *) subsection ‹More advanced properties of ANRs and ENRs› lemma ENR_rel_frontier_convex: fixes S :: "'a::euclidean_space set" assumes "bounded S" "convex S" shows "ENR(rel_frontier S)" proof (cases "S = {}") case True then show ?thesis by simp next case False with assms have "rel_interior S ≠ {}" by (simp add: rel_interior_eq_empty) then obtain a where a: "a ∈ rel_interior S" by auto have ahS: "affine hull S - {a} ⊆ {x. closest_point (affine hull S) x ≠ a}" by (auto simp: closest_point_self) have "rel_frontier S retract_of affine hull S - {a}" by (simp add: assms a rel_frontier_retract_of_punctured_affine_hull) also have "… retract_of {x. closest_point (affine hull S) x ≠ a}" unfolding retract_of_def retraction_def ahS apply (rule_tac x="closest_point (affine hull S)" in exI) apply (auto simp: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point) done finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x ≠ a}" . moreover have "openin (top_of_set UNIV) (UNIV ∩ closest_point (affine hull S) -` (- {a}))" by (intro continuous_openin_preimage_gen) (auto simp: False affine_imp_convex continuous_on_closest_point) ultimately show ?thesis by (meson ENR_convex_closed ENR_delete ENR_retract_of_ENR ‹rel_frontier S retract_of affine hull S - {a}› closed_affine_hull convex_affine_hull) qed lemma ANR_rel_frontier_convex: fixes S :: "'a::euclidean_space set" assumes "bounded S" "convex S" shows "ANR(rel_frontier S)" by (simp add: ENR_imp_ANR ENR_rel_frontier_convex assms) lemma ENR_closedin_Un_local: fixes S :: "'a::euclidean_space set" shows "⟦ENR S; ENR T; ENR(S ∩ T); closedin (top_of_set (S ∪ T)) S; closedin (top_of_set (S ∪ T)) T⟧ ⟹ ENR(S ∪ T)" by (simp add: ENR_ANR ANR_closed_Un_local locally_compact_closedin_Un) lemma ENR_closed_Un: fixes S :: "'a::euclidean_space set" shows "⟦closed S; closed T; ENR S; ENR T; ENR(S ∩ T)⟧ ⟹ ENR(S ∪ T)" by (auto simp: closed_subset ENR_closedin_Un_local) lemma absolute_retract_Un: fixes S :: "'a::euclidean_space set" shows "⟦S retract_of UNIV; T retract_of UNIV; (S ∩ T) retract_of UNIV⟧ ⟹ (S ∪ T) retract_of UNIV" by (meson AR_closed_Un_local_aux closed_subset retract_of_UNIV retract_of_imp_subset) lemma retract_from_Un_Int: fixes S :: "'a::euclidean_space set" assumes clS: "closedin (top_of_set (S ∪ T)) S" and clT: "closedin (top_of_set (S ∪ T)) T" and Un: "(S ∪ T) retract_of U" and Int: "(S ∩ T) retract_of T" shows "S retract_of U" proof - obtain r where r: "continuous_on T r" "r ` T ⊆ S ∩ T" "∀x∈S ∩ T. r x = x" using Int by (auto simp: retraction_def retract_of_def) have "S retract_of S ∪ T" unfolding retraction_def retract_of_def proof (intro exI conjI) show "continuous_on (S ∪ T) (λx. if x ∈ S then x else r x)" using r by (intro continuous_on_cases_local [OF clS clT]) auto qed (use r in auto) also have "… retract_of U" by (rule Un) finally show ?thesis . qed lemma AR_from_Un_Int_local: fixes S :: "'a::euclidean_space set" assumes clS: "closedin (top_of_set (S ∪ T)) S" and clT: "closedin (top_of_set (S ∪ T)) T" and Un: "AR(S ∪ T)" and Int: "AR(S ∩ T)" shows "AR S" by (meson AR_imp_retract AR_retract_of_AR Un assms closedin_closed_subset local.Int retract_from_Un_Int retract_of_refl sup_ge2) lemma AR_from_Un_Int_local': fixes S :: "'a::euclidean_space set" assumes "closedin (top_of_set (S ∪ T)) S" and "closedin (top_of_set (S ∪ T)) T" and "AR(S ∪ T)" "AR(S ∩ T)" shows "AR T" using AR_from_Un_Int_local [of T S] assms by (simp add: Un_commute Int_commute) lemma AR_from_Un_Int: fixes S :: "'a::euclidean_space set" assumes clo: "closed S" "closed T" and Un: "AR(S ∪ T)" and Int: "AR(S ∩ T)" shows "AR S" by (metis AR_from_Un_Int_local [OF _ _ Un Int] Un_commute clo closed_closedin closedin_closed_subset inf_sup_absorb subtopology_UNIV top_greatest) lemma ANR_from_Un_Int_local: fixes S :: "'a::euclidean_space set" assumes clS: "closedin (top_of_set (S ∪ T)) S" and clT: "closedin (top_of_set (S ∪ T)) T" and Un: "ANR(S ∪ T)" and Int: "ANR(S ∩ T)" shows "ANR S" proof - obtain V where clo: "closedin (top_of_set (S ∪ T)) (S ∩ T)" and ope: "openin (top_of_set (S ∪ T)) V" and ret: "S ∩ T retract_of V" using ANR_imp_neighbourhood_retract [OF Int] by (metis clS clT closedin_Int) then obtain r where r: "continuous_on V r" and rim: "r ` V ⊆ S ∩ T" and req: "∀x∈S ∩ T. r x = x" by (auto simp: retraction_def retract_of_def) have Vsub: "V ⊆ S ∪ T" by (meson ope openin_contains_cball) have Vsup: "S ∩ T ⊆ V" by (simp add: retract_of_imp_subset ret) then have eq: "S ∪ V = ((S ∪ T) - T) ∪ V" by auto have eq': "S ∪ V = S ∪ (V ∩ T)" using Vsub by blast have "continuous_on (S ∪ V ∩ T) (λx. if x ∈ S then x else r x)" proof (rule continuous_on_cases_local) show "closedin (top_of_set (S ∪ V ∩ T)) S" using clS closedin_subset_trans inf.boundedE by blast show "closedin (top_of_set (S ∪ V ∩ T)) (V ∩ T)" using clT Vsup by (auto simp: closedin_closed) show "continuous_on (V ∩ T) r" by (meson