# HG changeset patch # User paulson # Date 1567607224 -3600 # Node ID de9c4ed2d5df9794f4ad8c5cd5dd50fa3167eb79 # Parent 0e2a065d6f315c90eb8d32e9e3b597395c408eb9 Half of Brouwer_Fixpoint split off to form a separate theory: Retracts. diff -r 0e2a065d6f31 -r de9c4ed2d5df src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Sep 04 14:16:27 2019 +0100 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Sep 04 15:27:04 2019 +0100 @@ -221,1323 +221,6 @@ qed qed -subsection \Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\ - -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 \\\<^sup>n\ can be -embedded as a closed subset of a convex subset of \\\<^sup>n\<^sup>+\<^sup>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\<^marker>\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\<^marker>\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\<^marker>\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')" - apply (intro continuous_on_compose f') - using continuous_on_subset contr f' apply blast - by (meson \homeomorphism S S' g h\ \r ` C \ S'\ continuous_on_subset \f' ` U \ C\ homeomorphism_def image_mono) - 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) - have h: "continuous_on S' h" " h ` S' \ S" - using hom homeomorphism_def apply blast - apply (metis hom equalityE homeomorphism_def) - done - 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')" - apply (intro continuous_on_compose h') - apply (meson hom continuous_on_subset h' homeomorphism_cont1) - done - 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" and hom: "S homeomorphic S'" - and clo: "closed S'" - shows "S' retract_of UNIV" -apply (rule AR_imp_absolute_retract [OF \AR S\ hom]) -using clo closed_closedin by auto - -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) - have h: "continuous_on T h" " h ` T \ S" - using hom homeomorphism_def apply blast - apply (metis hom equalityE homeomorphism_def) - done - 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')" - apply (intro continuous_on_compose h') - apply (meson hom continuous_on_subset h' homeomorphism_cont1) - done - 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)))" -apply (rule iffI) - apply (metis AR_imp_absolute_extensor) -apply (simp add: absolute_extensor_imp_AR) -done - -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 (meson \f ` T \ S\ continuous_on_subset homeomorphism_def homgh) - 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 (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 \ 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)" - using \f' ` U \ C\ by (auto simp: opD contf' continuous_openin_preimage) - have conth: "continuous_on (r ` f' ` (U \ f' -` D)) h" - apply (rule continuous_on_subset [of S']) - using homeomorphism_def homgh apply blast - using \r ` D \ S'\ by blast - show "continuous_on (U \ f' -` D) (h \ r \ f')" - apply (intro continuous_on_compose conth - continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto) - done - 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 (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) - have h: "continuous_on S' h" " h ` S' \ S" - using hom homeomorphism_def apply blast - apply (metis hom equalityE homeomorphism_def) - done - 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')" - apply (intro continuous_on_compose h') - apply (meson hom continuous_on_subset h' homeomorphism_cont1) - done - 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) - have h: "continuous_on T h" " h ` T \ S" - using hom homeomorphism_def apply blast - apply (metis hom equalityE homeomorphism_def) - done - 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')" - apply (intro continuous_on_compose h') - apply (meson hom continuous_on_subset h' homeomorphism_cont1) - done - show "(g \ h') ` V \ 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 - 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)))" -apply (rule iffI) - apply (metis ANR_imp_absolute_neighbourhood_extensor) -apply (simp add: absolute_neighbourhood_extensor_imp_ANR) -done - -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" - apply (rule retract_of_subset [OF S'Z]) - using US' \S' \ V\ \V \ W = {}\ closedin_subset apply fastforce - using Diff_subset_conv \U - Z \ W\ by blast - ultimately show ?thesis - apply (rule_tac V=V and W = "U-W" in that) - using openin_imp_subset apply force+ - done -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) - -subsubsection \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) - apply (rename_tac W) - apply (rule_tac W = "U \ W" in that, blast) - by (simp add: \S' \ U\ closedin_limpt) - 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" - apply (rule continuous_on_subset [of S]) - using hom homeomorphism_def apply blast - apply clarify - apply (meson \retraction X S r\ subsetD imageI retraction_def) - done - 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 - apply (rule_tac V = "W \ h -` X" in that) - apply (rule openin_trans [OF _ UW]) - using \continuous_on W h\ \open X\ continuous_openin_preimage_eq apply blast+ - done -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" -apply (rule homeomorphic_ENR_iff_ENR) -using assms homeomorphic_sym linear_homeomorphic_image by auto - -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" -apply (simp add: ANR_def) -by (metis 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\ - apply (simp add: ANR_def) - apply (drule_tac x=UNIV in spec) - apply (drule_tac x=T in spec, clarsimp) - apply (meson ENR_def ENR_homeomorphic_ENR open_openin) - done -qed - - -lemma AR_ANR: - fixes S :: "'a::euclidean_space set" - shows "AR S \ ANR S \ contractible S \ S \ {}" - (is "?lhs = ?rhs") -proof - assume ?lhs - obtain C and S' :: "('a * real) set" - where "convex C" "C \ {}" "closedin (top_of_set C) S'" "S homeomorphic S'" - apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"]) - using aff_dim_le_DIM [of S] by auto - with \AR S\ have "contractible S" - apply (simp add: AR_def) - apply (drule_tac x=C in spec) - apply (drule_tac x="S'" in spec, simp) - using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce - with \AR S\ show ?rhs - apply (auto simp: AR_imp_ANR) - apply (force simp: AR_def) - done -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))" - apply (rule continuous_on_compose2 [OF conth continuous_on_Pair]) - apply (rule continuous_on_subset [OF contj Diff_subset]) - apply (rule continuous_on_subset [OF contg]) - apply (metis Diff_subset_conv Un_commute \W - U \ V'\) - using j \g ` U \ S\ \W - U \ V'\ apply fastforce - done - show "continuous_on W (\x. if x \ W - V then a else h (j x, g x))" - apply (subst Weq) - apply (rule continuous_on_cases_local) - apply (simp_all add: Weq [symmetric] WWV continuous_on_const *) - using WV' closedin_diff apply fastforce - apply (auto simp: j0 j1) - done - 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) -qed - - -lemma ANR_retract_of_ANR: - fixes S :: "'a::euclidean_space set" - assumes "ANR T" "S retract_of T" - shows "ANR S" -using assms -apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def) -apply (clarsimp elim!: all_forward) -apply (erule impCE, metis subset_trans) -apply (clarsimp elim!: ex_forward) -apply (rule_tac x="r \ g" in exI) -by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans) - -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" -apply (rule absolute_extensor_imp_AR) -apply (rule Dugundji, assumption+) -by blast - -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" - apply (rule AR_imp_absolute_retract [OF \AR(S \ T)\]) - apply (simp add: homeomorphic_refl) - apply (rule closedin_subset_trans [of U]) - apply (simp_all add: assms closedin_Int \S \ T \ W\ \W \ U\) - done - 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 "r ` (W \ S) \ S" "r ` (W \ T) \ T" - using \r0 ` W \ S \ T\ r_def by auto - 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 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" - apply (rule AR_imp_absolute_extensor [OF \AR S\ _ _ cloUWS]) - apply (rule continuous_on_subset [OF contr]) - using \r ` (W \ S) \ S\ apply auto - done - 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" - apply (rule AR_imp_absolute_extensor [OF \AR T\ _ _ cloUWT]) - apply (rule continuous_on_subset [OF contr]) - using \r ` (W \ T) \ T\ apply auto - done - have "U = S' \ T'" - by (force simp: S'_def T'_def) - then have cont: "continuous_on U (\x. if x \ S' then g x else h x)" - apply (rule ssubst) - apply (rule continuous_on_cases_local) - using US' UT' \S' \ T' = W\ \U = S' \ T'\ - contg conth continuous_on_subset geqr heqr apply auto - done - 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) - apply (intro conjI cont UST) - by (metis IntI ST Un_iff \S \ S'\ \S' \ T' = W\ \T \ T'\ subsetD geqr heqr r0 r_def) -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)" - apply (rule closedin_trans [OF _ UC]) - apply (rule continuous_closedin_preimage_gen [OF _ _ STS]) - using hom homeomorphism_def apply blast - apply (metis hom homeomorphism_def set_eq_subset) - done - have UT: "closedin (top_of_set U) (C \ g -` T)" - apply (rule closedin_trans [OF _ UC]) - apply (rule continuous_closedin_preimage_gen [OF _ _ STT]) - using hom homeomorphism_def apply blast - apply (metis hom homeomorphism_def set_eq_subset) - done - have ARS: "AR (C \ g -` S)" - apply (rule AR_homeomorphic_AR [OF \AR S\]) - apply (simp add: homeomorphic_def) - apply (rule_tac x=g in exI) - apply (rule_tac x=f in exI) - using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) - apply (rule_tac x="f x" in image_eqI, auto) - done - have ART: "AR (C \ g -` T)" - apply (rule AR_homeomorphic_AR [OF \AR T\]) - apply (simp add: homeomorphic_def) - apply (rule_tac x=g in exI) - apply (rule_tac x=f in exI) - using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) - apply (rule_tac x="f x" in image_eqI, auto) - done - have ARI: "AR ((C \ g -` S) \ (C \ g -` T))" - apply (rule AR_homeomorphic_AR [OF \AR (S \ T)\]) - apply (simp add: homeomorphic_def) - apply (rule_tac x=g in exI) - apply (rule_tac x=f in exI) - using hom - apply (auto simp: homeomorphism_def elim!: continuous_on_subset) - apply (rule_tac x="f x" in image_eqI, auto) - done - 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" - apply (rule ANR_imp_closed_neighbourhood_retract [OF \ANR(S \ T)\]) - apply (rule closedin_subset_trans [of U, OF _ ST_W \W \ U\]) - apply (blast intro: assms)+ - done - 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" - apply (rule closedin_subset_trans [of U]) - using cloWW0 cloUW closedin_trans \W0 \ U\ \S \ U\ \T \ U\ apply blast+ - done - 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" - apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ _ \r ` (W0 \ S) \ S\ cloS'WS]) - apply (rule continuous_on_subset [OF contr], blast+) - done - 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" - apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ _ \r ` (W0 \ T) \ T\ cloT'WT]) - apply (rule continuous_on_subset [OF contr], blast+) - done - have "S' \ T' = W" - by (force simp: S'_def T'_def W_def) - obtain O1 O2 where "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)" - 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) (W1 - (W - U0) \ (W2 - (W - U0)))" - apply (subst eq) - apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \open O1\ \open O2\, simp_all) - done - have cloW1: "closedin (top_of_set (W1 - (W - U0) \ (W2 - (W - U0)))) (W1 - (W - U0))" - using cloUS' apply (simp add: closedin_closed) - apply (erule ex_forward) - using U0 \W0 \ S \ W1\ - apply (auto simp: \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = U\ [symmetric]\S' \ T' = W\ [symmetric]) - done - have cloW2: "closedin (top_of_set (W1 - (W - U0) \ (W2 - (W - U0)))) (W2 - (W - U0))" - using cloUT' apply (simp add: closedin_closed) - apply (erule ex_forward) - using U0 \W0 \ T \ W2\ - apply (auto simp: \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = U\ [symmetric]\S' \ T' = W\ [symmetric]) - done - have *: "\x\S \ T. (if x \ S' then g x else h x) = x" - using ST \S' \ T' = W\ cloT'WT closedin_subset geqr heqr - apply (auto simp: r_def, fastforce) - using \S \ S'\ \T \ T'\ \W0 \ S \ W1\ \W1 = S' \ O1\ by auto - have "\r. continuous_on (W1 - (W - U0) \ (W2 - (W - U0))) r \ - r ` (W1 - (W - U0) \ (W2 - (W - U0))) \ S \ T \ - (\x\S \ T. r x = x)" - apply (rule_tac x = "\x. if x \ S' then g x else h x" in exI) - apply (intro conjI *) - apply (rule continuous_on_cases_local - [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]]) - using \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = W\ - \g ` W1 \ S\ \h ` W2 \ T\ apply auto - using \U0 \ W \ W0\ \W0 \ S \ W1\ apply (fastforce simp add: geqr heqr)+ - done - then show "S \ T retract_of W1 - (W - U0) \ (W2 - (W - U0))" - using \W0 \ S \ W1\ \W0 \ T \ W2\ ST opeUU0 U0 - by (auto simp: retract_of_def retraction_def) - 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)" - apply (rule closedin_trans [OF _ UC]) - apply (rule continuous_closedin_preimage_gen [OF _ _ STS]) - using hom [unfolded homeomorphism_def] apply blast - apply (metis hom homeomorphism_def set_eq_subset) - done - have UT: "closedin (top_of_set U) (C \ g -` T)" - apply (rule closedin_trans [OF _ UC]) - apply (rule continuous_closedin_preimage_gen [OF _ _ STT]) - using hom [unfolded homeomorphism_def] apply blast - apply (metis hom homeomorphism_def set_eq_subset) - done - have ANRS: "ANR (C \ g -` S)" - apply (rule ANR_homeomorphic_ANR [OF \ANR S\]) - apply (simp add: homeomorphic_def) - apply (rule_tac x=g in exI) - apply (rule_tac x=f in exI) - using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) - apply (rule_tac x="f x" in image_eqI, auto) - done - have ANRT: "ANR (C \ g -` T)" - apply (rule ANR_homeomorphic_ANR [OF \ANR T\]) - apply (simp add: homeomorphic_def) - apply (rule_tac x=g in exI) - apply (rule_tac x=f in exI) - using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) - apply (rule_tac x="f x" in image_eqI, auto) - done - have ANRI: "ANR ((C \ g -` S) \ (C \ g -` T))" - apply (rule ANR_homeomorphic_ANR [OF \ANR (S \ T)\]) - apply (simp add: homeomorphic_def) - apply (rule_tac x=g in exI) - apply (rule_tac x=f in exI) - using hom - apply (auto simp: homeomorphism_def elim!: continuous_on_subset) - apply (rule_tac x="f x" in image_eqI, auto) - done - 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" - apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf \f ` C \ T\ cloUC]) - using 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" and opeTS: "openin (top_of_set T) S" - shows "ENR S" - using assms apply (simp add: ENR_ANR) - using ANR_openin locally_open_subset by blast - -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)" -apply (simp add: ENR_convex_closed closed_cbox) -by (simp add: 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" - apply (rule homeomorphic_closedin_convex [of S]) - using aff_dim_le_DIM [of S] apply auto - done - 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 - show ?thesis - using assms - apply (clarsimp simp: ANR_def) - apply (drule_tac x=U in spec) - apply (drule_tac x=T in spec) - using \S homeomorphic T\ \U \ {}\ UT apply (blast intro: S) - done -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" - apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ contf1 _ cloUC]) - using fim apply auto - done - 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" - apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf2 _ cloUC]) - using fim apply auto - done - 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) - subsection \Kuhn Simplices\ lemma bij_betw_singleton_eq: @@ -3681,1262 +2364,6 @@ by blast qed -subsubsection \We continue with 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}" - apply (simp add: 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}))" - apply (rule continuous_openin_preimage_gen) - apply (auto simp: False affine_imp_convex continuous_on_closest_point) - done - ultimately show ?thesis - unfolding ENR_def - apply (rule_tac x = "closest_point (affine hull S) -` (- {a})" in exI) - apply (simp add: vimage_def) - done -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)" - apply (rule continuous_on_cases_local [OF clS clT]) - using r by (auto simp: continuous_on_id) - 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" - apply (rule AR_retract_of_AR [OF Un]) - by (meson AR_imp_retract clS clT 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 Int_lower1 continuous_on_subset r) - qed (use req continuous_on_id in auto) - with rim have "S retract_of S \ V" - unfolding retraction_def retract_of_def - apply (rule_tac x="\x. if x \ S then x else r x" in exI) - apply (auto simp: eq') - done - then show ?thesis - using ANR_neighborhood_retract [OF Un] - using \S \ V = S \ T - T \ V\ clT ope by fastforce -qed - -lemma ANR_from_Un_Int: - fixes S :: "'a::euclidean_space set" - assumes clo: "closed S" "closed T" and Un: "ANR(S \ T)" and Int: "ANR(S \ T)" - shows "ANR S" - 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) - -lemma ANR_finite_Union_convex_closed: - fixes \ :: "'a::euclidean_space set set" - assumes \: "finite \" and clo: "\C. C \ \ \ closed C" and con: "\C. C \ \ \ convex C" - shows "ANR(\\)" -proof - - have "ANR(\\)" if "card \ < n" for n - using assms that - proof (induction n arbitrary: \) - case 0 then show ?case by simp - next - case (Suc n) - have "ANR(\\)" if "finite \" "\ \ \" for \ - using that - proof (induction \) - case empty - then show ?case by simp - next - case (insert C \) - have "ANR (C \ \\)" - proof (rule ANR_closed_Un) - show "ANR (C \ \\)" - unfolding Int_Union - proof (rule Suc) - show "finite ((\) C ` \)" - by (simp add: insert.hyps(1)) - show "\Ca. Ca \ (\) C ` \ \ closed Ca" - by (metis (no_types, hide_lams) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2) - show "\Ca. Ca \ (\) C ` \ \ convex Ca" - by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE) - show "card ((\) C ` \) < n" - proof - - have "card \ \ n" - by (meson Suc.prems(4) not_less not_less_eq) - then show ?thesis - by (metis Suc.prems(1) card_image_le card_seteq insert.hyps insert.prems insert_subset le_trans not_less) - qed - qed - show "closed (\\)" - using Suc.prems(2) insert.hyps(1) insert.prems by blast - qed (use Suc.prems convex_imp_ANR insert.prems insert.IH in auto) - then show ?case - by simp - qed - then show ?case - using Suc.prems(1) by blast - qed - then show ?thesis - by blast -qed - - -lemma finite_imp_ANR: - fixes S :: "'a::euclidean_space set" - assumes "finite S" - shows "ANR S" -proof - - have "ANR(\x \ S. {x})" - by (blast intro: ANR_finite_Union_convex_closed assms) - then show ?thesis - by simp -qed - -lemma ANR_insert: - fixes S :: "'a::euclidean_space set" - assumes "ANR S" "closed S" - shows "ANR(insert a S)" - by (metis ANR_closed_Un ANR_empty ANR_singleton Diff_disjoint Diff_insert_absorb assms closed_singleton insert_absorb insert_is_Un) - -lemma ANR_path_component_ANR: - fixes S :: "'a::euclidean_space set" - shows "ANR S \ ANR(path_component_set S x)" - using ANR_imp_locally_path_connected ANR_openin openin_path_component_locally_path_connected by blast - -lemma ANR_connected_component_ANR: - fixes S :: "'a::euclidean_space set" - shows "ANR S \ ANR(connected_component_set S x)" - by (metis ANR_openin openin_connected_component_locally_connected ANR_imp_locally_connected) - -lemma ANR_component_ANR: - fixes S :: "'a::euclidean_space set" - assumes "ANR S" "c \ components S" - shows "ANR c" - by (metis ANR_connected_component_ANR assms componentsE) - -subsubsection\Original ANR material, now for ENRs\ - -lemma ENR_bounded: - fixes S :: "'a::euclidean_space set" - assumes "bounded S" - shows "ENR S \ (\U. open U \ bounded U \ S retract_of U)" - (is "?lhs = ?rhs") -proof - obtain r where "0 < r" and r: "S \ ball 0 r" - using bounded_subset_ballD assms by blast - assume ?lhs - then show ?rhs - apply (clarsimp simp: ENR_def) - apply (rule_tac x="ball 0 r \ U" in exI, auto) - using r retract_of_imp_subset retract_of_subset by fastforce -next - assume ?rhs - then show ?lhs - using ENR_def by blast -qed - -lemma absolute_retract_imp_AR_gen: - fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" - assumes "S retract_of T" "convex T" "T \ {}" "S homeomorphic S'" "closedin (top_of_set U) S'" - shows "S' retract_of U" -proof - - have "AR T" - by (simp add: assms convex_imp_AR) - then have "AR S" - using AR_retract_of_AR assms by auto - then show ?thesis - using assms AR_imp_absolute_retract by metis -qed - -lemma absolute_retract_imp_AR: - fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" - assumes "S retract_of UNIV" "S homeomorphic S'" "closed S'" - shows "S' retract_of UNIV" - using AR_imp_absolute_retract_UNIV assms retract_of_UNIV by blast - -lemma homeomorphic_compact_arness: - fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" - assumes "S homeomorphic S'" - shows "compact S \ S retract_of UNIV \ compact S' \ S' retract_of UNIV" - using assms homeomorphic_compactness - apply auto - apply (meson assms compact_AR homeomorphic_AR_iff_AR homeomorphic_compactness)+ - done - -lemma absolute_retract_from_Un_Int: - fixes S :: "'a::euclidean_space set" - assumes "(S \ T) retract_of UNIV" "(S \ T) retract_of UNIV" "closed S" "closed T" - shows "S retract_of UNIV" - using AR_from_Un_Int assms retract_of_UNIV by auto - -lemma ENR_from_Un_Int_gen: - fixes S :: "'a::euclidean_space set" - assumes "closedin (top_of_set (S \ T)) S" "closedin (top_of_set (S \ T)) T" "ENR(S \ T)" "ENR(S \ T)" - shows "ENR S" - apply (simp add: ENR_ANR) - using ANR_from_Un_Int_local ENR_ANR assms locally_compact_closedin by blast - - -lemma ENR_from_Un_Int: - fixes S :: "'a::euclidean_space set" - assumes "closed S" "closed T" "ENR(S \ T)" "ENR(S \ T)" - shows "ENR S" - by (meson ENR_from_Un_Int_gen assms closed_subset sup_ge1 sup_ge2) - - -lemma ENR_finite_Union_convex_closed: - fixes \ :: "'a::euclidean_space set set" - assumes \: "finite \" and clo: "\C. C \ \ \ closed C" and con: "\C. C \ \ \ convex C" - shows "ENR(\ \)" - by (simp add: ENR_ANR ANR_finite_Union_convex_closed \ clo closed_Union closed_imp_locally_compact con) - -lemma finite_imp_ENR: - fixes S :: "'a::euclidean_space set" - shows "finite S \ ENR S" - by (simp add: ENR_ANR finite_imp_ANR finite_imp_closed closed_imp_locally_compact) - -lemma ENR_insert: - fixes S :: "'a::euclidean_space set" - assumes "closed S" "ENR S" - shows "ENR(insert a S)" -proof - - have "ENR ({a} \ S)" - by (metis ANR_insert ENR_ANR Un_commute Un_insert_right assms closed_imp_locally_compact closed_insert sup_bot_right) - then show ?thesis - by auto -qed - -lemma ENR_path_component_ENR: - fixes S :: "'a::euclidean_space set" - assumes "ENR S" - shows "ENR(path_component_set S x)" - by (metis ANR_imp_locally_path_connected ENR_empty ENR_imp_ANR ENR_openin assms - locally_path_connected_2 openin_subtopology_self path_component_eq_empty) - -(*UNUSED -lemma ENR_Times: - fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" - assumes "ENR S" "ENR T" shows "ENR(S \ T)" -using assms apply (simp add: ENR_ANR ANR_Times) -thm locally_compact_Times -oops - SIMP_TAC[ENR_ANR; ANR_PCROSS; LOCALLY_COMPACT_PCROSS]);; -*) - -subsubsection\Finally, spheres are ANRs and ENRs\ - -lemma absolute_retract_homeomorphic_convex_compact: - fixes S :: "'a::euclidean_space set" and U :: "'b::euclidean_space set" - assumes "S homeomorphic U" "S \ {}" "S \ T" "convex U" "compact U" - shows "S retract_of T" - by (metis UNIV_I assms compact_AR convex_imp_AR homeomorphic_AR_iff_AR homeomorphic_compactness homeomorphic_empty(1) retract_of_subset subsetI) - -lemma frontier_retract_of_punctured_universe: - fixes S :: "'a::euclidean_space set" - assumes "convex S" "bounded S" "a \ interior S" - shows "(frontier S) retract_of (- {a})" - using rel_frontier_retract_of_punctured_affine_hull - by (metis Compl_eq_Diff_UNIV affine_hull_nonempty_interior assms empty_iff rel_frontier_frontier rel_interior_nonempty_interior) - -lemma sphere_retract_of_punctured_universe_gen: - fixes a :: "'a::euclidean_space" - assumes "b \ ball a r" - shows "sphere a r retract_of (- {b})" -proof - - have "frontier (cball a r) retract_of (- {b})" - apply (rule frontier_retract_of_punctured_universe) - using assms by auto - then show ?thesis - by simp -qed - -lemma sphere_retract_of_punctured_universe: - fixes a :: "'a::euclidean_space" - assumes "0 < r" - shows "sphere a r retract_of (- {a})" - by (simp add: assms sphere_retract_of_punctured_universe_gen) - -lemma ENR_sphere: - fixes a :: "'a::euclidean_space" - shows "ENR(sphere a r)" -proof (cases "0 < r") - case True - then have "sphere a r retract_of -{a}" - by (simp add: sphere_retract_of_punctured_universe) - with open_delete show ?thesis - by (auto simp: ENR_def) -next - case False - then show ?thesis - using finite_imp_ENR - by (metis finite_insert infinite_imp_nonempty less_linear sphere_eq_empty sphere_trivial) -qed - -corollary\<^marker>\tag unimportant\ ANR_sphere: - fixes a :: "'a::euclidean_space" - shows "ANR(sphere a r)" - by (simp add: ENR_imp_ANR ENR_sphere) - -subsubsection\Spheres are connected, etc\ - -lemma locally_path_connected_sphere_gen: - fixes S :: "'a::euclidean_space set" - assumes "bounded S" and "convex S" - shows "locally path_connected (rel_frontier S)" -proof (cases "rel_interior S = {}") - case True - with assms show ?thesis - by (simp add: rel_interior_eq_empty) -next - case False - then obtain a where a: "a \ rel_interior S" - by blast - show ?thesis - proof (rule retract_of_locally_path_connected) - show "locally path_connected (affine hull S - {a})" - by (meson convex_affine_hull convex_imp_locally_path_connected locally_open_subset openin_delete openin_subtopology_self) - show "rel_frontier S retract_of affine hull S - {a}" - using a assms rel_frontier_retract_of_punctured_affine_hull by blast - qed -qed - -lemma locally_connected_sphere_gen: - fixes S :: "'a::euclidean_space set" - assumes "bounded S" and "convex S" - shows "locally connected (rel_frontier S)" - by (simp add: ANR_imp_locally_connected ANR_rel_frontier_convex assms) - -lemma locally_path_connected_sphere: - fixes a :: "'a::euclidean_space" - shows "locally path_connected (sphere a r)" - using ENR_imp_locally_path_connected ENR_sphere by blast - -lemma locally_connected_sphere: - fixes a :: "'a::euclidean_space" - shows "locally connected(sphere a r)" - using ANR_imp_locally_connected ANR_sphere by blast - -subsubsection\Borsuk homotopy extension theorem\ - -text\It's only this late so we can use the concept of retraction, - saying that the domain sets or range set are ENRs.\ - -theorem Borsuk_homotopy_extension_homotopic: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes cloTS: "closedin (top_of_set T) S" - and anr: "(ANR S \ ANR T) \ ANR U" - and contf: "continuous_on T f" - and "f ` T \ U" - and "homotopic_with_canon (\x. True) S U f g" - obtains g' where "homotopic_with_canon (\x. True) T U f g'" - "continuous_on T g'" "image g' T \ U" - "\x. x \ S \ g' x = g x" -proof - - have "S \ T" using assms closedin_imp_subset by blast - obtain h where conth: "continuous_on ({0..1} \ S) h" - and him: "h ` ({0..1} \ S) \ U" - and [simp]: "\x. h(0, x) = f x" "\x. h(1::real, x) = g x" - using assms by (auto simp: homotopic_with_def) - define h' where "h' \ \z. if snd z \ S then h z else (f \ snd) z" - define B where "B \ {0::real} \ T \ {0..1} \ S" - have clo0T: "closedin (top_of_set ({0..1} \ T)) ({0::real} \ T)" - by (simp add: Abstract_Topology.closedin_Times) - moreover have cloT1S: "closedin (top_of_set ({0..1} \ T)) ({0..1} \ S)" - by (simp add: Abstract_Topology.closedin_Times assms) - ultimately have clo0TB:"closedin (top_of_set ({0..1} \ T)) B" - by (auto simp: B_def) - have cloBS: "closedin (top_of_set B) ({0..1} \ S)" - by (metis (no_types) Un_subset_iff B_def closedin_subset_trans [OF cloT1S] clo0TB closedin_imp_subset closedin_self) - moreover have cloBT: "closedin (top_of_set B) ({0} \ T)" - using \S \ T\ closedin_subset_trans [OF clo0T] - by (metis B_def Un_upper1 clo0TB closedin_closed inf_le1) - moreover have "continuous_on ({0} \ T) (f \ snd)" - apply (rule continuous_intros)+ - apply (simp add: contf) - done - ultimately have conth': "continuous_on B h'" - apply (simp add: h'_def B_def Un_commute [of "{0} \ T"]) - apply (auto intro!: continuous_on_cases_local conth) - done - have "image h' B \ U" - using \f ` T \ U\ him by (auto simp: h'_def B_def) - obtain V k where "B \ V" and opeTV: "openin (top_of_set ({0..1} \ T)) V" - and contk: "continuous_on V k" and kim: "k ` V \ U" - and keq: "\x. x \ B \ k x = h' x" - using anr - proof - assume ST: "ANR S \ ANR T" - have eq: "({0} \ T \ {0..1} \ S) = {0::real} \ S" - using \S \ T\ by auto - have "ANR B" - apply (simp add: B_def) - apply (rule ANR_closed_Un_local) - apply (metis cloBT B_def) - apply (metis Un_commute cloBS B_def) - apply (simp_all add: ANR_Times convex_imp_ANR ANR_singleton ST eq) - done - note Vk = that - have *: thesis if "openin (top_of_set ({0..1::real} \ T)) V" - "retraction V B r" for V r - using that - apply (clarsimp simp add: retraction_def) - apply (rule Vk [of V "h' \ r"], assumption+) - apply (metis continuous_on_compose conth' continuous_on_subset) - using \h' ` B \ U\ apply force+ - done - show thesis - apply (rule ANR_imp_neighbourhood_retract [OF \ANR B\ clo0TB]) - apply (auto simp: ANR_Times ANR_singleton ST retract_of_def *) - done - next - assume "ANR U" - with ANR_imp_absolute_neighbourhood_extensor \h' ` B \ U\ clo0TB conth' that - show ?thesis by blast - qed - define S' where "S' \ {x. \u::real. u \ {0..1} \ (u, x::'a) \ {0..1} \ T - V}" - have "closedin (top_of_set T) S'" - unfolding S'_def - apply (rule closedin_compact_projection, blast) - using closedin_self opeTV by blast - have S'_def: "S' = {x. \u::real. (u, x::'a) \ {0..1} \ T - V}" - by (auto simp: S'_def) - have cloTS': "closedin (top_of_set T) S'" - using S'_def \closedin (top_of_set T) S'\ by blast - have "S \ S' = {}" - using S'_def B_def \B \ V\ by force - obtain a :: "'a \ real" where conta: "continuous_on T a" - and "\x. x \ T \ a x \ closed_segment 1 0" - and a1: "\x. x \ S \ a x = 1" - and a0: "\x. x \ S' \ a x = 0" - apply (rule Urysohn_local [OF cloTS cloTS' \S \ S' = {}\, of 1 0], blast) - done - then have ain: "\x. x \ T \ a x \ {0..1}" - using closed_segment_eq_real_ivl by auto - have inV: "(u * a t, t) \ V" if "t \ T" "0 \ u" "u \ 1" for t u - proof (rule ccontr) - assume "(u * a t, t) \ V" - with ain [OF \t \ T\] have "a t = 0" - apply simp - apply (rule a0) - by (metis (no_types, lifting) Diff_iff S'_def SigmaI atLeastAtMost_iff mem_Collect_eq mult_le_one mult_nonneg_nonneg that) - show False - using B_def \(u * a t, t) \ V\ \B \ V\ \a t = 0\ that by auto - qed - show ?thesis - proof - show hom: "homotopic_with_canon (\x. True) T U f (\x. k (a x, x))" - proof (simp add: homotopic_with, intro exI conjI) - show "continuous_on ({0..1} \ T) (k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z)))" - apply (intro continuous_on_compose continuous_intros) - apply (rule continuous_on_subset [OF conta], force) - apply (rule continuous_on_subset [OF contk]) - apply (force intro: inV) - done - show "(k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z))) ` ({0..1} \ T) \ U" - using inV kim by auto - show "\x\T. (k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z))) (0, x) = f x" - by (simp add: B_def h'_def keq) - show "\x\T. (k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z))) (1, x) = k (a x, x)" - by auto - qed - show "continuous_on T (\x. k (a x, x))" - using homotopic_with_imp_continuous_maps [OF hom] by auto - show "(\x. k (a x, x)) ` T \ U" - proof clarify - fix t - assume "t \ T" - show "k (a t, t) \ U" - by (metis \t \ T\ image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1) - qed - show "\x. x \ S \ k (a x, x) = g x" - by (simp add: B_def a1 h'_def keq) - qed -qed - - -corollary\<^marker>\tag unimportant\ nullhomotopic_into_ANR_extension: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes "closed S" - and contf: "continuous_on S f" - and "ANR T" - and fim: "f ` S \ T" - and "S \ {}" - shows "(\c. homotopic_with_canon (\x. True) S T f (\x. c)) \ - (\g. continuous_on UNIV g \ range g \ T \ (\x \ S. g x = f x))" - (is "?lhs = ?rhs") -proof - assume ?lhs - then obtain c where c: "homotopic_with_canon (\x. True) S T (\x. c) f" - by (blast intro: homotopic_with_symD) - have "closedin (top_of_set UNIV) S" - using \closed S\ closed_closedin by fastforce - then obtain g where "continuous_on UNIV g" "range g \ T" - "\x. x \ S \ g x = f x" - apply (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ c, where T=UNIV]) - using \ANR T\ \S \ {}\ c homotopic_with_imp_subset1 apply fastforce+ - done - then show ?rhs by blast -next - assume ?rhs - then obtain g where "continuous_on UNIV g" "range g \ T" "\x. x\S \ g x = f x" - by blast - then obtain c where "homotopic_with_canon (\h. True) UNIV T g (\x. c)" - using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast - then have "homotopic_with_canon (\x. True) S T g (\x. c)" - by (simp add: homotopic_from_subtopology) - then show ?lhs - by (force elim: homotopic_with_eq [of _ _ _ g "\x. c"] simp: \\x. x \ S \ g x = f x\) -qed - -corollary\<^marker>\tag unimportant\ nullhomotopic_into_rel_frontier_extension: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes "closed S" - and contf: "continuous_on S f" - and "convex T" "bounded T" - and fim: "f ` S \ rel_frontier T" - and "S \ {}" - shows "(\c. homotopic_with_canon (\x. True) S (rel_frontier T) f (\x. c)) \ - (\g. continuous_on UNIV g \ range g \ rel_frontier T \ (\x \ S. g x = f x))" -by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex) - -corollary\<^marker>\tag unimportant\ nullhomotopic_into_sphere_extension: - fixes f :: "'a::euclidean_space \ 'b :: euclidean_space" - assumes "closed S" and contf: "continuous_on S f" - and "S \ {}" and fim: "f ` S \ sphere a r" - shows "((\c. homotopic_with_canon (\x. True) S (sphere a r) f (\x. c)) \ - (\g. continuous_on UNIV g \ range g \ sphere a r \ (\x \ S. g x = f x)))" - (is "?lhs = ?rhs") -proof (cases "r = 0") - case True with fim show ?thesis - apply auto - using fim continuous_on_const apply fastforce - by (metis contf contractible_sing nullhomotopic_into_contractible) -next - case False - then have eq: "sphere a r = rel_frontier (cball a r)" by simp - show ?thesis - using fim unfolding eq - apply (rule nullhomotopic_into_rel_frontier_extension [OF \closed S\ contf convex_cball bounded_cball]) - apply (rule \S \ {}\) - done -qed - -proposition\<^marker>\tag unimportant\ Borsuk_map_essential_bounded_component: - fixes a :: "'a :: euclidean_space" - assumes "compact S" and "a \ S" - shows "bounded (connected_component_set (- S) a) \ - \(\c. homotopic_with_canon (\x. True) S (sphere 0 1) - (\x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\x. c))" - (is "?lhs = ?rhs") -proof (cases "S = {}") - case True then show ?thesis - by simp -next - case False - have "closed S" "bounded S" - using \compact S\ compact_eq_bounded_closed by auto - have s01: "(\x. (x - a) /\<^sub>R norm (x - a)) ` S \ sphere 0 1" - using \a \ S\ by clarsimp (metis dist_eq_0_iff dist_norm mult.commute right_inverse) - have aincc: "a \ connected_component_set (- S) a" - by (simp add: \a \ S\) - obtain r where "r>0" and r: "S \ ball 0 r" - using bounded_subset_ballD \bounded S\ by blast - have "\ ?rhs \ \ ?lhs" - proof - assume notr: "\ ?rhs" - have nog: "\g. continuous_on (S \ connected_component_set (- S) a) g \ - g ` (S \ connected_component_set (- S) a) \ sphere 0 1 \ - (\x\S. g x = (x - a) /\<^sub>R norm (x - a))" - if "bounded (connected_component_set (- S) a)" - apply (rule non_extensible_Borsuk_map [OF \compact S\ componentsI _ aincc]) - using \a \ S\ that by auto - obtain g where "range g \ sphere 0 1" "continuous_on UNIV g" - "\x. x \ S \ g x = (x - a) /\<^sub>R norm (x - a)" - using notr - by (auto simp: nullhomotopic_into_sphere_extension - [OF \closed S\ continuous_on_Borsuk_map [OF \a \ S\] False s01]) - with \a \ S\ show "\ ?lhs" - apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog) - apply (drule_tac x=g in spec) - using continuous_on_subset by fastforce - next - assume "\ ?lhs" - then obtain b where b: "b \ connected_component_set (- S) a" and "r \ norm b" - using bounded_iff linear by blast - then have bnot: "b \ ball 0 r" - by simp - have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. (x - a) /\<^sub>R norm (x - a)) - (\x. (x - b) /\<^sub>R norm (x - b))" - apply (rule Borsuk_maps_homotopic_in_path_component) - using \closed S\ b open_Compl open_path_connected_component apply fastforce - done - moreover - obtain c where "homotopic_with_canon (\x. True) (ball 0 r) (sphere 0 1) - (\x. inverse (norm (x - b)) *\<^sub>R (x - b)) (\x. c)" - proof (rule nullhomotopic_from_contractible) - show "contractible (ball (0::'a) r)" - by (metis convex_imp_contractible convex_ball) - show "continuous_on (ball 0 r) (\x. inverse(norm (x - b)) *\<^sub>R (x - b))" - by (rule continuous_on_Borsuk_map [OF bnot]) - show "(\x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \ sphere 0 1" - using bnot Borsuk_map_into_sphere by blast - qed blast - ultimately have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. (x - a) /\<^sub>R norm (x - a)) (\x. c)" - by (meson homotopic_with_subset_left homotopic_with_trans r) - then show "\ ?rhs" - by blast - qed - then show ?thesis by blast -qed - -lemma homotopic_Borsuk_maps_in_bounded_component: - fixes a :: "'a :: euclidean_space" - assumes "compact S" and "a \ S"and "b \ S" - and boc: "bounded (connected_component_set (- S) a)" - and hom: "homotopic_with_canon (\x. True) S (sphere 0 1) - (\x. (x - a) /\<^sub>R norm (x - a)) - (\x. (x - b) /\<^sub>R norm (x - b))" - shows "connected_component (- S) a b" -proof (rule ccontr) - assume notcc: "\ connected_component (- S) a b" - let ?T = "S \ connected_component_set (- S) a" - have "\g. continuous_on (S \ connected_component_set (- S) a) g \ - g ` (S \ connected_component_set (- S) a) \ sphere 0 1 \ - (\x\S. g x = (x - a) /\<^sub>R norm (x - a))" - by (simp add: \a \ S\ componentsI non_extensible_Borsuk_map [OF \compact S\ _ boc]) - moreover obtain g where "continuous_on (S \ connected_component_set (- S) a) g" - "g ` (S \ connected_component_set (- S) a) \ sphere 0 1" - "\x. x \ S \ g x = (x - a) /\<^sub>R norm (x - a)" - proof (rule Borsuk_homotopy_extension_homotopic) - show "closedin (top_of_set ?T) S" - by (simp add: \compact S\ closed_subset compact_imp_closed) - show "continuous_on ?T (\x. (x - b) /\<^sub>R norm (x - b))" - by (simp add: \b \ S\ notcc continuous_on_Borsuk_map) - show "(\x. (x - b) /\<^sub>R norm (x - b)) ` ?T \ sphere 0 1" - by (simp add: \b \ S\ notcc Borsuk_map_into_sphere) - show "homotopic_with_canon (\x. True) S (sphere 0 1) - (\x. (x - b) /\<^sub>R norm (x - b)) (\x. (x - a) /\<^sub>R norm (x - a))" - by (simp add: hom homotopic_with_symD) - qed (auto simp: ANR_sphere intro: that) - ultimately show False by blast -qed - - -lemma Borsuk_maps_homotopic_in_connected_component_eq: - fixes a :: "'a :: euclidean_space" - assumes S: "compact S" "a \ S" "b \ S" and 2: "2 \ DIM('a)" - shows "(homotopic_with_canon (\x. True) S (sphere 0 1) - (\x. (x - a) /\<^sub>R norm (x - a)) - (\x. (x - b) /\<^sub>R norm (x - b)) \ - connected_component (- S) a b)" - (is "?lhs = ?rhs") -proof - assume L: ?lhs - show ?rhs - proof (cases "bounded(connected_component_set (- S) a)") - case True - show ?thesis - by (rule homotopic_Borsuk_maps_in_bounded_component [OF S True L]) - next - case not_bo_a: False - show ?thesis - proof (cases "bounded(connected_component_set (- S) b)") - case True - show ?thesis - using homotopic_Borsuk_maps_in_bounded_component [OF S] - by (simp add: L True assms connected_component_sym homotopic_Borsuk_maps_in_bounded_component homotopic_with_sym) - next - case False - then show ?thesis - using cobounded_unique_unbounded_component [of "-S" a b] \compact S\ not_bo_a - by (auto simp: compact_eq_bounded_closed assms connected_component_eq_eq) - qed - qed -next - assume R: ?rhs - then have "path_component (- S) a b" - using assms(1) compact_eq_bounded_closed open_Compl open_path_connected_component_set by fastforce - then show ?lhs - by (simp add: Borsuk_maps_homotopic_in_path_component) -qed - -subsubsection\More extension theorems\ - -lemma extension_from_clopen: - assumes ope: "openin (top_of_set S) T" - and clo: "closedin (top_of_set S) T" - and contf: "continuous_on T f" and fim: "f ` T \ U" and null: "U = {} \ S = {}" - obtains g where "continuous_on S g" "g ` S \ U" "\x. x \ T \ g x = f x" -proof (cases "U = {}") - case True - then show ?thesis - by (simp add: null that) -next - case False - then obtain a where "a \ U" - by auto - let ?g = "\x. if x \ T then f x else a" - have Seq: "S = T \ (S - T)" - using clo closedin_imp_subset by fastforce - show ?thesis - proof - have "continuous_on (T \ (S - T)) ?g" - apply (rule continuous_on_cases_local) - using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local) - with Seq show "continuous_on S ?g" - by metis - show "?g ` S \ U" - using \a \ U\ fim by auto - show "\x. x \ T \ ?g x = f x" - by auto - qed -qed - - -lemma extension_from_component: - fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" - assumes S: "locally connected S \ compact S" and "ANR U" - and C: "C \ components S" and contf: "continuous_on C f" and fim: "f ` C \ U" - obtains g where "continuous_on S g" "g ` S \ U" "\x. x \ C \ g x = f x" -proof - - obtain T g where ope: "openin (top_of_set S) T" - and clo: "closedin (top_of_set S) T" - and "C \ T" and contg: "continuous_on T g" and gim: "g ` T \ U" - and gf: "\x. x \ C \ g x = f x" - using S - proof - assume "locally connected S" - show ?thesis - by (metis C \locally connected S\ openin_components_locally_connected closedin_component contf fim order_refl that) - next - assume "compact S" - then obtain W g where "C \ W" and opeW: "openin (top_of_set S) W" - and contg: "continuous_on W g" - and gim: "g ` W \ U" and gf: "\x. x \ C \ g x = f x" - using ANR_imp_absolute_neighbourhood_extensor [of U C f S] C \ANR U\ closedin_component contf fim by blast - then obtain V where "open V" and V: "W = S \ V" - by (auto simp: openin_open) - moreover have "locally compact S" - by (simp add: \compact S\ closed_imp_locally_compact compact_imp_closed) - ultimately obtain K where opeK: "openin (top_of_set S) K" and "compact K" "C \ K" "K \ V" - by (metis C Int_subset_iff \C \ W\ \compact S\ compact_components Sura_Bura_clopen_subset) - show ?thesis - proof - show "closedin (top_of_set S) K" - by (meson \compact K\ \compact S\ closedin_compact_eq opeK openin_imp_subset) - show "continuous_on K g" - by (metis Int_subset_iff V \K \ V\ contg continuous_on_subset opeK openin_subtopology subset_eq) - show "g ` K \ U" - using V \K \ V\ gim opeK openin_imp_subset by fastforce - qed (use opeK gf \C \ K\ in auto) - qed - obtain h where "continuous_on S h" "h ` S \ U" "\x. x \ T \ h x = g x" - using extension_from_clopen - by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope) - then show ?thesis - by (metis \C \ T\ gf subset_eq that) -qed - - -lemma tube_lemma: - fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" - assumes "compact S" and S: "S \ {}" "(\x. (x,a)) ` S \ U" - and ope: "openin (top_of_set (S \ T)) U" - obtains V where "openin (top_of_set T) V" "a \ V" "S \ V \ U" -proof - - let ?W = "{y. \x. x \ S \ (x, y) \ (S \ T - U)}" - have "U \ S \ T" "closedin (top_of_set (S \ T)) (S \ T - U)" - using ope by (auto simp: openin_closedin_eq) - then have "closedin (top_of_set T) ?W" - using \compact S\ closedin_compact_projection by blast - moreover have "a \ T - ?W" - using \U \ S \ T\ S by auto - moreover have "S \ (T - ?W) \ U" - by auto - ultimately show ?thesis - by (metis (no_types, lifting) Sigma_cong closedin_def that topspace_euclidean_subtopology) -qed - -lemma tube_lemma_gen: - fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" - assumes "compact S" "S \ {}" "T \ T'" "S \ T \ U" - and ope: "openin (top_of_set (S \ T')) U" - obtains V where "openin (top_of_set T') V" "T \ V" "S \ V \ U" -proof - - have "\x. x \ T \ \V. openin (top_of_set T') V \ x \ V \ S \ V \ U" - using assms by (auto intro: tube_lemma [OF \compact S\]) - then obtain F where F: "\x. x \ T \ openin (top_of_set T') (F x) \ x \ F x \ S \ F x \ U" - by metis - show ?thesis - proof - show "openin (top_of_set T') (\(F ` T))" - using F by blast - show "T \ \(F ` T)" - using F by blast - show "S \ \(F ` T) \ U" - using F by auto - qed -qed - -proposition\<^marker>\tag unimportant\ homotopic_neighbourhood_extension: - fixes f :: "'a::euclidean_space \ 'b::euclidean_space" - assumes contf: "continuous_on S f" and fim: "f ` S \ U" - and contg: "continuous_on S g" and gim: "g ` S \ U" - and clo: "closedin (top_of_set S) T" - and "ANR U" and hom: "homotopic_with_canon (\x. True) T U f g" - obtains V where "T \ V" "openin (top_of_set S) V" - "homotopic_with_canon (\x. True) V U f g" -proof - - have "T \ S" - using clo closedin_imp_subset by blast - obtain h where conth: "continuous_on ({0..1::real} \ T) h" - and him: "h ` ({0..1} \ T) \ U" - and h0: "\x. h(0, x) = f x" and h1: "\x. h(1, x) = g x" - using hom by (auto simp: homotopic_with_def) - define h' where "h' \ \z. if fst z \ {0} then f(snd z) - else if fst z \ {1} then g(snd z) - else h z" - let ?S0 = "{0::real} \ S" and ?S1 = "{1::real} \ S" - have "continuous_on(?S0 \ (?S1 \ {0..1} \ T)) h'" - unfolding h'_def - proof (intro continuous_on_cases_local) - show "closedin (top_of_set (?S0 \ (?S1 \ {0..1} \ T))) ?S0" - "closedin (top_of_set (?S1 \ {0..1} \ T)) ?S1" - using \T \ S\ by (force intro: closedin_Times closedin_subset_trans [of "{0..1} \ S"])+ - show "closedin (top_of_set (?S0 \ (?S1 \ {0..1} \ T))) (?S1 \ {0..1} \ T)" - "closedin (top_of_set (?S1 \ {0..1} \ T)) ({0..1} \ T)" - using \T \ S\ by (force intro: clo closedin_Times closedin_subset_trans [of "{0..1} \ S"])+ - show "continuous_on (?S0) (\x. f (snd x))" - by (intro continuous_intros continuous_on_compose2 [OF contf]) auto - show "continuous_on (?S1) (\x. g (snd x))" - by (intro continuous_intros continuous_on_compose2 [OF contg]) auto - qed (use h0 h1 conth in auto) - then have "continuous_on ({0,1} \ S \ ({0..1} \ T)) h'" - by (metis Sigma_Un_distrib1 Un_assoc insert_is_Un) - moreover have "h' ` ({0,1} \ S \ {0..1} \ T) \ U" - using fim gim him \T \ S\ unfolding h'_def by force - moreover have "closedin (top_of_set ({0..1::real} \ S)) ({0,1} \ S \ {0..1::real} \ T)" - by (intro closedin_Times closedin_Un clo) (simp_all add: closed_subset) - ultimately - obtain W k where W: "({0,1} \ S) \ ({0..1} \ T) \ W" - and opeW: "openin (top_of_set ({0..1} \ S)) W" - and contk: "continuous_on W k" - and kim: "k ` W \ U" - and kh': "\x. x \ ({0,1} \ S) \ ({0..1} \ T) \ k x = h' x" - by (metis ANR_imp_absolute_neighbourhood_extensor [OF \ANR U\, of "({0,1} \ S) \ ({0..1} \ T)" h' "{0..1} \ S"]) - obtain T' where opeT': "openin (top_of_set S) T'" - and "T \ T'" and TW: "{0..1} \ T' \ W" - using tube_lemma_gen [of "{0..1::real}" T S W] W \T \ S\ opeW by auto - moreover have "homotopic_with_canon (\x. True) T' U f g" - proof (simp add: homotopic_with, intro exI conjI) - show "continuous_on ({0..1} \ T') k" - using TW continuous_on_subset contk by auto - show "k ` ({0..1} \ T') \ U" - using TW kim by fastforce - have "T' \ S" - by (meson opeT' subsetD openin_imp_subset) - then show "\x\T'. k (0, x) = f x" "\x\T'. k (1, x) = g x" - by (auto simp: kh' h'_def) - qed - ultimately show ?thesis - by (blast intro: that) -qed - -text\ Homotopy on a union of closed-open sets.\ -proposition\<^marker>\tag unimportant\ homotopic_on_clopen_Union: - fixes \ :: "'a::euclidean_space set set" - assumes "\S. S \ \ \ closedin (top_of_set (\\)) S" - and "\S. S \ \ \ openin (top_of_set (\\)) S" - and "\S. S \ \ \ homotopic_with_canon (\x. True) S T f g" - shows "homotopic_with_canon (\x. True) (\\) T f g" -proof - - obtain \ where "\ \ \" "countable \" and eqU: "\\ = \\" - using Lindelof_openin assms by blast - show ?thesis - proof (cases "\ = {}") - case True - then show ?thesis - by (metis Union_empty eqU homotopic_with_canon_on_empty) - next - case False - then obtain V :: "nat \ 'a set" where V: "range V = \" - using range_from_nat_into \countable \\ by metis - with \\ \ \\ have clo: "\n. closedin (top_of_set (\\)) (V n)" - and ope: "\n. openin (top_of_set (\\)) (V n)" - and hom: "\n. homotopic_with_canon (\x. True) (V n) T f g" - using assms by auto - then obtain h where conth: "\n. continuous_on ({0..1::real} \ V n) (h n)" - and him: "\n. h n ` ({0..1} \ V n) \ T" - and h0: "\n. \x. x \ V n \ h n (0, x) = f x" - and h1: "\n. \x. x \ V n \ h n (1, x) = g x" - by (simp add: homotopic_with) metis - have wop: "b \ V x \ \k. b \ V k \ (\j V j)" for b x - using nat_less_induct [where P = "\i. b \ V i"] by meson - obtain \ where cont: "continuous_on ({0..1} \ \(V ` UNIV)) \" - and eq: "\x i. \x \ {0..1} \ \(V ` UNIV) \ - {0..1} \ (V i - (\m \ \ x = h i x" - proof (rule pasting_lemma_exists) - let ?X = "top_of_set ({0..1::real} \ \(range V))" - show "topspace ?X \ (\i. {0..1::real} \ (V i - (\m \(V ` UNIV))) - ({0..1::real} \ (V i - (\m(V ` UNIV))) (V i)" - using ope V eqU by auto - show "closedin (top_of_set (\(V ` UNIV))) (\m (V i - \ (V ` {..i j x. x \ topspace ?X \ {0..1} \ (V i - (\m {0..1} \ (V j - (\m h i x = h j x" - by clarsimp (metis lessThan_iff linorder_neqE_nat) - qed auto - show ?thesis - proof (simp add: homotopic_with eqU [symmetric], intro exI conjI ballI) - show "continuous_on ({0..1} \ \\) \" - using V eqU by (blast intro!: continuous_on_subset [OF cont]) - show "\` ({0..1} \ \\) \ T" - proof clarsimp - fix t :: real and y :: "'a" and X :: "'a set" - assume "y \ X" "X \ \" and t: "0 \ t" "t \ 1" - then obtain k where "y \ V k" and j: "\j V j" - by (metis image_iff V wop) - with him t show "\(t, y) \ T" - by (subst eq) force+ - qed - fix X y - assume "X \ \" "y \ X" - then obtain k where "y \ V k" and j: "\j V j" - by (metis image_iff V wop) - then show "\(0, y) = f y" and "\(1, y) = g y" - by (subst eq [where i=k]; force simp: h0 h1)+ - qed - qed -qed - -lemma homotopic_on_components_eq: - fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set" - assumes S: "locally connected S \ compact S" and "ANR T" - shows "homotopic_with_canon (\x. True) S T f g \ - (continuous_on S f \ f ` S \ T \ continuous_on S g \ g ` S \ T) \ - (\C \ components S. homotopic_with_canon (\x. True) C T f g)" - (is "?lhs \ ?C \ ?rhs") -proof - - have "continuous_on S f" "f ` S \ T" "continuous_on S g" "g ` S \ T" if ?lhs - using homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2 that by blast+ - moreover have "?lhs \ ?rhs" - if contf: "continuous_on S f" and fim: "f ` S \ T" and contg: "continuous_on S g" and gim: "g ` S \ T" - proof - assume ?lhs - with that show ?rhs - by (simp add: homotopic_with_subset_left in_components_subset) - next - assume R: ?rhs - have "\U. C \ U \ closedin (top_of_set S) U \ - openin (top_of_set S) U \ - homotopic_with_canon (\x. True) U T f g" if C: "C \ components S" for C - proof - - have "C \ S" - by (simp add: in_components_subset that) - show ?thesis - using S - proof - assume "locally connected S" - show ?thesis - proof (intro exI conjI) - show "closedin (top_of_set S) C" - by (simp add: closedin_component that) - show "openin (top_of_set S) C" - by (simp add: \locally connected S\ openin_components_locally_connected that) - show "homotopic_with_canon (\x. True) C T f g" - by (simp add: R that) - qed auto - next - assume "compact S" - have hom: "homotopic_with_canon (\x. True) C T f g" - using R that by blast - obtain U where "C \ U" and opeU: "openin (top_of_set S) U" - and hom: "homotopic_with_canon (\x. True) U T f g" - using homotopic_neighbourhood_extension [OF contf fim contg gim _ \ANR T\ hom] - \C \ components S\ closedin_component by blast - then obtain V where "open V" and V: "U = S \ V" - by (auto simp: openin_open) - moreover have "locally compact S" - by (simp add: \compact S\ closed_imp_locally_compact compact_imp_closed) - ultimately obtain K where opeK: "openin (top_of_set S) K" and "compact K" "C \ K" "K \ V" - by (metis C Int_subset_iff Sura_Bura_clopen_subset \C \ U\ \compact S\ compact_components) - show ?thesis - proof (intro exI conjI) - show "closedin (top_of_set S) K" - by (meson \compact K\ \compact S\ closedin_compact_eq opeK openin_imp_subset) - show "homotopic_with_canon (\x. True) K T f g" - using V \K \ V\ hom homotopic_with_subset_left opeK openin_imp_subset by fastforce - qed (use opeK \C \ K\ in auto) - qed - qed - then obtain \ where \: "\C. C \ components S \ C \ \ C" - and clo\: "\C. C \ components S \ closedin (top_of_set S) (\ C)" - and ope\: "\C. C \ components S \ openin (top_of_set S) (\ C)" - and hom\: "\C. C \ components S \ homotopic_with_canon (\x. True) (\ C) T f g" - by metis - have Seq: "S = \ (\ ` components S)" - proof - show "S \ \ (\ ` components S)" - by (metis Sup_mono Union_components \ imageI) - show "\ (\ ` components S) \ S" - using ope\ openin_imp_subset by fastforce - qed - show ?lhs - apply (subst Seq) - apply (rule homotopic_on_clopen_Union) - using Seq clo\ ope\ hom\ by auto - qed - ultimately show ?thesis by blast -qed - - -lemma cohomotopically_trivial_on_components: - fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set" - assumes S: "locally connected S \ compact S" and "ANR T" - shows - "(\f g. continuous_on S f \ f ` S \ T \ continuous_on S g \ g ` S \ T \ - homotopic_with_canon (\x. True) S T f g) - \ - (\C\components S. - \f g. continuous_on C f \ f ` C \ T \ continuous_on C g \ g ` C \ T \ - homotopic_with_canon (\x. True) C T f g)" - (is "?lhs = ?rhs") -proof - assume L[rule_format]: ?lhs - show ?rhs - proof clarify - fix C f g - assume contf: "continuous_on C f" and fim: "f ` C \ T" - and contg: "continuous_on C g" and gim: "g ` C \ T" and C: "C \ components S" - obtain f' where contf': "continuous_on S f'" and f'im: "f' ` S \ T" and f'f: "\x. x \ C \ f' x = f x" - using extension_from_component [OF S \ANR T\ C contf fim] by metis - obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \ T" and g'g: "\x. x \ C \ g' x = g x" - using extension_from_component [OF S \ANR T\ C contg gim] by metis - have "homotopic_with_canon (\x. True) C T f' g'" - using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce - then show "homotopic_with_canon (\x. True) C T f g" - using f'f g'g homotopic_with_eq by force - qed -next - assume R [rule_format]: ?rhs - show ?lhs - proof clarify - fix f g - assume contf: "continuous_on S f" and fim: "f ` S \ T" - and contg: "continuous_on S g" and gim: "g ` S \ T" - moreover have "homotopic_with_canon (\x. True) C T f g" if "C \ components S" for C - using R [OF that] - by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that) - ultimately show "homotopic_with_canon (\x. True) S T f g" - by (subst homotopic_on_components_eq [OF S \ANR T\]) auto - qed -qed - -subsubsection\The complement of a set and path-connectedness\ - -text\Complement in dimension N > 1 of set homeomorphic to any interval in - any dimension is (path-)connected. This naively generalizes the argument - in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer fixed point theorem", -American Mathematical Monthly 1984.\ - -lemma unbounded_components_complement_absolute_retract: - fixes S :: "'a::euclidean_space set" - assumes C: "C \ components(- S)" and S: "compact S" "AR S" - shows "\ bounded C" -proof - - obtain y where y: "C = connected_component_set (- S) y" and "y \ S" - using C by (auto simp: components_def) - have "open(- S)" - using S by (simp add: closed_open compact_eq_bounded_closed) - have "S retract_of UNIV" - using S compact_AR by blast - then obtain r where contr: "continuous_on UNIV r" and ontor: "range r \ S" - and r: "\x. x \ S \ r x = x" - by (auto simp: retract_of_def retraction_def) - show ?thesis - proof - assume "bounded C" - have "connected_component_set (- S) y \ S" - proof (rule frontier_subset_retraction) - show "bounded (connected_component_set (- S) y)" - using \bounded C\ y by blast - show "frontier (connected_component_set (- S) y) \ S" - using C \compact S\ compact_eq_bounded_closed frontier_of_components_closed_complement y by blast - show "continuous_on (closure (connected_component_set (- S) y)) r" - by (blast intro: continuous_on_subset [OF contr]) - qed (use ontor r in auto) - with \y \ S\ show False by force - qed -qed - -lemma connected_complement_absolute_retract: - fixes S :: "'a::euclidean_space set" - assumes S: "compact S" "AR S" and 2: "2 \ DIM('a)" - shows "connected(- S)" -proof - - have "S retract_of UNIV" - using S compact_AR by blast - show ?thesis - apply (clarsimp simp: connected_iff_connected_component_eq) - apply (rule cobounded_unique_unbounded_component [OF _ 2]) - apply (simp add: \compact S\ compact_imp_bounded) - apply (meson ComplI S componentsI unbounded_components_complement_absolute_retract)+ - done -qed - -lemma path_connected_complement_absolute_retract: - fixes S :: "'a::euclidean_space set" - assumes "compact S" "AR S" "2 \ DIM('a)" - shows "path_connected(- S)" - using connected_complement_absolute_retract [OF assms] - using \compact S\ compact_eq_bounded_closed connected_open_path_connected by blast - -theorem connected_complement_homeomorphic_convex_compact: - fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" - assumes hom: "S homeomorphic T" and T: "convex T" "compact T" and 2: "2 \ DIM('a)" - shows "connected(- S)" -proof (cases "S = {}") - case True - then show ?thesis - by (simp add: connected_UNIV) -next - case False - show ?thesis - proof (rule connected_complement_absolute_retract) - show "compact S" - using \compact T\ hom homeomorphic_compactness by auto - show "AR S" - by (meson AR_ANR False \convex T\ convex_imp_ANR convex_imp_contractible hom homeomorphic_ANR_iff_ANR homeomorphic_contractible_eq) - qed (rule 2) -qed - -corollary path_connected_complement_homeomorphic_convex_compact: - fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" - assumes hom: "S homeomorphic T" "convex T" "compact T" "2 \ DIM('a)" - shows "path_connected(- S)" - using connected_complement_homeomorphic_convex_compact [OF assms] - using \compact T\ compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast - -lemma path_connected_complement_homeomorphic_interval: - fixes S :: "'a::euclidean_space set" - assumes "S homeomorphic cbox a b" "2 \ DIM('a)" - shows "path_connected(-S)" - using assms compact_cbox convex_box(1) path_connected_complement_homeomorphic_convex_compact by blast - -lemma connected_complement_homeomorphic_interval: - fixes S :: "'a::euclidean_space set" - assumes "S homeomorphic cbox a b" "2 \ DIM('a)" - shows "connected(-S)" - using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast - subsubsection \Proving surjectivity via Brouwer fixpoint theorem\ lemma brouwer_surjective: diff -r 0e2a065d6f31 -r de9c4ed2d5df src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 04 14:16:27 2019 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Sep 04 15:27:04 2019 +0100 @@ -3,7 +3,7 @@ text\By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\ theory Cauchy_Integral_Theorem -imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Ordered_Euclidean_Space +imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Retracts begin lemma leibniz_rule_holomorphic: diff -r 0e2a065d6f31 -r de9c4ed2d5df src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Wed Sep 04 14:16:27 2019 +0100 +++ b/src/HOL/Analysis/Further_Topology.thy Wed Sep 04 15:27:04 2019 +0100 @@ -3,21 +3,9 @@ text\Ported from HOL Light (moretop.ml) by L C Paulson\ theory Further_Topology - imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration + imports Weierstrass_Theorems Polytope Complex_Transcendental Equivalence_Lebesgue_Henstock_Integration Retracts begin -subsection\<^marker>\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\A map from a sphere to a higher dimensional sphere is nullhomotopic\ lemma spheremap_lemma1: diff -r 0e2a065d6f31 -r de9c4ed2d5df src/HOL/Analysis/Retracts.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Analysis/Retracts.thy Wed Sep 04 15:27:04 2019 +0100 @@ -0,0 +1,2591 @@ +section \Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\ + +theory Retracts + imports Brouwer_Fixpoint Ordered_Euclidean_Space +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 \\\<^sup>n\ can be +embedded as a closed subset of a convex subset of \\\<^sup>n\<^sup>+\<^sup>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\<^marker>\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\<^marker>\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\<^marker>\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')" + apply (intro continuous_on_compose f') + using continuous_on_subset contr f' apply blast + by (meson \homeomorphism S S' g h\ \r ` C \ S'\ continuous_on_subset \f' ` U \ C\ homeomorphism_def image_mono) + 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) + have h: "continuous_on S' h" " h ` S' \ S" + using hom homeomorphism_def apply blast + apply (metis hom equalityE homeomorphism_def) + done + 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')" + apply (intro continuous_on_compose h') + apply (meson hom continuous_on_subset h' homeomorphism_cont1) + done + 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" and hom: "S homeomorphic S'" + and clo: "closed S'" + shows "S' retract_of UNIV" +apply (rule AR_imp_absolute_retract [OF \AR S\ hom]) +using clo closed_closedin by auto + +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) + have h: "continuous_on T h" " h ` T \ S" + using hom homeomorphism_def apply blast + apply (metis hom equalityE homeomorphism_def) + done + 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')" + apply (intro continuous_on_compose h') + apply (meson hom continuous_on_subset h' homeomorphism_cont1) + done + 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)))" +apply (rule iffI) + apply (metis AR_imp_absolute_extensor) +apply (simp add: absolute_extensor_imp_AR) +done + +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 (meson \f ` T \ S\ continuous_on_subset homeomorphism_def homgh) + 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 (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 \ 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)" + using \f' ` U \ C\ by (auto simp: opD contf' continuous_openin_preimage) + have conth: "continuous_on (r ` f' ` (U \ f' -` D)) h" + apply (rule continuous_on_subset [of S']) + using homeomorphism_def homgh apply blast + using \r ` D \ S'\ by blast + show "continuous_on (U \ f' -` D) (h \ r \ f')" + apply (intro continuous_on_compose conth + continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto) + done + 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 (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) + have h: "continuous_on S' h" " h ` S' \ S" + using hom homeomorphism_def apply blast + apply (metis hom equalityE homeomorphism_def) + done + 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')" + apply (intro continuous_on_compose h') + apply (meson hom continuous_on_subset h' homeomorphism_cont1) + done + 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) + have h: "continuous_on T h" " h ` T \ S" + using hom homeomorphism_def apply blast + apply (metis hom equalityE homeomorphism_def) + done + 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')" + apply (intro continuous_on_compose h') + apply (meson hom continuous_on_subset h' homeomorphism_cont1) + done + show "(g \ h') ` V \ 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 + 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)))" +apply (rule iffI) + apply (metis ANR_imp_absolute_neighbourhood_extensor) +apply (simp add: absolute_neighbourhood_extensor_imp_ANR) +done + +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" + apply (rule retract_of_subset [OF S'Z]) + using US' \S' \ V\ \V \ W = {}\ closedin_subset apply fastforce + using Diff_subset_conv \U - Z \ W\ by blast + ultimately show ?thesis + apply (rule_tac V=V and W = "U-W" in that) + using openin_imp_subset apply force+ + done +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) + apply (rename_tac W) + apply (rule_tac W = "U \ W" in that, blast) + by (simp add: \S' \ U\ closedin_limpt) + 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" + apply (rule continuous_on_subset [of S]) + using hom homeomorphism_def apply blast + apply clarify + apply (meson \retraction X S r\ subsetD imageI retraction_def) + done + 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 + apply (rule_tac V = "W \ h -` X" in that) + apply (rule openin_trans [OF _ UW]) + using \continuous_on W h\ \open X\ continuous_openin_preimage_eq apply blast+ + done +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" +apply (rule homeomorphic_ENR_iff_ENR) +using assms homeomorphic_sym linear_homeomorphic_image by auto + +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" +apply (simp add: ANR_def) +by (metis 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\ + apply (simp add: ANR_def) + apply (drule_tac x=UNIV in spec) + apply (drule_tac x=T in spec, clarsimp) + apply (meson ENR_def ENR_homeomorphic_ENR open_openin) + done +qed + + +lemma AR_ANR: + fixes S :: "'a::euclidean_space set" + shows "AR S \ ANR S \ contractible S \ S \ {}" + (is "?lhs = ?rhs") +proof + assume ?lhs + obtain C and S' :: "('a * real) set" + where "convex C" "C \ {}" "closedin (top_of_set C) S'" "S homeomorphic S'" + apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"]) + using aff_dim_le_DIM [of S] by auto + with \AR S\ have "contractible S" + apply (simp add: AR_def) + apply (drule_tac x=C in spec) + apply (drule_tac x="S'" in spec, simp) + using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce + with \AR S\ show ?rhs + apply (auto simp: AR_imp_ANR) + apply (force simp: AR_def) + done +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))" + apply (rule continuous_on_compose2 [OF conth continuous_on_Pair]) + apply (rule continuous_on_subset [OF contj Diff_subset]) + apply (rule continuous_on_subset [OF contg]) + apply (metis Diff_subset_conv Un_commute \W - U \ V'\) + using j \g ` U \ S\ \W - U \ V'\ apply fastforce + done + show "continuous_on W (\x. if x \ W - V then a else h (j x, g x))" + apply (subst Weq) + apply (rule continuous_on_cases_local) + apply (simp_all add: Weq [symmetric] WWV continuous_on_const *) + using WV' closedin_diff apply fastforce + apply (auto simp: j0 j1) + done + 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) +qed + + +lemma ANR_retract_of_ANR: + fixes S :: "'a::euclidean_space set" + assumes "ANR T" "S retract_of T" + shows "ANR S" +using assms +apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def) +apply (clarsimp elim!: all_forward) +apply (erule impCE, metis subset_trans) +apply (clarsimp elim!: ex_forward) +apply (rule_tac x="r \ g" in exI) +by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans) + +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" +apply (rule absolute_extensor_imp_AR) +apply (rule Dugundji, assumption+) +by blast + +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" + apply (rule AR_imp_absolute_retract [OF \AR(S \ T)\]) + apply (simp add: homeomorphic_refl) + apply (rule closedin_subset_trans [of U]) + apply (simp_all add: assms closedin_Int \S \ T \ W\ \W \ U\) + done + 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 "r ` (W \ S) \ S" "r ` (W \ T) \ T" + using \r0 ` W \ S \ T\ r_def by auto + 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 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" + apply (rule AR_imp_absolute_extensor [OF \AR S\ _ _ cloUWS]) + apply (rule continuous_on_subset [OF contr]) + using \r ` (W \ S) \ S\ apply auto + done + 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" + apply (rule AR_imp_absolute_extensor [OF \AR T\ _ _ cloUWT]) + apply (rule continuous_on_subset [OF contr]) + using \r ` (W \ T) \ T\ apply auto + done + have "U = S' \ T'" + by (force simp: S'_def T'_def) + then have cont: "continuous_on U (\x. if x \ S' then g x else h x)" + apply (rule ssubst) + apply (rule continuous_on_cases_local) + using US' UT' \S' \ T' = W\ \U = S' \ T'\ + contg conth continuous_on_subset geqr heqr apply auto + done + 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) + apply (intro conjI cont UST) + by (metis IntI ST Un_iff \S \ S'\ \S' \ T' = W\ \T \ T'\ subsetD geqr heqr r0 r_def) +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)" + apply (rule closedin_trans [OF _ UC]) + apply (rule continuous_closedin_preimage_gen [OF _ _ STS]) + using hom homeomorphism_def apply blast + apply (metis hom homeomorphism_def set_eq_subset) + done + have UT: "closedin (top_of_set U) (C \ g -` T)" + apply (rule closedin_trans [OF _ UC]) + apply (rule continuous_closedin_preimage_gen [OF _ _ STT]) + using hom homeomorphism_def apply blast + apply (metis hom homeomorphism_def set_eq_subset) + done + have ARS: "AR (C \ g -` S)" + apply (rule AR_homeomorphic_AR [OF \AR S\]) + apply (simp add: homeomorphic_def) + apply (rule_tac x=g in exI) + apply (rule_tac x=f in exI) + using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) + apply (rule_tac x="f x" in image_eqI, auto) + done + have ART: "AR (C \ g -` T)" + apply (rule AR_homeomorphic_AR [OF \AR T\]) + apply (simp add: homeomorphic_def) + apply (rule_tac x=g in exI) + apply (rule_tac x=f in exI) + using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) + apply (rule_tac x="f x" in image_eqI, auto) + done + have ARI: "AR ((C \ g -` S) \ (C \ g -` T))" + apply (rule AR_homeomorphic_AR [OF \AR (S \ T)\]) + apply (simp add: homeomorphic_def) + apply (rule_tac x=g in exI) + apply (rule_tac x=f in exI) + using hom + apply (auto simp: homeomorphism_def elim!: continuous_on_subset) + apply (rule_tac x="f x" in image_eqI, auto) + done + 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" + apply (rule ANR_imp_closed_neighbourhood_retract [OF \ANR(S \ T)\]) + apply (rule closedin_subset_trans [of U, OF _ ST_W \W \ U\]) + apply (blast intro: assms)+ + done + 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" + apply (rule closedin_subset_trans [of U]) + using cloWW0 cloUW closedin_trans \W0 \ U\ \S \ U\ \T \ U\ apply blast+ + done + 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" + apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ _ \r ` (W0 \ S) \ S\ cloS'WS]) + apply (rule continuous_on_subset [OF contr], blast+) + done + 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" + apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ _ \r ` (W0 \ T) \ T\ cloT'WT]) + apply (rule continuous_on_subset [OF contr], blast+) + done + have "S' \ T' = W" + by (force simp: S'_def T'_def W_def) + obtain O1 O2 where "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)" + 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) (W1 - (W - U0) \ (W2 - (W - U0)))" + apply (subst eq) + apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \open O1\ \open O2\, simp_all) + done + have cloW1: "closedin (top_of_set (W1 - (W - U0) \ (W2 - (W - U0)))) (W1 - (W - U0))" + using cloUS' apply (simp add: closedin_closed) + apply (erule ex_forward) + using U0 \W0 \ S \ W1\ + apply (auto simp: \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = U\ [symmetric]\S' \ T' = W\ [symmetric]) + done + have cloW2: "closedin (top_of_set (W1 - (W - U0) \ (W2 - (W - U0)))) (W2 - (W - U0))" + using cloUT' apply (simp add: closedin_closed) + apply (erule ex_forward) + using U0 \W0 \ T \ W2\ + apply (auto simp: \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = U\ [symmetric]\S' \ T' = W\ [symmetric]) + done + have *: "\x\S \ T. (if x \ S' then g x else h x) = x" + using ST \S' \ T' = W\ cloT'WT closedin_subset geqr heqr + apply (auto simp: r_def, fastforce) + using \S \ S'\ \T \ T'\ \W0 \ S \ W1\ \W1 = S' \ O1\ by auto + have "\r. continuous_on (W1 - (W - U0) \ (W2 - (W - U0))) r \ + r ` (W1 - (W - U0) \ (W2 - (W - U0))) \ S \ T \ + (\x\S \ T. r x = x)" + apply (rule_tac x = "\x. if x \ S' then g x else h x" in exI) + apply (intro conjI *) + apply (rule continuous_on_cases_local + [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]]) + using \W1 = S' \ O1\ \W2 = T' \ O2\ \S' \ T' = W\ + \g ` W1 \ S\ \h ` W2 \ T\ apply auto + using \U0 \ W \ W0\ \W0 \ S \ W1\ apply (fastforce simp add: geqr heqr)+ + done + then show "S \ T retract_of W1 - (W - U0) \ (W2 - (W - U0))" + using \W0 \ S \ W1\ \W0 \ T \ W2\ ST opeUU0 U0 + by (auto simp: retract_of_def retraction_def) + 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)" + apply (rule closedin_trans [OF _ UC]) + apply (rule continuous_closedin_preimage_gen [OF _ _ STS]) + using hom [unfolded homeomorphism_def] apply blast + apply (metis hom homeomorphism_def set_eq_subset) + done + have UT: "closedin (top_of_set U) (C \ g -` T)" + apply (rule closedin_trans [OF _ UC]) + apply (rule continuous_closedin_preimage_gen [OF _ _ STT]) + using hom [unfolded homeomorphism_def] apply blast + apply (metis hom homeomorphism_def set_eq_subset) + done + have ANRS: "ANR (C \ g -` S)" + apply (rule ANR_homeomorphic_ANR [OF \ANR S\]) + apply (simp add: homeomorphic_def) + apply (rule_tac x=g in exI) + apply (rule_tac x=f in exI) + using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) + apply (rule_tac x="f x" in image_eqI, auto) + done + have ANRT: "ANR (C \ g -` T)" + apply (rule ANR_homeomorphic_ANR [OF \ANR T\]) + apply (simp add: homeomorphic_def) + apply (rule_tac x=g in exI) + apply (rule_tac x=f in exI) + using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset) + apply (rule_tac x="f x" in image_eqI, auto) + done + have ANRI: "ANR ((C \ g -` S) \ (C \ g -` T))" + apply (rule ANR_homeomorphic_ANR [OF \ANR (S \ T)\]) + apply (simp add: homeomorphic_def) + apply (rule_tac x=g in exI) + apply (rule_tac x=f in exI) + using hom + apply (auto simp: homeomorphism_def elim!: continuous_on_subset) + apply (rule_tac x="f x" in image_eqI, auto) + done + 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" + apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf \f ` C \ T\ cloUC]) + using 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" and opeTS: "openin (top_of_set T) S" + shows "ENR S" + using assms apply (simp add: ENR_ANR) + using ANR_openin locally_open_subset by blast + +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)" +apply (simp add: ENR_convex_closed closed_cbox) +by (simp add: 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" + apply (rule homeomorphic_closedin_convex [of S]) + using aff_dim_le_DIM [of S] apply auto + done + 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 + show ?thesis + using assms + apply (clarsimp simp: ANR_def) + apply (drule_tac x=U in spec) + apply (drule_tac x=T in spec) + using \S homeomorphic T\ \U \ {}\ UT apply (blast intro: S) + done +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" + apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR S\ contf1 _ cloUC]) + using fim apply auto + done + 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" + apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \ANR T\ contf2 _ cloUC]) + using fim apply auto + done + 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) + +subsection\<^marker>\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}" + apply (simp add: 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}))" + apply (rule continuous_openin_preimage_gen) + apply (auto simp: False affine_imp_convex continuous_on_closest_point) + done + ultimately show ?thesis + unfolding ENR_def + apply (rule_tac x = "closest_point (affine hull S) -` (- {a})" in exI) + apply (simp add: vimage_def) + done +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)" + apply (rule continuous_on_cases_local [OF clS clT]) + using r by (auto simp: continuous_on_id) + 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" + apply (rule AR_retract_of_AR [OF Un]) + by (meson AR_imp_retract clS clT 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 Int_lower1 continuous_on_subset r) + qed (use req continuous_on_id in auto) + with rim have "S retract_of S \ V" + unfolding retraction_def retract_of_def + apply (rule_tac x="\x. if x \ S then x else r x" in exI) + apply (auto simp: eq') + done + then show ?thesis + using ANR_neighborhood_retract [OF Un] + using \S \ V = S \ T - T \ V\ clT ope by fastforce +qed + +lemma ANR_from_Un_Int: + fixes S :: "'a::euclidean_space set" + assumes clo: "closed S" "closed T" and Un: "ANR(S \ T)" and Int: "ANR(S \ T)" + shows "ANR S" + 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) + +lemma ANR_finite_Union_convex_closed: + fixes \ :: "'a::euclidean_space set set" + assumes \: "finite \" and clo: "\C. C \ \ \ closed C" and con: "\C. C \ \ \ convex C" + shows "ANR(\\)" +proof - + have "ANR(\\)" if "card \ < n" for n + using assms that + proof (induction n arbitrary: \) + case 0 then show ?case by simp + next + case (Suc n) + have "ANR(\\)" if "finite \" "\ \ \" for \ + using that + proof (induction \) + case empty + then show ?case by simp + next + case (insert C \) + have "ANR (C \ \\)" + proof (rule ANR_closed_Un) + show "ANR (C \ \\)" + unfolding Int_Union + proof (rule Suc) + show "finite ((\) C ` \)" + by (simp add: insert.hyps(1)) + show "\Ca. Ca \ (\) C ` \ \ closed Ca" + by (metis (no_types, hide_lams) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2) + show "\Ca. Ca \ (\) C ` \ \ convex Ca" + by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE) + show "card ((\) C ` \) < n" + proof - + have "card \ \ n" + by (meson Suc.prems(4) not_less not_less_eq) + then show ?thesis + by (metis Suc.prems(1) card_image_le card_seteq insert.hyps insert.prems insert_subset le_trans not_less) + qed + qed + show "closed (\\)" + using Suc.prems(2) insert.hyps(1) insert.prems by blast + qed (use Suc.prems convex_imp_ANR insert.prems insert.IH in auto) + then show ?case + by simp + qed + then show ?case + using Suc.prems(1) by blast + qed + then show ?thesis + by blast +qed + + +lemma finite_imp_ANR: + fixes S :: "'a::euclidean_space set" + assumes "finite S" + shows "ANR S" +proof - + have "ANR(\x \ S. {x})" + by (blast intro: ANR_finite_Union_convex_closed assms) + then show ?thesis + by simp +qed + +lemma ANR_insert: + fixes S :: "'a::euclidean_space set" + assumes "ANR S" "closed S" + shows "ANR(insert a S)" + by (metis ANR_closed_Un ANR_empty ANR_singleton Diff_disjoint Diff_insert_absorb assms closed_singleton insert_absorb insert_is_Un) + +lemma ANR_path_component_ANR: + fixes S :: "'a::euclidean_space set" + shows "ANR S \ ANR(path_component_set S x)" + using ANR_imp_locally_path_connected ANR_openin openin_path_component_locally_path_connected by blast + +lemma ANR_connected_component_ANR: + fixes S :: "'a::euclidean_space set" + shows "ANR S \ ANR(connected_component_set S x)" + by (metis ANR_openin openin_connected_component_locally_connected ANR_imp_locally_connected) + +lemma ANR_component_ANR: + fixes S :: "'a::euclidean_space set" + assumes "ANR S" "c \ components S" + shows "ANR c" + by (metis ANR_connected_component_ANR assms componentsE) + +subsection\Original ANR material, now for ENRs\ + +lemma ENR_bounded: + fixes S :: "'a::euclidean_space set" + assumes "bounded S" + shows "ENR S \ (\U. open U \ bounded U \ S retract_of U)" + (is "?lhs = ?rhs") +proof + obtain r where "0 < r" and r: "S \ ball 0 r" + using bounded_subset_ballD assms by blast + assume ?lhs + then show ?rhs + apply (clarsimp simp: ENR_def) + apply (rule_tac x="ball 0 r \ U" in exI, auto) + using r retract_of_imp_subset retract_of_subset by fastforce +next + assume ?rhs + then show ?lhs + using ENR_def by blast +qed + +lemma absolute_retract_imp_AR_gen: + fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" + assumes "S retract_of T" "convex T" "T \ {}" "S homeomorphic S'" "closedin (top_of_set U) S'" + shows "S' retract_of U" +proof - + have "AR T" + by (simp add: assms convex_imp_AR) + then have "AR S" + using AR_retract_of_AR assms by auto + then show ?thesis + using assms AR_imp_absolute_retract by metis +qed + +lemma absolute_retract_imp_AR: + fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" + assumes "S retract_of UNIV" "S homeomorphic S'" "closed S'" + shows "S' retract_of UNIV" + using AR_imp_absolute_retract_UNIV assms retract_of_UNIV by blast + +lemma homeomorphic_compact_arness: + fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set" + assumes "S homeomorphic S'" + shows "compact S \ S retract_of UNIV \ compact S' \ S' retract_of UNIV" + using assms homeomorphic_compactness + apply auto + apply (meson assms compact_AR homeomorphic_AR_iff_AR homeomorphic_compactness)+ + done + +lemma absolute_retract_from_Un_Int: + fixes S :: "'a::euclidean_space set" + assumes "(S \ T) retract_of UNIV" "(S \ T) retract_of UNIV" "closed S" "closed T" + shows "S retract_of UNIV" + using AR_from_Un_Int assms retract_of_UNIV by auto + +lemma ENR_from_Un_Int_gen: + fixes S :: "'a::euclidean_space set" + assumes "closedin (top_of_set (S \ T)) S" "closedin (top_of_set (S \ T)) T" "ENR(S \ T)" "ENR(S \ T)" + shows "ENR S" + apply (simp add: ENR_ANR) + using ANR_from_Un_Int_local ENR_ANR assms locally_compact_closedin by blast + + +lemma ENR_from_Un_Int: + fixes S :: "'a::euclidean_space set" + assumes "closed S" "closed T" "ENR(S \ T)" "ENR(S \ T)" + shows "ENR S" + by (meson ENR_from_Un_Int_gen assms closed_subset sup_ge1 sup_ge2) + + +lemma ENR_finite_Union_convex_closed: + fixes \ :: "'a::euclidean_space set set" + assumes \: "finite \" and clo: "\C. C \ \ \ closed C" and con: "\C. C \ \ \ convex C" + shows "ENR(\ \)" + by (simp add: ENR_ANR ANR_finite_Union_convex_closed \ clo closed_Union closed_imp_locally_compact con) + +lemma finite_imp_ENR: + fixes S :: "'a::euclidean_space set" + shows "finite S \ ENR S" + by (simp add: ENR_ANR finite_imp_ANR finite_imp_closed closed_imp_locally_compact) + +lemma ENR_insert: + fixes S :: "'a::euclidean_space set" + assumes "closed S" "ENR S" + shows "ENR(insert a S)" +proof - + have "ENR ({a} \ S)" + by (metis ANR_insert ENR_ANR Un_commute Un_insert_right assms closed_imp_locally_compact closed_insert sup_bot_right) + then show ?thesis + by auto +qed + +lemma ENR_path_component_ENR: + fixes S :: "'a::euclidean_space set" + assumes "ENR S" + shows "ENR(path_component_set S x)" + by (metis ANR_imp_locally_path_connected ENR_empty ENR_imp_ANR ENR_openin assms + locally_path_connected_2 openin_subtopology_self path_component_eq_empty) + +(*UNUSED +lemma ENR_Times: + fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" + assumes "ENR S" "ENR T" shows "ENR(S \ T)" +using assms apply (simp add: ENR_ANR ANR_Times) +thm locally_compact_Times +oops + SIMP_TAC[ENR_ANR; ANR_PCROSS; LOCALLY_COMPACT_PCROSS]);; +*) + +subsection\Finally, spheres are ANRs and ENRs\ + +lemma absolute_retract_homeomorphic_convex_compact: + fixes S :: "'a::euclidean_space set" and U :: "'b::euclidean_space set" + assumes "S homeomorphic U" "S \ {}" "S \ T" "convex U" "compact U" + shows "S retract_of T" + by (metis UNIV_I assms compact_AR convex_imp_AR homeomorphic_AR_iff_AR homeomorphic_compactness homeomorphic_empty(1) retract_of_subset subsetI) + +lemma frontier_retract_of_punctured_universe: + fixes S :: "'a::euclidean_space set" + assumes "convex S" "bounded S" "a \ interior S" + shows "(frontier S) retract_of (- {a})" + using rel_frontier_retract_of_punctured_affine_hull + by (metis Compl_eq_Diff_UNIV affine_hull_nonempty_interior assms empty_iff rel_frontier_frontier rel_interior_nonempty_interior) + +lemma sphere_retract_of_punctured_universe_gen: + fixes a :: "'a::euclidean_space" + assumes "b \ ball a r" + shows "sphere a r retract_of (- {b})" +proof - + have "frontier (cball a r) retract_of (- {b})" + apply (rule frontier_retract_of_punctured_universe) + using assms by auto + then show ?thesis + by simp +qed + +lemma sphere_retract_of_punctured_universe: + fixes a :: "'a::euclidean_space" + assumes "0 < r" + shows "sphere a r retract_of (- {a})" + by (simp add: assms sphere_retract_of_punctured_universe_gen) + +lemma ENR_sphere: + fixes a :: "'a::euclidean_space" + shows "ENR(sphere a r)" +proof (cases "0 < r") + case True + then have "sphere a r retract_of -{a}" + by (simp add: sphere_retract_of_punctured_universe) + with open_delete show ?thesis + by (auto simp: ENR_def) +next + case False + then show ?thesis + using finite_imp_ENR + by (metis finite_insert infinite_imp_nonempty less_linear sphere_eq_empty sphere_trivial) +qed + +corollary\<^marker>\tag unimportant\ ANR_sphere: + fixes a :: "'a::euclidean_space" + shows "ANR(sphere a r)" + by (simp add: ENR_imp_ANR ENR_sphere) + +subsection\Spheres are connected, etc\ + +lemma locally_path_connected_sphere_gen: + fixes S :: "'a::euclidean_space set" + assumes "bounded S" and "convex S" + shows "locally path_connected (rel_frontier S)" +proof (cases "rel_interior S = {}") + case True + with assms show ?thesis + by (simp add: rel_interior_eq_empty) +next + case False + then obtain a where a: "a \ rel_interior S" + by blast + show ?thesis + proof (rule retract_of_locally_path_connected) + show "locally path_connected (affine hull S - {a})" + by (meson convex_affine_hull convex_imp_locally_path_connected locally_open_subset openin_delete openin_subtopology_self) + show "rel_frontier S retract_of affine hull S - {a}" + using a assms rel_frontier_retract_of_punctured_affine_hull by blast + qed +qed + +lemma locally_connected_sphere_gen: + fixes S :: "'a::euclidean_space set" + assumes "bounded S" and "convex S" + shows "locally connected (rel_frontier S)" + by (simp add: ANR_imp_locally_connected ANR_rel_frontier_convex assms) + +lemma locally_path_connected_sphere: + fixes a :: "'a::euclidean_space" + shows "locally path_connected (sphere a r)" + using ENR_imp_locally_path_connected ENR_sphere by blast + +lemma locally_connected_sphere: + fixes a :: "'a::euclidean_space" + shows "locally connected(sphere a r)" + using ANR_imp_locally_connected ANR_sphere by blast + +subsection\Borsuk homotopy extension theorem\ + +text\It's only this late so we can use the concept of retraction, + saying that the domain sets or range set are ENRs.\ + +theorem Borsuk_homotopy_extension_homotopic: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes cloTS: "closedin (top_of_set T) S" + and anr: "(ANR S \ ANR T) \ ANR U" + and contf: "continuous_on T f" + and "f ` T \ U" + and "homotopic_with_canon (\x. True) S U f g" + obtains g' where "homotopic_with_canon (\x. True) T U f g'" + "continuous_on T g'" "image g' T \ U" + "\x. x \ S \ g' x = g x" +proof - + have "S \ T" using assms closedin_imp_subset by blast + obtain h where conth: "continuous_on ({0..1} \ S) h" + and him: "h ` ({0..1} \ S) \ U" + and [simp]: "\x. h(0, x) = f x" "\x. h(1::real, x) = g x" + using assms by (auto simp: homotopic_with_def) + define h' where "h' \ \z. if snd z \ S then h z else (f \ snd) z" + define B where "B \ {0::real} \ T \ {0..1} \ S" + have clo0T: "closedin (top_of_set ({0..1} \ T)) ({0::real} \ T)" + by (simp add: Abstract_Topology.closedin_Times) + moreover have cloT1S: "closedin (top_of_set ({0..1} \ T)) ({0..1} \ S)" + by (simp add: Abstract_Topology.closedin_Times assms) + ultimately have clo0TB:"closedin (top_of_set ({0..1} \ T)) B" + by (auto simp: B_def) + have cloBS: "closedin (top_of_set B) ({0..1} \ S)" + by (metis (no_types) Un_subset_iff B_def closedin_subset_trans [OF cloT1S] clo0TB closedin_imp_subset closedin_self) + moreover have cloBT: "closedin (top_of_set B) ({0} \ T)" + using \S \ T\ closedin_subset_trans [OF clo0T] + by (metis B_def Un_upper1 clo0TB closedin_closed inf_le1) + moreover have "continuous_on ({0} \ T) (f \ snd)" + apply (rule continuous_intros)+ + apply (simp add: contf) + done + ultimately have conth': "continuous_on B h'" + apply (simp add: h'_def B_def Un_commute [of "{0} \ T"]) + apply (auto intro!: continuous_on_cases_local conth) + done + have "image h' B \ U" + using \f ` T \ U\ him by (auto simp: h'_def B_def) + obtain V k where "B \ V" and opeTV: "openin (top_of_set ({0..1} \ T)) V" + and contk: "continuous_on V k" and kim: "k ` V \ U" + and keq: "\x. x \ B \ k x = h' x" + using anr + proof + assume ST: "ANR S \ ANR T" + have eq: "({0} \ T \ {0..1} \ S) = {0::real} \ S" + using \S \ T\ by auto + have "ANR B" + apply (simp add: B_def) + apply (rule ANR_closed_Un_local) + apply (metis cloBT B_def) + apply (metis Un_commute cloBS B_def) + apply (simp_all add: ANR_Times convex_imp_ANR ANR_singleton ST eq) + done + note Vk = that + have *: thesis if "openin (top_of_set ({0..1::real} \ T)) V" + "retraction V B r" for V r + using that + apply (clarsimp simp add: retraction_def) + apply (rule Vk [of V "h' \ r"], assumption+) + apply (metis continuous_on_compose conth' continuous_on_subset) + using \h' ` B \ U\ apply force+ + done + show thesis + apply (rule ANR_imp_neighbourhood_retract [OF \ANR B\ clo0TB]) + apply (auto simp: ANR_Times ANR_singleton ST retract_of_def *) + done + next + assume "ANR U" + with ANR_imp_absolute_neighbourhood_extensor \h' ` B \ U\ clo0TB conth' that + show ?thesis by blast + qed + define S' where "S' \ {x. \u::real. u \ {0..1} \ (u, x::'a) \ {0..1} \ T - V}" + have "closedin (top_of_set T) S'" + unfolding S'_def + apply (rule closedin_compact_projection, blast) + using closedin_self opeTV by blast + have S'_def: "S' = {x. \u::real. (u, x::'a) \ {0..1} \ T - V}" + by (auto simp: S'_def) + have cloTS': "closedin (top_of_set T) S'" + using S'_def \closedin (top_of_set T) S'\ by blast + have "S \ S' = {}" + using S'_def B_def \B \ V\ by force + obtain a :: "'a \ real" where conta: "continuous_on T a" + and "\x. x \ T \ a x \ closed_segment 1 0" + and a1: "\x. x \ S \ a x = 1" + and a0: "\x. x \ S' \ a x = 0" + apply (rule Urysohn_local [OF cloTS cloTS' \S \ S' = {}\, of 1 0], blast) + done + then have ain: "\x. x \ T \ a x \ {0..1}" + using closed_segment_eq_real_ivl by auto + have inV: "(u * a t, t) \ V" if "t \ T" "0 \ u" "u \ 1" for t u + proof (rule ccontr) + assume "(u * a t, t) \ V" + with ain [OF \t \ T\] have "a t = 0" + apply simp + apply (rule a0) + by (metis (no_types, lifting) Diff_iff S'_def SigmaI atLeastAtMost_iff mem_Collect_eq mult_le_one mult_nonneg_nonneg that) + show False + using B_def \(u * a t, t) \ V\ \B \ V\ \a t = 0\ that by auto + qed + show ?thesis + proof + show hom: "homotopic_with_canon (\x. True) T U f (\x. k (a x, x))" + proof (simp add: homotopic_with, intro exI conjI) + show "continuous_on ({0..1} \ T) (k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z)))" + apply (intro continuous_on_compose continuous_intros) + apply (rule continuous_on_subset [OF conta], force) + apply (rule continuous_on_subset [OF contk]) + apply (force intro: inV) + done + show "(k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z))) ` ({0..1} \ T) \ U" + using inV kim by auto + show "\x\T. (k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z))) (0, x) = f x" + by (simp add: B_def h'_def keq) + show "\x\T. (k \ (\z. (fst z *\<^sub>R (a \ snd) z, snd z))) (1, x) = k (a x, x)" + by auto + qed + show "continuous_on T (\x. k (a x, x))" + using homotopic_with_imp_continuous_maps [OF hom] by auto + show "(\x. k (a x, x)) ` T \ U" + proof clarify + fix t + assume "t \ T" + show "k (a t, t) \ U" + by (metis \t \ T\ image_subset_iff inV kim not_one_le_zero linear mult_cancel_right1) + qed + show "\x. x \ S \ k (a x, x) = g x" + by (simp add: B_def a1 h'_def keq) + qed +qed + + +corollary\<^marker>\tag unimportant\ nullhomotopic_into_ANR_extension: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "closed S" + and contf: "continuous_on S f" + and "ANR T" + and fim: "f ` S \ T" + and "S \ {}" + shows "(\c. homotopic_with_canon (\x. True) S T f (\x. c)) \ + (\g. continuous_on UNIV g \ range g \ T \ (\x \ S. g x = f x))" + (is "?lhs = ?rhs") +proof + assume ?lhs + then obtain c where c: "homotopic_with_canon (\x. True) S T (\x. c) f" + by (blast intro: homotopic_with_symD) + have "closedin (top_of_set UNIV) S" + using \closed S\ closed_closedin by fastforce + then obtain g where "continuous_on UNIV g" "range g \ T" + "\x. x \ S \ g x = f x" + apply (rule Borsuk_homotopy_extension_homotopic [OF _ _ continuous_on_const _ c, where T=UNIV]) + using \ANR T\ \S \ {}\ c homotopic_with_imp_subset1 apply fastforce+ + done + then show ?rhs by blast +next + assume ?rhs + then obtain g where "continuous_on UNIV g" "range g \ T" "\x. x\S \ g x = f x" + by blast + then obtain c where "homotopic_with_canon (\h. True) UNIV T g (\x. c)" + using nullhomotopic_from_contractible [of UNIV g T] contractible_UNIV by blast + then have "homotopic_with_canon (\x. True) S T g (\x. c)" + by (simp add: homotopic_from_subtopology) + then show ?lhs + by (force elim: homotopic_with_eq [of _ _ _ g "\x. c"] simp: \\x. x \ S \ g x = f x\) +qed + +corollary\<^marker>\tag unimportant\ nullhomotopic_into_rel_frontier_extension: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes "closed S" + and contf: "continuous_on S f" + and "convex T" "bounded T" + and fim: "f ` S \ rel_frontier T" + and "S \ {}" + shows "(\c. homotopic_with_canon (\x. True) S (rel_frontier T) f (\x. c)) \ + (\g. continuous_on UNIV g \ range g \ rel_frontier T \ (\x \ S. g x = f x))" +by (simp add: nullhomotopic_into_ANR_extension assms ANR_rel_frontier_convex) + +corollary\<^marker>\tag unimportant\ nullhomotopic_into_sphere_extension: + fixes f :: "'a::euclidean_space \ 'b :: euclidean_space" + assumes "closed S" and contf: "continuous_on S f" + and "S \ {}" and fim: "f ` S \ sphere a r" + shows "((\c. homotopic_with_canon (\x. True) S (sphere a r) f (\x. c)) \ + (\g. continuous_on UNIV g \ range g \ sphere a r \ (\x \ S. g x = f x)))" + (is "?lhs = ?rhs") +proof (cases "r = 0") + case True with fim show ?thesis + apply auto + using fim continuous_on_const apply fastforce + by (metis contf contractible_sing nullhomotopic_into_contractible) +next + case False + then have eq: "sphere a r = rel_frontier (cball a r)" by simp + show ?thesis + using fim unfolding eq + apply (rule nullhomotopic_into_rel_frontier_extension [OF \closed S\ contf convex_cball bounded_cball]) + apply (rule \S \ {}\) + done +qed + +proposition\<^marker>\tag unimportant\ Borsuk_map_essential_bounded_component: + fixes a :: "'a :: euclidean_space" + assumes "compact S" and "a \ S" + shows "bounded (connected_component_set (- S) a) \ + \(\c. homotopic_with_canon (\x. True) S (sphere 0 1) + (\x. inverse(norm(x - a)) *\<^sub>R (x - a)) (\x. c))" + (is "?lhs = ?rhs") +proof (cases "S = {}") + case True then show ?thesis + by simp +next + case False + have "closed S" "bounded S" + using \compact S\ compact_eq_bounded_closed by auto + have s01: "(\x. (x - a) /\<^sub>R norm (x - a)) ` S \ sphere 0 1" + using \a \ S\ by clarsimp (metis dist_eq_0_iff dist_norm mult.commute right_inverse) + have aincc: "a \ connected_component_set (- S) a" + by (simp add: \a \ S\) + obtain r where "r>0" and r: "S \ ball 0 r" + using bounded_subset_ballD \bounded S\ by blast + have "\ ?rhs \ \ ?lhs" + proof + assume notr: "\ ?rhs" + have nog: "\g. continuous_on (S \ connected_component_set (- S) a) g \ + g ` (S \ connected_component_set (- S) a) \ sphere 0 1 \ + (\x\S. g x = (x - a) /\<^sub>R norm (x - a))" + if "bounded (connected_component_set (- S) a)" + apply (rule non_extensible_Borsuk_map [OF \compact S\ componentsI _ aincc]) + using \a \ S\ that by auto + obtain g where "range g \ sphere 0 1" "continuous_on UNIV g" + "\x. x \ S \ g x = (x - a) /\<^sub>R norm (x - a)" + using notr + by (auto simp: nullhomotopic_into_sphere_extension + [OF \closed S\ continuous_on_Borsuk_map [OF \a \ S\] False s01]) + with \a \ S\ show "\ ?lhs" + apply (clarsimp simp: Borsuk_map_into_sphere [of a S, symmetric] dest!: nog) + apply (drule_tac x=g in spec) + using continuous_on_subset by fastforce + next + assume "\ ?lhs" + then obtain b where b: "b \ connected_component_set (- S) a" and "r \ norm b" + using bounded_iff linear by blast + then have bnot: "b \ ball 0 r" + by simp + have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. (x - a) /\<^sub>R norm (x - a)) + (\x. (x - b) /\<^sub>R norm (x - b))" + apply (rule Borsuk_maps_homotopic_in_path_component) + using \closed S\ b open_Compl open_path_connected_component apply fastforce + done + moreover + obtain c where "homotopic_with_canon (\x. True) (ball 0 r) (sphere 0 1) + (\x. inverse (norm (x - b)) *\<^sub>R (x - b)) (\x. c)" + proof (rule nullhomotopic_from_contractible) + show "contractible (ball (0::'a) r)" + by (metis convex_imp_contractible convex_ball) + show "continuous_on (ball 0 r) (\x. inverse(norm (x - b)) *\<^sub>R (x - b))" + by (rule continuous_on_Borsuk_map [OF bnot]) + show "(\x. (x - b) /\<^sub>R norm (x - b)) ` ball 0 r \ sphere 0 1" + using bnot Borsuk_map_into_sphere by blast + qed blast + ultimately have "homotopic_with_canon (\x. True) S (sphere 0 1) (\x. (x - a) /\<^sub>R norm (x - a)) (\x. c)" + by (meson homotopic_with_subset_left homotopic_with_trans r) + then show "\ ?rhs" + by blast + qed + then show ?thesis by blast +qed + +lemma homotopic_Borsuk_maps_in_bounded_component: + fixes a :: "'a :: euclidean_space" + assumes "compact S" and "a \ S"and "b \ S" + and boc: "bounded (connected_component_set (- S) a)" + and hom: "homotopic_with_canon (\x. True) S (sphere 0 1) + (\x. (x - a) /\<^sub>R norm (x - a)) + (\x. (x - b) /\<^sub>R norm (x - b))" + shows "connected_component (- S) a b" +proof (rule ccontr) + assume notcc: "\ connected_component (- S) a b" + let ?T = "S \ connected_component_set (- S) a" + have "\g. continuous_on (S \ connected_component_set (- S) a) g \ + g ` (S \ connected_component_set (- S) a) \ sphere 0 1 \ + (\x\S. g x = (x - a) /\<^sub>R norm (x - a))" + by (simp add: \a \ S\ componentsI non_extensible_Borsuk_map [OF \compact S\ _ boc]) + moreover obtain g where "continuous_on (S \ connected_component_set (- S) a) g" + "g ` (S \ connected_component_set (- S) a) \ sphere 0 1" + "\x. x \ S \ g x = (x - a) /\<^sub>R norm (x - a)" + proof (rule Borsuk_homotopy_extension_homotopic) + show "closedin (top_of_set ?T) S" + by (simp add: \compact S\ closed_subset compact_imp_closed) + show "continuous_on ?T (\x. (x - b) /\<^sub>R norm (x - b))" + by (simp add: \b \ S\ notcc continuous_on_Borsuk_map) + show "(\x. (x - b) /\<^sub>R norm (x - b)) ` ?T \ sphere 0 1" + by (simp add: \b \ S\ notcc Borsuk_map_into_sphere) + show "homotopic_with_canon (\x. True) S (sphere 0 1) + (\x. (x - b) /\<^sub>R norm (x - b)) (\x. (x - a) /\<^sub>R norm (x - a))" + by (simp add: hom homotopic_with_symD) + qed (auto simp: ANR_sphere intro: that) + ultimately show False by blast +qed + + +lemma Borsuk_maps_homotopic_in_connected_component_eq: + fixes a :: "'a :: euclidean_space" + assumes S: "compact S" "a \ S" "b \ S" and 2: "2 \ DIM('a)" + shows "(homotopic_with_canon (\x. True) S (sphere 0 1) + (\x. (x - a) /\<^sub>R norm (x - a)) + (\x. (x - b) /\<^sub>R norm (x - b)) \ + connected_component (- S) a b)" + (is "?lhs = ?rhs") +proof + assume L: ?lhs + show ?rhs + proof (cases "bounded(connected_component_set (- S) a)") + case True + show ?thesis + by (rule homotopic_Borsuk_maps_in_bounded_component [OF S True L]) + next + case not_bo_a: False + show ?thesis + proof (cases "bounded(connected_component_set (- S) b)") + case True + show ?thesis + using homotopic_Borsuk_maps_in_bounded_component [OF S] + by (simp add: L True assms connected_component_sym homotopic_Borsuk_maps_in_bounded_component homotopic_with_sym) + next + case False + then show ?thesis + using cobounded_unique_unbounded_component [of "-S" a b] \compact S\ not_bo_a + by (auto simp: compact_eq_bounded_closed assms connected_component_eq_eq) + qed + qed +next + assume R: ?rhs + then have "path_component (- S) a b" + using assms(1) compact_eq_bounded_closed open_Compl open_path_connected_component_set by fastforce + then show ?lhs + by (simp add: Borsuk_maps_homotopic_in_path_component) +qed + +subsection\More extension theorems\ + +lemma extension_from_clopen: + assumes ope: "openin (top_of_set S) T" + and clo: "closedin (top_of_set S) T" + and contf: "continuous_on T f" and fim: "f ` T \ U" and null: "U = {} \ S = {}" + obtains g where "continuous_on S g" "g ` S \ U" "\x. x \ T \ g x = f x" +proof (cases "U = {}") + case True + then show ?thesis + by (simp add: null that) +next + case False + then obtain a where "a \ U" + by auto + let ?g = "\x. if x \ T then f x else a" + have Seq: "S = T \ (S - T)" + using clo closedin_imp_subset by fastforce + show ?thesis + proof + have "continuous_on (T \ (S - T)) ?g" + apply (rule continuous_on_cases_local) + using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local) + with Seq show "continuous_on S ?g" + by metis + show "?g ` S \ U" + using \a \ U\ fim by auto + show "\x. x \ T \ ?g x = f x" + by auto + qed +qed + + +lemma extension_from_component: + fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" + assumes S: "locally connected S \ compact S" and "ANR U" + and C: "C \ components S" and contf: "continuous_on C f" and fim: "f ` C \ U" + obtains g where "continuous_on S g" "g ` S \ U" "\x. x \ C \ g x = f x" +proof - + obtain T g where ope: "openin (top_of_set S) T" + and clo: "closedin (top_of_set S) T" + and "C \ T" and contg: "continuous_on T g" and gim: "g ` T \ U" + and gf: "\x. x \ C \ g x = f x" + using S + proof + assume "locally connected S" + show ?thesis + by (metis C \locally connected S\ openin_components_locally_connected closedin_component contf fim order_refl that) + next + assume "compact S" + then obtain W g where "C \ W" and opeW: "openin (top_of_set S) W" + and contg: "continuous_on W g" + and gim: "g ` W \ U" and gf: "\x. x \ C \ g x = f x" + using ANR_imp_absolute_neighbourhood_extensor [of U C f S] C \ANR U\ closedin_component contf fim by blast + then obtain V where "open V" and V: "W = S \ V" + by (auto simp: openin_open) + moreover have "locally compact S" + by (simp add: \compact S\ closed_imp_locally_compact compact_imp_closed) + ultimately obtain K where opeK: "openin (top_of_set S) K" and "compact K" "C \ K" "K \ V" + by (metis C Int_subset_iff \C \ W\ \compact S\ compact_components Sura_Bura_clopen_subset) + show ?thesis + proof + show "closedin (top_of_set S) K" + by (meson \compact K\ \compact S\ closedin_compact_eq opeK openin_imp_subset) + show "continuous_on K g" + by (metis Int_subset_iff V \K \ V\ contg continuous_on_subset opeK openin_subtopology subset_eq) + show "g ` K \ U" + using V \K \ V\ gim opeK openin_imp_subset by fastforce + qed (use opeK gf \C \ K\ in auto) + qed + obtain h where "continuous_on S h" "h ` S \ U" "\x. x \ T \ h x = g x" + using extension_from_clopen + by (metis C bot.extremum_uniqueI clo contg gim fim image_is_empty in_components_nonempty ope) + then show ?thesis + by (metis \C \ T\ gf subset_eq that) +qed + + +lemma tube_lemma: + fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" + assumes "compact S" and S: "S \ {}" "(\x. (x,a)) ` S \ U" + and ope: "openin (top_of_set (S \ T)) U" + obtains V where "openin (top_of_set T) V" "a \ V" "S \ V \ U" +proof - + let ?W = "{y. \x. x \ S \ (x, y) \ (S \ T - U)}" + have "U \ S \ T" "closedin (top_of_set (S \ T)) (S \ T - U)" + using ope by (auto simp: openin_closedin_eq) + then have "closedin (top_of_set T) ?W" + using \compact S\ closedin_compact_projection by blast + moreover have "a \ T - ?W" + using \U \ S \ T\ S by auto + moreover have "S \ (T - ?W) \ U" + by auto + ultimately show ?thesis + by (metis (no_types, lifting) Sigma_cong closedin_def that topspace_euclidean_subtopology) +qed + +lemma tube_lemma_gen: + fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" + assumes "compact S" "S \ {}" "T \ T'" "S \ T \ U" + and ope: "openin (top_of_set (S \ T')) U" + obtains V where "openin (top_of_set T') V" "T \ V" "S \ V \ U" +proof - + have "\x. x \ T \ \V. openin (top_of_set T') V \ x \ V \ S \ V \ U" + using assms by (auto intro: tube_lemma [OF \compact S\]) + then obtain F where F: "\x. x \ T \ openin (top_of_set T') (F x) \ x \ F x \ S \ F x \ U" + by metis + show ?thesis + proof + show "openin (top_of_set T') (\(F ` T))" + using F by blast + show "T \ \(F ` T)" + using F by blast + show "S \ \(F ` T) \ U" + using F by auto + qed +qed + +proposition\<^marker>\tag unimportant\ homotopic_neighbourhood_extension: + fixes f :: "'a::euclidean_space \ 'b::euclidean_space" + assumes contf: "continuous_on S f" and fim: "f ` S \ U" + and contg: "continuous_on S g" and gim: "g ` S \ U" + and clo: "closedin (top_of_set S) T" + and "ANR U" and hom: "homotopic_with_canon (\x. True) T U f g" + obtains V where "T \ V" "openin (top_of_set S) V" + "homotopic_with_canon (\x. True) V U f g" +proof - + have "T \ S" + using clo closedin_imp_subset by blast + obtain h where conth: "continuous_on ({0..1::real} \ T) h" + and him: "h ` ({0..1} \ T) \ U" + and h0: "\x. h(0, x) = f x" and h1: "\x. h(1, x) = g x" + using hom by (auto simp: homotopic_with_def) + define h' where "h' \ \z. if fst z \ {0} then f(snd z) + else if fst z \ {1} then g(snd z) + else h z" + let ?S0 = "{0::real} \ S" and ?S1 = "{1::real} \ S" + have "continuous_on(?S0 \ (?S1 \ {0..1} \ T)) h'" + unfolding h'_def + proof (intro continuous_on_cases_local) + show "closedin (top_of_set (?S0 \ (?S1 \ {0..1} \ T))) ?S0" + "closedin (top_of_set (?S1 \ {0..1} \ T)) ?S1" + using \T \ S\ by (force intro: closedin_Times closedin_subset_trans [of "{0..1} \ S"])+ + show "closedin (top_of_set (?S0 \ (?S1 \ {0..1} \ T))) (?S1 \ {0..1} \ T)" + "closedin (top_of_set (?S1 \ {0..1} \ T)) ({0..1} \ T)" + using \T \ S\ by (force intro: clo closedin_Times closedin_subset_trans [of "{0..1} \ S"])+ + show "continuous_on (?S0) (\x. f (snd x))" + by (intro continuous_intros continuous_on_compose2 [OF contf]) auto + show "continuous_on (?S1) (\x. g (snd x))" + by (intro continuous_intros continuous_on_compose2 [OF contg]) auto + qed (use h0 h1 conth in auto) + then have "continuous_on ({0,1} \ S \ ({0..1} \ T)) h'" + by (metis Sigma_Un_distrib1 Un_assoc insert_is_Un) + moreover have "h' ` ({0,1} \ S \ {0..1} \ T) \ U" + using fim gim him \T \ S\ unfolding h'_def by force + moreover have "closedin (top_of_set ({0..1::real} \ S)) ({0,1} \ S \ {0..1::real} \ T)" + by (intro closedin_Times closedin_Un clo) (simp_all add: closed_subset) + ultimately + obtain W k where W: "({0,1} \ S) \ ({0..1} \ T) \ W" + and opeW: "openin (top_of_set ({0..1} \ S)) W" + and contk: "continuous_on W k" + and kim: "k ` W \ U" + and kh': "\x. x \ ({0,1} \ S) \ ({0..1} \ T) \ k x = h' x" + by (metis ANR_imp_absolute_neighbourhood_extensor [OF \ANR U\, of "({0,1} \ S) \ ({0..1} \ T)" h' "{0..1} \ S"]) + obtain T' where opeT': "openin (top_of_set S) T'" + and "T \ T'" and TW: "{0..1} \ T' \ W" + using tube_lemma_gen [of "{0..1::real}" T S W] W \T \ S\ opeW by auto + moreover have "homotopic_with_canon (\x. True) T' U f g" + proof (simp add: homotopic_with, intro exI conjI) + show "continuous_on ({0..1} \ T') k" + using TW continuous_on_subset contk by auto + show "k ` ({0..1} \ T') \ U" + using TW kim by fastforce + have "T' \ S" + by (meson opeT' subsetD openin_imp_subset) + then show "\x\T'. k (0, x) = f x" "\x\T'. k (1, x) = g x" + by (auto simp: kh' h'_def) + qed + ultimately show ?thesis + by (blast intro: that) +qed + +text\ Homotopy on a union of closed-open sets.\ +proposition\<^marker>\tag unimportant\ homotopic_on_clopen_Union: + fixes \ :: "'a::euclidean_space set set" + assumes "\S. S \ \ \ closedin (top_of_set (\\)) S" + and "\S. S \ \ \ openin (top_of_set (\\)) S" + and "\S. S \ \ \ homotopic_with_canon (\x. True) S T f g" + shows "homotopic_with_canon (\x. True) (\\) T f g" +proof - + obtain \ where "\ \ \" "countable \" and eqU: "\\ = \\" + using Lindelof_openin assms by blast + show ?thesis + proof (cases "\ = {}") + case True + then show ?thesis + by (metis Union_empty eqU homotopic_with_canon_on_empty) + next + case False + then obtain V :: "nat \ 'a set" where V: "range V = \" + using range_from_nat_into \countable \\ by metis + with \\ \ \\ have clo: "\n. closedin (top_of_set (\\)) (V n)" + and ope: "\n. openin (top_of_set (\\)) (V n)" + and hom: "\n. homotopic_with_canon (\x. True) (V n) T f g" + using assms by auto + then obtain h where conth: "\n. continuous_on ({0..1::real} \ V n) (h n)" + and him: "\n. h n ` ({0..1} \ V n) \ T" + and h0: "\n. \x. x \ V n \ h n (0, x) = f x" + and h1: "\n. \x. x \ V n \ h n (1, x) = g x" + by (simp add: homotopic_with) metis + have wop: "b \ V x \ \k. b \ V k \ (\j V j)" for b x + using nat_less_induct [where P = "\i. b \ V i"] by meson + obtain \ where cont: "continuous_on ({0..1} \ \(V ` UNIV)) \" + and eq: "\x i. \x \ {0..1} \ \(V ` UNIV) \ + {0..1} \ (V i - (\m \ \ x = h i x" + proof (rule pasting_lemma_exists) + let ?X = "top_of_set ({0..1::real} \ \(range V))" + show "topspace ?X \ (\i. {0..1::real} \ (V i - (\m \(V ` UNIV))) + ({0..1::real} \ (V i - (\m(V ` UNIV))) (V i)" + using ope V eqU by auto + show "closedin (top_of_set (\(V ` UNIV))) (\m (V i - \ (V ` {..i j x. x \ topspace ?X \ {0..1} \ (V i - (\m {0..1} \ (V j - (\m h i x = h j x" + by clarsimp (metis lessThan_iff linorder_neqE_nat) + qed auto + show ?thesis + proof (simp add: homotopic_with eqU [symmetric], intro exI conjI ballI) + show "continuous_on ({0..1} \ \\) \" + using V eqU by (blast intro!: continuous_on_subset [OF cont]) + show "\` ({0..1} \ \\) \ T" + proof clarsimp + fix t :: real and y :: "'a" and X :: "'a set" + assume "y \ X" "X \ \" and t: "0 \ t" "t \ 1" + then obtain k where "y \ V k" and j: "\j V j" + by (metis image_iff V wop) + with him t show "\(t, y) \ T" + by (subst eq) force+ + qed + fix X y + assume "X \ \" "y \ X" + then obtain k where "y \ V k" and j: "\j V j" + by (metis image_iff V wop) + then show "\(0, y) = f y" and "\(1, y) = g y" + by (subst eq [where i=k]; force simp: h0 h1)+ + qed + qed +qed + +lemma homotopic_on_components_eq: + fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set" + assumes S: "locally connected S \ compact S" and "ANR T" + shows "homotopic_with_canon (\x. True) S T f g \ + (continuous_on S f \ f ` S \ T \ continuous_on S g \ g ` S \ T) \ + (\C \ components S. homotopic_with_canon (\x. True) C T f g)" + (is "?lhs \ ?C \ ?rhs") +proof - + have "continuous_on S f" "f ` S \ T" "continuous_on S g" "g ` S \ T" if ?lhs + using homotopic_with_imp_continuous homotopic_with_imp_subset1 homotopic_with_imp_subset2 that by blast+ + moreover have "?lhs \ ?rhs" + if contf: "continuous_on S f" and fim: "f ` S \ T" and contg: "continuous_on S g" and gim: "g ` S \ T" + proof + assume ?lhs + with that show ?rhs + by (simp add: homotopic_with_subset_left in_components_subset) + next + assume R: ?rhs + have "\U. C \ U \ closedin (top_of_set S) U \ + openin (top_of_set S) U \ + homotopic_with_canon (\x. True) U T f g" if C: "C \ components S" for C + proof - + have "C \ S" + by (simp add: in_components_subset that) + show ?thesis + using S + proof + assume "locally connected S" + show ?thesis + proof (intro exI conjI) + show "closedin (top_of_set S) C" + by (simp add: closedin_component that) + show "openin (top_of_set S) C" + by (simp add: \locally connected S\ openin_components_locally_connected that) + show "homotopic_with_canon (\x. True) C T f g" + by (simp add: R that) + qed auto + next + assume "compact S" + have hom: "homotopic_with_canon (\x. True) C T f g" + using R that by blast + obtain U where "C \ U" and opeU: "openin (top_of_set S) U" + and hom: "homotopic_with_canon (\x. True) U T f g" + using homotopic_neighbourhood_extension [OF contf fim contg gim _ \ANR T\ hom] + \C \ components S\ closedin_component by blast + then obtain V where "open V" and V: "U = S \ V" + by (auto simp: openin_open) + moreover have "locally compact S" + by (simp add: \compact S\ closed_imp_locally_compact compact_imp_closed) + ultimately obtain K where opeK: "openin (top_of_set S) K" and "compact K" "C \ K" "K \ V" + by (metis C Int_subset_iff Sura_Bura_clopen_subset \C \ U\ \compact S\ compact_components) + show ?thesis + proof (intro exI conjI) + show "closedin (top_of_set S) K" + by (meson \compact K\ \compact S\ closedin_compact_eq opeK openin_imp_subset) + show "homotopic_with_canon (\x. True) K T f g" + using V \K \ V\ hom homotopic_with_subset_left opeK openin_imp_subset by fastforce + qed (use opeK \C \ K\ in auto) + qed + qed + then obtain \ where \: "\C. C \ components S \ C \ \ C" + and clo\: "\C. C \ components S \ closedin (top_of_set S) (\ C)" + and ope\: "\C. C \ components S \ openin (top_of_set S) (\ C)" + and hom\: "\C. C \ components S \ homotopic_with_canon (\x. True) (\ C) T f g" + by metis + have Seq: "S = \ (\ ` components S)" + proof + show "S \ \ (\ ` components S)" + by (metis Sup_mono Union_components \ imageI) + show "\ (\ ` components S) \ S" + using ope\ openin_imp_subset by fastforce + qed + show ?lhs + apply (subst Seq) + apply (rule homotopic_on_clopen_Union) + using Seq clo\ ope\ hom\ by auto + qed + ultimately show ?thesis by blast +qed + + +lemma cohomotopically_trivial_on_components: + fixes S :: "'a :: euclidean_space set" and T :: "'b :: euclidean_space set" + assumes S: "locally connected S \ compact S" and "ANR T" + shows + "(\f g. continuous_on S f \ f ` S \ T \ continuous_on S g \ g ` S \ T \ + homotopic_with_canon (\x. True) S T f g) + \ + (\C\components S. + \f g. continuous_on C f \ f ` C \ T \ continuous_on C g \ g ` C \ T \ + homotopic_with_canon (\x. True) C T f g)" + (is "?lhs = ?rhs") +proof + assume L[rule_format]: ?lhs + show ?rhs + proof clarify + fix C f g + assume contf: "continuous_on C f" and fim: "f ` C \ T" + and contg: "continuous_on C g" and gim: "g ` C \ T" and C: "C \ components S" + obtain f' where contf': "continuous_on S f'" and f'im: "f' ` S \ T" and f'f: "\x. x \ C \ f' x = f x" + using extension_from_component [OF S \ANR T\ C contf fim] by metis + obtain g' where contg': "continuous_on S g'" and g'im: "g' ` S \ T" and g'g: "\x. x \ C \ g' x = g x" + using extension_from_component [OF S \ANR T\ C contg gim] by metis + have "homotopic_with_canon (\x. True) C T f' g'" + using L [OF contf' f'im contg' g'im] homotopic_with_subset_left C in_components_subset by fastforce + then show "homotopic_with_canon (\x. True) C T f g" + using f'f g'g homotopic_with_eq by force + qed +next + assume R [rule_format]: ?rhs + show ?lhs + proof clarify + fix f g + assume contf: "continuous_on S f" and fim: "f ` S \ T" + and contg: "continuous_on S g" and gim: "g ` S \ T" + moreover have "homotopic_with_canon (\x. True) C T f g" if "C \ components S" for C + using R [OF that] + by (meson contf contg continuous_on_subset fim gim image_mono in_components_subset order.trans that) + ultimately show "homotopic_with_canon (\x. True) S T f g" + by (subst homotopic_on_components_eq [OF S \ANR T\]) auto + qed +qed + +subsection\The complement of a set and path-connectedness\ + +text\Complement in dimension N > 1 of set homeomorphic to any interval in + any dimension is (path-)connected. This naively generalizes the argument + in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer fixed point theorem", +American Mathematical Monthly 1984.\ + +lemma unbounded_components_complement_absolute_retract: + fixes S :: "'a::euclidean_space set" + assumes C: "C \ components(- S)" and S: "compact S" "AR S" + shows "\ bounded C" +proof - + obtain y where y: "C = connected_component_set (- S) y" and "y \ S" + using C by (auto simp: components_def) + have "open(- S)" + using S by (simp add: closed_open compact_eq_bounded_closed) + have "S retract_of UNIV" + using S compact_AR by blast + then obtain r where contr: "continuous_on UNIV r" and ontor: "range r \ S" + and r: "\x. x \ S \ r x = x" + by (auto simp: retract_of_def retraction_def) + show ?thesis + proof + assume "bounded C" + have "connected_component_set (- S) y \ S" + proof (rule frontier_subset_retraction) + show "bounded (connected_component_set (- S) y)" + using \bounded C\ y by blast + show "frontier (connected_component_set (- S) y) \ S" + using C \compact S\ compact_eq_bounded_closed frontier_of_components_closed_complement y by blast + show "continuous_on (closure (connected_component_set (- S) y)) r" + by (blast intro: continuous_on_subset [OF contr]) + qed (use ontor r in auto) + with \y \ S\ show False by force + qed +qed + +lemma connected_complement_absolute_retract: + fixes S :: "'a::euclidean_space set" + assumes S: "compact S" "AR S" and 2: "2 \ DIM('a)" + shows "connected(- S)" +proof - + have "S retract_of UNIV" + using S compact_AR by blast + show ?thesis + apply (clarsimp simp: connected_iff_connected_component_eq) + apply (rule cobounded_unique_unbounded_component [OF _ 2]) + apply (simp add: \compact S\ compact_imp_bounded) + apply (meson ComplI S componentsI unbounded_components_complement_absolute_retract)+ + done +qed + +lemma path_connected_complement_absolute_retract: + fixes S :: "'a::euclidean_space set" + assumes "compact S" "AR S" "2 \ DIM('a)" + shows "path_connected(- S)" + using connected_complement_absolute_retract [OF assms] + using \compact S\ compact_eq_bounded_closed connected_open_path_connected by blast + +theorem connected_complement_homeomorphic_convex_compact: + fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" + assumes hom: "S homeomorphic T" and T: "convex T" "compact T" and 2: "2 \ DIM('a)" + shows "connected(- S)" +proof (cases "S = {}") + case True + then show ?thesis + by (simp add: connected_UNIV) +next + case False + show ?thesis + proof (rule connected_complement_absolute_retract) + show "compact S" + using \compact T\ hom homeomorphic_compactness by auto + show "AR S" + by (meson AR_ANR False \convex T\ convex_imp_ANR convex_imp_contractible hom homeomorphic_ANR_iff_ANR homeomorphic_contractible_eq) + qed (rule 2) +qed + +corollary path_connected_complement_homeomorphic_convex_compact: + fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set" + assumes hom: "S homeomorphic T" "convex T" "compact T" "2 \ DIM('a)" + shows "path_connected(- S)" + using connected_complement_homeomorphic_convex_compact [OF assms] + using \compact T\ compact_eq_bounded_closed connected_open_path_connected hom homeomorphic_compactness by blast + +lemma path_connected_complement_homeomorphic_interval: + fixes S :: "'a::euclidean_space set" + assumes "S homeomorphic cbox a b" "2 \ DIM('a)" + shows "path_connected(-S)" + using assms compact_cbox convex_box(1) path_connected_complement_homeomorphic_convex_compact by blast + +lemma connected_complement_homeomorphic_interval: + fixes S :: "'a::euclidean_space set" + assumes "S homeomorphic cbox a b" "2 \ DIM('a)" + shows "connected(-S)" + using assms path_connected_complement_homeomorphic_interval path_connected_imp_connected by blast + +end