section \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
theory Retracts
imports
Brouwer_Fixpoint
Continuous_Extension
begin
text \<open>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 \<open>\<real>\<^sup>n\<close> can be
embedded as a closed subset of a convex subset of \<open>\<real>\<^sup>n\<^sup>+\<^sup>1\<close>) 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."\<close>
definition\<^marker>\<open>tag important\<close> AR :: "'a::topological_space set \<Rightarrow> bool" where
"AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
S homeomorphic S' \<and> closedin (top_of_set U) S' \<longrightarrow> S' retract_of U"
definition\<^marker>\<open>tag important\<close> ANR :: "'a::topological_space set \<Rightarrow> bool" where
"ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set.
S homeomorphic S' \<and> closedin (top_of_set U) S'
\<longrightarrow> (\<exists>T. openin (top_of_set U) T \<and> S' retract_of T)"
definition\<^marker>\<open>tag important\<close> ENR :: "'a::topological_space set \<Rightarrow> bool" where
"ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
text \<open>First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
lemma AR_imp_absolute_extensor:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "AR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
and cloUT: "closedin (top_of_set U) T"
obtains g where "continuous_on U g" "g ` U \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
proof -
have "aff_dim S < int (DIM('b \<times> real))"
using aff_dim_le_DIM [of S] by simp
then obtain C and S' :: "('b * real) set"
where C: "convex C" "C \<noteq> {}"
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 \<open>AR S\<close> by (simp add: AR_def)
then obtain r where "S' \<subseteq> C" and contr: "continuous_on C r"
and "r ` C \<subseteq> S'" and rid: "\<And>x. x\<in>S' \<Longrightarrow> 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 \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
then have contgf: "continuous_on T (g \<circ> f)"
by (metis continuous_on_compose contf)
have gfTC: "(g \<circ> f) ` T \<subseteq> C"
proof -
have "g ` S = S'"
by (metis (no_types) \<open>homeomorphism S S' g h\<close> homeomorphism_def)
with \<open>S' \<subseteq> C\<close> \<open>f ` T \<subseteq> S\<close> show ?thesis by force
qed
obtain f' where f': "continuous_on U f'" "f' ` U \<subseteq> C"
"\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
by (metis Dugundji [OF C cloUT contgf gfTC])
show ?thesis
proof (rule_tac g = "h \<circ> r \<circ> f'" in that)
show "continuous_on U (h \<circ> r \<circ> 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 \<open>homeomorphism S S' g h\<close> \<open>f' ` U \<subseteq> C\<close>
unfolding homeomorphism_def
by (metis \<open>r ` C \<subseteq> S'\<close> continuous_on_subset image_mono)
qed
show "(h \<circ> r \<circ> f') ` U \<subseteq> S"
using \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> \<open>f' ` U \<subseteq> C\<close>
by (fastforce simp: homeomorphism_def)
show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> 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' \<subseteq> S"
using hom homeomorphism_def by blast
obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
and h'h: "\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
by (blast intro: AR_imp_absolute_extensor [OF \<open>AR S\<close> h clo])
have [simp]: "S' \<subseteq> 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 \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
show "(g \<circ> h') ` U \<subseteq> S'"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>S'. (g \<circ> 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 "\<And>f :: 'a * real \<Rightarrow> 'a.
\<And>U T. \<lbrakk>continuous_on T f; f ` T \<subseteq> S;
closedin (top_of_set U) T\<rbrakk>
\<Longrightarrow> \<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> 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 \<subseteq> S"
using hom homeomorphism_def by blast
obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
and h'h: "\<forall>x\<in>T. h' x = h x"
using assms [OF h clo] by blast
have [simp]: "T \<subseteq> 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 \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
show "(g \<circ> h') ` U \<subseteq> T"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>T. (g \<circ> 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 \<longleftrightarrow>
(\<forall>f :: 'a * real \<Rightarrow> 'a.
\<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
closedin (top_of_set U) T \<longrightarrow>
(\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> 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 \<and> 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 \<Longrightarrow> AR S \<longleftrightarrow> AR T"
by (metis AR_homeomorphic_AR homeomorphic_sym)
lemma ANR_imp_absolute_neighbourhood_extensor:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
and cloUT: "closedin (top_of_set U) T"
obtains V g where "T \<subseteq> V" "openin (top_of_set U) V"
"continuous_on V g"
"g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
proof -
have "aff_dim S < int (DIM('b \<times> real))"
using aff_dim_le_DIM [of S] by simp
then obtain C and S' :: "('b * real) set"
where C: "convex C" "C \<noteq> {}"
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 \<open>ANR S\<close> by (auto simp: ANR_def)
then obtain r where "S' \<subseteq> D" and contr: "continuous_on D r"
and "r ` D \<subseteq> S'" and rid: "\<And>x. x \<in> S' \<Longrightarrow> 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 (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
then have contgf: "continuous_on T (g \<circ> f)"
by (intro continuous_on_compose contf)
have gfTC: "(g \<circ> f) ` T \<subseteq> C"
proof -
have "g ` S = S'"
by (metis (no_types) homeomorphism_def homgh)
then show ?thesis
by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology)
qed
obtain f' where contf': "continuous_on U f'"
and "f' ` U \<subseteq> C"
and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
by (metis Dugundji [OF C cloUT contgf gfTC])
show ?thesis
proof (rule_tac V = "U \<inter> f' -` D" and g = "h \<circ> r \<circ> f'" in that)
show "T \<subseteq> U \<inter> f' -` D"
using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
by fastforce
show ope: "openin (top_of_set U) (U \<inter> f' -` D)"
using \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
have conth: "continuous_on (r ` f' ` (U \<inter> f' -` D)) h"
proof (rule continuous_on_subset [of S'])
show "continuous_on S' h"
using homeomorphism_def homgh by blast
qed (use \<open>r ` D \<subseteq> S'\<close> in blast)
show "continuous_on (U \<inter> f' -` D) (h \<circ> r \<circ> f')"
by (blast intro: continuous_on_compose conth continuous_on_subset [OF contr] continuous_on_subset [OF contf'])
show "(h \<circ> r \<circ> f') ` (U \<inter> f' -` D) \<subseteq> S"
using \<open>homeomorphism S S' g h\<close> \<open>f' ` U \<subseteq> C\<close> \<open>r ` D \<subseteq> S'\<close>
by (auto simp: homeomorphism_def)
show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> eq
by (auto simp: rid homeomorphism_def)
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' \<subseteq> S"
using hom homeomorphism_def by blast
from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
obtain V h' where "S' \<subseteq> V" and opUV: "openin (top_of_set U) V"
and h': "continuous_on V h'" "h' ` V \<subseteq> S"
and h'h:"\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
have "S' retract_of V"
proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
show "continuous_on V (g \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h'(1) h'(2) hom homeomorphism_cont1)
show "(g \<circ> h') ` V \<subseteq> S'"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>S'. (g \<circ> 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 \<open>ANR S\<close> hom]
by (metis clo closed_closedin open_openin subtopology_UNIV)
corollary neighbourhood_extension_into_ANR:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes contf: "continuous_on S f" and fim: "f ` S \<subseteq> T" and "ANR T" "closed S"
obtains V g where "S \<subseteq> V" "open V" "continuous_on V g"
"g ` V \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
using ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> contf fim]
by (metis \<open>closed S\<close> closed_closedin open_openin subtopology_UNIV)
lemma absolute_neighbourhood_extensor_imp_ANR:
fixes S :: "'a::euclidean_space set"
assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
\<And>U T. \<lbrakk>continuous_on T f; f ` T \<subseteq> S;
closedin (top_of_set U) T\<rbrakk>
\<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (top_of_set U) V \<and>
continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> 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 \<subseteq> S"
using hom homeomorphism_def by blast
obtain V h' where "T \<subseteq> V" and opV: "openin (top_of_set U) V"
and h': "continuous_on V h'" "h' ` V \<subseteq> S"
and h'h: "\<forall>x\<in>T. h' x = h x"
using assms [OF h clo] by blast
have [simp]: "T \<subseteq> U"
using clo closedin_imp_subset by auto
have "T retract_of V"
proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
show "continuous_on V (g \<circ> h')"
by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
show "(g \<circ> h') ` V \<subseteq> T"
using h' by clarsimp (metis hom subsetD homeomorphism_def imageI)
show "\<forall>x\<in>T. (g \<circ> h') x = x"
by clarsimp (metis h'h hom homeomorphism_def)
qed
then show "\<exists>V. openin (top_of_set U) V \<and> T retract_of V"
using opV by blast
qed
lemma ANR_eq_absolute_neighbourhood_extensor:
fixes S :: "'a::euclidean_space set"
shows "ANR S \<longleftrightarrow>
(\<forall>f :: 'a * real \<Rightarrow> 'a.
\<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
closedin (top_of_set U) T \<longrightarrow>
(\<exists>V g. T \<subseteq> V \<and> openin (top_of_set U) V \<and>
continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> 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' \<subseteq> V" "V \<subseteq> 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' \<inter> (U - Z) = {}"
using \<open>S' retract_of Z\<close> 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' \<subseteq> V" "U - Z \<subseteq> W" "V \<inter> 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' \<subseteq> U - W"
using US' \<open>S' \<subseteq> V\<close> \<open>V \<inter> W = {}\<close> closedin_subset by fastforce
show "U - W \<subseteq> Z"
using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> 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 \<subseteq> V" "V \<subseteq> 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 \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
by (metis ANR_homeomorphic_ANR homeomorphic_sym)
subsection \<open>Analogous properties of ENRs\<close>
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' \<subseteq> 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 \<open>ENR S\<close> 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 \<open>S retract_of X\<close> \<open>open X\<close> 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' \<subseteq> S" by (metis hom equalityE homeomorphism_def)
ultimately obtain h where conth: "continuous_on W h" and hg: "\<And>x. x \<in> S' \<Longrightarrow> h x = g x"
using Tietze_unbounded [of S' g W] WS' by blast
have "W \<subseteq> U" using UW openin_open by auto
have "S' \<subseteq> W" using WS' closedin_closed by auto
have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
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)
have "S' retract_of (W \<inter> h -` X)"
proof (simp add: retraction_def retract_of_def, intro exI conjI)
show "S' \<subseteq> W" "S' \<subseteq> h -` X"
using him WS' closedin_imp_subset by blast+
show "continuous_on (W \<inter> h -` X) (f \<circ> r \<circ> h)"
proof (intro continuous_on_compose)
show "continuous_on (W \<inter> h -` X) h"
by (meson conth continuous_on_subset inf_le1)
show "continuous_on (h ` (W \<inter> h -` X)) r"
proof -
have "h ` (W \<inter> h -` X) \<subseteq> X"
by blast
then show "continuous_on (h ` (W \<inter> h -` X)) r"
by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
qed
show "continuous_on (r ` h ` (W \<inter> 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 \<inter> h -` X) \<subseteq> S"
by (metis \<open>retraction X S r\<close> image_mono image_subset_iff_subset_vimage inf_le2 retraction)
qed
qed
show "(f \<circ> r \<circ> h) ` (W \<inter> h -` X) \<subseteq> S'"
using \<open>retraction X S r\<close> hom
by (auto simp: retraction_def homeomorphism_def)
show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
qed
then show ?thesis
using UW \<open>open X\<close> 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 \<longleftrightarrow> ENR T"
by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)
lemma ENR_translation:
fixes S :: "'a::euclidean_space set"
shows "ENR(image (\<lambda>x. a + x) S) \<longleftrightarrow> ENR S"
by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)
lemma ENR_linear_image_eq:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes "linear f" "inj f"
shows "ENR (image f S) \<longleftrightarrow> ENR S"
by (meson assms homeomorphic_ENR_iff_ENR linear_homeomorphic_image)
text \<open>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.\<close>
lemma AR_imp_ANR: "AR S \<Longrightarrow> ANR S"
using ANR_def AR_def by fastforce
lemma ENR_imp_ANR:
fixes S :: "'a::euclidean_space set"
shows "ENR S \<Longrightarrow> 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 \<longleftrightarrow> ANR S \<and> 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 \<and> locally compact S"
using ENR_imp_ANR \<open>ENR S\<close> by blast
next
assume "ANR S \<and> 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 \<open>ANR S\<close>
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 \<longleftrightarrow> ANR S \<and> contractible S \<and> S \<noteq> {}"
(is "?lhs = ?rhs")
proof
assume ?lhs
have "aff_dim S < int DIM('a \<times> real)"
using aff_dim_le_DIM [of S] by auto
then obtain C and S' :: "('a * real) set"
where "convex C" "C \<noteq> {}" "closedin (top_of_set C) S'" "S homeomorphic S'"
using homeomorphic_closedin_convex by blast
with \<open>AR S\<close> have "contractible S"
by (meson AR_def convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible)
with \<open>AR S\<close> show ?rhs
using AR_imp_ANR AR_imp_retract by fastforce
next
assume ?rhs
then obtain a and h:: "real \<times> 'a \<Rightarrow> 'a"
where conth: "continuous_on ({0..1} \<times> S) h"
and hS: "h ` ({0..1} \<times> S) \<subseteq> S"
and [simp]: "\<And>x. h(0, x) = x"
and [simp]: "\<And>x. h(1, x) = a"
and "ANR S" "S \<noteq> {}"
by (auto simp: contractible_def homotopic_with_def)
then have "a \<in> S"
by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
if f: "continuous_on T f" "f ` T \<subseteq> S"
and WT: "closedin (top_of_set W) T"
for W T and f :: "'a \<times> real \<Rightarrow> 'a"
proof -
obtain U g
where "T \<subseteq> U" and WU: "openin (top_of_set W) U"
and contg: "continuous_on U g"
and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, 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) \<inter> T = {}"
using \<open>T \<subseteq> U\<close> 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 \<subseteq> V'" "T \<subseteq> V" "V' \<inter> V = {}"
using separation_normal_local [of W "W-U" T] WT by blast
then have WVT: "T \<inter> (W - V) = {}"
by auto
have WWV: "closedin (top_of_set W) (W - V)"
using WV closedin_diff by fastforce
obtain j :: " 'a \<times> real \<Rightarrow> real"
where contj: "continuous_on W j"
and j: "\<And>x. x \<in> W \<Longrightarrow> j x \<in> {0..1}"
and j0: "\<And>x. x \<in> W - V \<Longrightarrow> j x = 1"
and j1: "\<And>x. x \<in> T \<Longrightarrow> j x = 0"
by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
have Weq: "W = (W - V) \<union> (W - V')"
using \<open>V' \<inter> V = {}\<close> by force
show ?thesis
proof (intro conjI exI)
have *: "continuous_on (W - V') (\<lambda>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 \<open>W - U \<subseteq> V'\<close> contg continuous_on_subset Un_commute)
show "(\<lambda>x. (j x, g x)) ` (W - V') \<subseteq> {0..1} \<times> S"
using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> by fastforce
qed
show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
proof (subst Weq, rule continuous_on_cases_local)
show "continuous_on (W - V') (\<lambda>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)) \<in> S" if "(x, y) \<in> W" "(x, y) \<in> V" for x y
proof -
have "j(x, y) \<in> {0..1}"
using j that by blast
moreover have "g(x, y) \<in> S"
using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
ultimately show ?thesis
using hS by blast
qed
with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"