Theory Retracts

section ‹Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts›

theory Retracts
imports
  Brouwer_Fixpoint
  Continuous_Extension
begin

text ‹Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
retracts (ENR). We define AR and ANR by specializing the standard definitions for a set to embedding
in spaces of higher dimension.

John Harrison writes: "This turns out to be sufficient (since any set in ‹ℝ⇧n› can be
embedded as a closed subset of a convex subset of ‹ℝ⇧n⇧+⇧1›) to derive the usual
definitions, but we need to split them into two implications because of the lack of type
quantifiers. Then ENR turns out to be equivalent to ANR plus local compactness."›

definition✐‹tag important› AR :: "'a::topological_space set ⇒ bool" where
"AR S ≡ ∀U. ∀S'::('a * real) set.
  S homeomorphic S' ∧ closedin (top_of_set U) S' ⟶ S' retract_of U"

definition✐‹tag important› ANR :: "'a::topological_space set ⇒ bool" where
"ANR S ≡ ∀U. ∀S'::('a * real) set.
  S homeomorphic S' ∧ closedin (top_of_set U) S'
  ⟶ (∃T. openin (top_of_set U) T ∧ S' retract_of T)"

definition✐‹tag important› ENR :: "'a::topological_space set ⇒ bool" where
"ENR S ≡ ∃U. open U ∧ S retract_of U"

text ‹First, show that we do indeed get the "usual" properties of ARs and ANRs.›

lemma AR_imp_absolute_extensor:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "AR S" and contf: "continuous_on T f" and "f ` T ⊆ S"
      and cloUT: "closedin (top_of_set U) T"
  obtains g where "continuous_on U g" "g ` U ⊆ S" "⋀x. x ∈ T ⟹ g x = f x"
proof -
  have "aff_dim S < int (DIM('b × real))"
    using aff_dim_le_DIM [of S] by simp
  then obtain C and S' :: "('b * real) set"
          where C: "convex C" "C ≠ {}"
            and cloCS: "closedin (top_of_set C) S'"
            and hom: "S homeomorphic S'"
    by (metis that homeomorphic_closedin_convex)
  then have "S' retract_of C"
    using ‹AR S› by (simp add: AR_def)
  then obtain r where "S' ⊆ C" and contr: "continuous_on C r"
                  and "r ` C ⊆ S'" and rid: "⋀x. x∈S' ⟹ r x = x"
    by (auto simp: retraction_def retract_of_def)
  obtain g h where "homeomorphism S S' g h"
    using hom by (force simp: homeomorphic_def)
  then have "continuous_on (f ` T) g"
    by (meson ‹f ` T ⊆ S› continuous_on_subset homeomorphism_def)
  then have contgf: "continuous_on T (g ∘ f)"
    by (metis continuous_on_compose contf)
  have gfTC: "(g ∘ f) ` T ⊆ C"
  proof -
    have "g ` S = S'"
      by (metis (no_types) ‹homeomorphism S S' g h› homeomorphism_def)
    with ‹S' ⊆ C› ‹f ` T ⊆ S› show ?thesis by force
  qed
  obtain f' where f': "continuous_on U f'"  "f' ` U ⊆ C"
                      "⋀x. x ∈ T ⟹ f' x = (g ∘ f) x"
    by (metis Dugundji [OF C cloUT contgf gfTC])
  show ?thesis
  proof (rule_tac g = "h ∘ r ∘ f'" in that)
    show "continuous_on U (h ∘ r ∘ f')"
    proof (intro continuous_on_compose f')
      show "continuous_on (f' ` U) r"
        using continuous_on_subset contr f' by blast
      show "continuous_on (r ` f' ` U) h"
        using ‹homeomorphism S S' g h› ‹f' ` U ⊆ C› 
        unfolding homeomorphism_def
        by (metis ‹r ` C ⊆ S'› continuous_on_subset image_mono)
    qed
    show "(h ∘ r ∘ f') ` U ⊆ S"
      using ‹homeomorphism S S' g h› ‹r ` C ⊆ S'› ‹f' ` U ⊆ C›
      by (fastforce simp: homeomorphism_def)
    show "⋀x. x ∈ T ⟹ (h ∘ r ∘ f') x = f x"
      using ‹homeomorphism S S' g h› ‹f ` T ⊆ S› f'
      by (auto simp: rid homeomorphism_def)
  qed
qed

lemma AR_imp_absolute_retract:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "AR S" "S homeomorphic S'"
      and clo: "closedin (top_of_set U) S'"
    shows "S' retract_of U"
proof -
  obtain g h where hom: "homeomorphism S S' g h"
    using assms by (force simp: homeomorphic_def)
  obtain h: "continuous_on S' h" " h ` S' ⊆ S"
    using hom homeomorphism_def by blast
  obtain h' where h': "continuous_on U h'" "h' ` U ⊆ S"
              and h'h: "⋀x. x ∈ S' ⟹ h' x = h x"
    by (blast intro: AR_imp_absolute_extensor [OF ‹AR S› h clo])
  have [simp]: "S' ⊆ U" using clo closedin_limpt by blast
  show ?thesis
  proof (simp add: retraction_def retract_of_def, intro exI conjI)
    show "continuous_on U (g ∘ h')"
      by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
    show "(g ∘ h') ∈ U → S'"
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
    show "∀x∈S'. (g ∘ h') x = x"
      by clarsimp (metis h'h hom homeomorphism_def)
  qed
qed

lemma AR_imp_absolute_retract_UNIV:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "AR S" "S homeomorphic S'" "closed S'"
    shows "S' retract_of UNIV"
  using AR_imp_absolute_retract assms by fastforce

lemma absolute_extensor_imp_AR:
  fixes S :: "'a::euclidean_space set"
  assumes "⋀f :: 'a * real ⇒ 'a.
           ⋀U T. ⟦continuous_on T f;  f ` T ⊆ S;
                  closedin (top_of_set U) T⟧
                 ⟹ ∃g. continuous_on U g ∧ g ` U ⊆ S ∧ (∀x ∈ T. g x = f x)"
  shows "AR S"
proof (clarsimp simp: AR_def)
  fix U and T :: "('a * real) set"
  assume "S homeomorphic T" and clo: "closedin (top_of_set U) T"
  then obtain g h where hom: "homeomorphism S T g h"
    by (force simp: homeomorphic_def)
  obtain h: "continuous_on T h" " h ` T ⊆ S"
    using hom homeomorphism_def by blast
  obtain h' where h': "continuous_on U h'" "h' ` U ⊆ S"
              and h'h: "∀x∈T. h' x = h x"
    using assms [OF h clo] by blast
  have [simp]: "T ⊆ U"
    using clo closedin_imp_subset by auto
  show "T retract_of U"
  proof (simp add: retraction_def retract_of_def, intro exI conjI)
    show "continuous_on U (g ∘ h')"
      by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_cont1)
    show "(g ∘ h') ∈ U → T"
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
    show "∀x∈T. (g ∘ h') x = x"
      by clarsimp (metis h'h hom homeomorphism_def)
  qed
qed

lemma AR_eq_absolute_extensor:
  fixes S :: "'a::euclidean_space set"
  shows "AR S ⟷
       (∀f :: 'a * real ⇒ 'a.
        ∀U T. continuous_on T f ⟶ f ` T ⊆ S ⟶
               closedin (top_of_set U) T ⟶
                (∃g. continuous_on U g ∧ g ` U ⊆ S ∧ (∀x ∈ T. g x = f x)))"
  by (metis (mono_tags, opaque_lifting) AR_imp_absolute_extensor absolute_extensor_imp_AR)

lemma AR_imp_retract:
  fixes S :: "'a::euclidean_space set"
  assumes "AR S ∧ closedin (top_of_set U) S"
    shows "S retract_of U"
using AR_imp_absolute_retract assms homeomorphic_refl by blast

lemma AR_homeomorphic_AR:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "AR T" "S homeomorphic T"
    shows "AR S"
unfolding AR_def
by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym)

lemma homeomorphic_AR_iff_AR:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  shows "S homeomorphic T ⟹ AR S ⟷ AR T"
by (metis AR_homeomorphic_AR homeomorphic_sym)


lemma ANR_imp_absolute_neighbourhood_extensor:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "ANR S" and contf: "continuous_on T f" and "f ∈ T → S"
      and cloUT: "closedin (top_of_set U) T"
  obtains V g where "T ⊆ V" "openin (top_of_set U) V"
                    "continuous_on V g"
                    "g ∈ V → S" "⋀x. x ∈ T ⟹ g x = f x"
proof -
  have "aff_dim S < int (DIM('b × real))"
    using aff_dim_le_DIM [of S] by simp
  then obtain C and S' :: "('b * real) set"
          where C: "convex C" "C ≠ {}"
            and cloCS: "closedin (top_of_set C) S'"
            and hom: "S homeomorphic S'"
    by (metis that homeomorphic_closedin_convex)
  then obtain D where opD: "openin (top_of_set C) D" and "S' retract_of D"
    using ‹ANR S› by (auto simp: ANR_def)
  then obtain r where "S' ⊆ D" and contr: "continuous_on D r"
                  and "r ` D ⊆ S'" and rid: "⋀x. x ∈ S' ⟹ r x = x"
    by (auto simp: retraction_def retract_of_def)
  obtain g h where homgh: "homeomorphism S S' g h"
    using hom by (force simp: homeomorphic_def)
  have "continuous_on (f ` T) g"
    by (metis PiE assms(3) continuous_on_subset homeomorphism_cont1 homgh image_subset_iff)
  then have contgf: "continuous_on T (g ∘ f)"
    by (intro continuous_on_compose contf)
  have gfTC: "(g ∘ f) ` T ⊆ C"
  proof -
    have "g ` S = S'"
      by (metis (no_types) homeomorphism_def homgh)
    then show ?thesis
      by (metis PiE assms(3) cloCS closedin_def image_comp image_mono image_subset_iff order.trans topspace_euclidean_subtopology)
  qed
  obtain f' where contf': "continuous_on U f'"
              and "f' ` U ⊆ C"
              and eq: "⋀x. x ∈ T ⟹ f' x = (g ∘ f) x"
    by (metis Dugundji [OF C cloUT contgf gfTC])
  show ?thesis
  proof (rule_tac V = "U ∩ f' -` D" and g = "h ∘ r ∘ f'" in that)
    show "T ⊆ U ∩ f' -` D"
      using cloUT closedin_imp_subset ‹S' ⊆ D› ‹f ∈ T → S› eq homeomorphism_image1 homgh
      by fastforce
    show ope: "openin (top_of_set U) (U ∩ f' -` D)"
      by (meson ‹f' ` U ⊆ C› contf' continuous_openin_preimage image_subset_iff_funcset opD)
    have conth: "continuous_on (r ` f' ` (U ∩ f' -` D)) h"
    proof (rule continuous_on_subset [of S'])
      show "continuous_on S' h"
        using homeomorphism_def homgh by blast
    qed (use ‹r ` D ⊆ S'› in blast)
    show "continuous_on (U ∩ f' -` D) (h ∘ r ∘ f')"
      by (blast intro: continuous_on_compose conth continuous_on_subset [OF contr] continuous_on_subset [OF contf'])
    show "(h ∘ r ∘ f') ∈ (U ∩ f' -` D) → S"
      using ‹homeomorphism S S' g h›  ‹f' ` U ⊆ C›  ‹r ` D ⊆ S'›
      by (auto simp: homeomorphism_def)
    show "⋀x. x ∈ T ⟹ (h ∘ r ∘ f') x = f x"
      using ‹homeomorphism S S' g h› ‹f ∈ T → S› eq
      by (metis PiE comp_apply homeomorphism_def image_iff rid)
  qed
qed


corollary ANR_imp_absolute_neighbourhood_retract:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "ANR S" "S homeomorphic S'"
      and clo: "closedin (top_of_set U) S'"
  obtains V where "openin (top_of_set U) V" "S' retract_of V"
proof -
  obtain g h where hom: "homeomorphism S S' g h"
    using assms by (force simp: homeomorphic_def)
  obtain h: "continuous_on S' h" " h ∈ S' → S"
    using hom homeomorphism_def by blast
    from ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› h clo]
  obtain V h' where "S' ⊆ V" and opUV: "openin (top_of_set U) V"
                and h': "continuous_on V h'" "h' ` V ⊆ S"
                and h'h:"⋀x. x ∈ S' ⟹ h' x = h x"
    by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› h clo])
  have "S' retract_of V"
  proof (simp add: retraction_def retract_of_def, intro exI conjI ‹S' ⊆ V›)
    show "continuous_on V (g ∘ h')"
      by (meson continuous_on_compose continuous_on_subset h'(1) h'(2) hom homeomorphism_cont1)
    show "(g ∘ h') ∈ V → S'"
      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
    show "∀x∈S'. (g ∘ h') x = x"
      by clarsimp (metis h'h hom homeomorphism_def)
  qed
  then show ?thesis
    by (rule that [OF opUV])
qed

corollary ANR_imp_absolute_neighbourhood_retract_UNIV:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'"
  obtains V where "open V" "S' retract_of V"
  using ANR_imp_absolute_neighbourhood_retract [OF ‹ANR S› hom]
by (metis clo closed_closedin open_openin subtopology_UNIV)

corollary neighbourhood_extension_into_ANR:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes contf: "continuous_on S f" and fim: "f ∈ S → T" and "ANR T" "closed S"
  obtains V g where "S ⊆ V" "open V" "continuous_on V g"
                    "g ∈ V → T" "⋀x. x ∈ S ⟹ g x = f x"
  using ANR_imp_absolute_neighbourhood_extensor [OF  ‹ANR T› contf fim]
  by (metis ‹closed S› closed_closedin open_openin subtopology_UNIV)

lemma absolute_neighbourhood_extensor_imp_ANR:
  fixes S :: "'a::euclidean_space set"
  assumes "⋀f :: 'a * real ⇒ 'a.
           ⋀U T. ⟦continuous_on T f;  f ∈ T → S;
                  closedin (top_of_set U) T⟧
                 ⟹ ∃V g. T ⊆ V ∧ openin (top_of_set U) V ∧
                       continuous_on V g ∧ g ∈ V → S ∧ (∀x ∈ T. g x = f x)"
  shows "ANR S"
proof (clarsimp simp: ANR_def)
  fix U and T :: "('a * real) set"
  assume "S homeomorphic T" and clo: "closedin (top_of_set U) T"
  then obtain g h where hom: "homeomorphism S T g h"
    by (force simp: homeomorphic_def)
  obtain h: "continuous_on T h" " h ∈ T → S"
    using hom homeomorphism_def by blast
  obtain V h' where "T ⊆ V" and opV: "openin (top_of_set U) V"
                and h': "continuous_on V h'" "h' ∈ V → S"
              and h'h: "∀x∈T. h' x = h x"
    using assms [OF h clo] by blast
  have [simp]: "T ⊆ U"
    using clo closedin_imp_subset by auto
  have "T retract_of V"
  proof (simp add: retraction_def retract_of_def, intro exI conjI ‹T ⊆ V›)
    show "continuous_on V (g ∘ h')"
      by (meson continuous_on_compose continuous_on_subset h' hom homeomorphism_def image_subset_iff_funcset)
    show "(g ∘ h') ∈ V → T"
      using h' hom homeomorphism_image1 by fastforce
    show "∀x∈T. (g ∘ h') x = x"
      by clarsimp (metis h'h hom homeomorphism_def)
  qed
  then show "∃V. openin (top_of_set U) V ∧ T retract_of V"
    using opV by blast
qed

lemma ANR_eq_absolute_neighbourhood_extensor:
  fixes S :: "'a::euclidean_space set"
  shows "ANR S ⟷
         (∀f :: 'a * real ⇒ 'a.
          ∀U T. continuous_on T f ⟶ f ∈ T → S ⟶
                closedin (top_of_set U) T ⟶
               (∃V g. T ⊆ V ∧ openin (top_of_set U) V ∧
                       continuous_on V g ∧ g ∈ V → S ∧ (∀x ∈ T. g x = f x)))" (is "_ = ?rhs")
proof
  assume "ANR S" then show ?rhs
    by (metis ANR_imp_absolute_neighbourhood_extensor)
qed (simp add: absolute_neighbourhood_extensor_imp_ANR)

lemma ANR_imp_neighbourhood_retract:
  fixes S :: "'a::euclidean_space set"
  assumes "ANR S" "closedin (top_of_set U) S"
  obtains V where "openin (top_of_set U) V" "S retract_of V"
using ANR_imp_absolute_neighbourhood_retract assms homeomorphic_refl by blast

lemma ANR_imp_absolute_closed_neighbourhood_retract:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "ANR S" "S homeomorphic S'" and US': "closedin (top_of_set U) S'"
  obtains V W
    where "openin (top_of_set U) V"
          "closedin (top_of_set U) W"
          "S' ⊆ V" "V ⊆ W" "S' retract_of W"
proof -
  obtain Z where "openin (top_of_set U) Z" and S'Z: "S' retract_of Z"
    by (blast intro: assms ANR_imp_absolute_neighbourhood_retract)
  then have UUZ: "closedin (top_of_set U) (U - Z)"
    by auto
  have "S' ∩ (U - Z) = {}"
    using ‹S' retract_of Z› closedin_retract closedin_subtopology by fastforce
  then obtain V W
      where "openin (top_of_set U) V"
        and "openin (top_of_set U) W"
        and "S' ⊆ V" "U - Z ⊆ W" "V ∩ W = {}"
      using separation_normal_local [OF US' UUZ]  by auto
  moreover have "S' retract_of U - W"
  proof (rule retract_of_subset [OF S'Z])
    show "S' ⊆ U - W"
      using US' ‹S' ⊆ V› ‹V ∩ W = {}› closedin_subset by fastforce
    show "U - W ⊆ Z"
      using Diff_subset_conv ‹U - Z ⊆ W› by blast
  qed
  ultimately show ?thesis
    by (metis Diff_subset_conv Diff_triv Int_Diff_Un Int_absorb1 openin_closedin_eq that topspace_euclidean_subtopology)
qed

lemma ANR_imp_closed_neighbourhood_retract:
  fixes S :: "'a::euclidean_space set"
  assumes "ANR S" "closedin (top_of_set U) S"
  obtains V W where "openin (top_of_set U) V"
                    "closedin (top_of_set U) W"
                    "S ⊆ V" "V ⊆ W" "S retract_of W"
by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl)

lemma ANR_homeomorphic_ANR:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "ANR T" "S homeomorphic T"
    shows "ANR S"
unfolding ANR_def
by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym)

lemma homeomorphic_ANR_iff_ANR:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  shows "S homeomorphic T ⟹ ANR S ⟷ ANR T"
by (metis ANR_homeomorphic_ANR homeomorphic_sym)

subsection ‹Analogous properties of ENRs›

lemma ENR_imp_absolute_neighbourhood_retract:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "ENR S" and hom: "S homeomorphic S'"
      and "S' ⊆ U"
  obtains V where "openin (top_of_set U) V" "S' retract_of V"
proof -
  obtain X where "open X" "S retract_of X"
    using ‹ENR S› by (auto simp: ENR_def)
  then obtain r where "retraction X S r"
    by (auto simp: retract_of_def)
  have "locally compact S'"
    using retract_of_locally_compact open_imp_locally_compact
          homeomorphic_local_compactness ‹S retract_of X› ‹open X› hom by blast
  then obtain W where UW: "openin (top_of_set U) W"
                  and WS': "closedin (top_of_set W) S'"
    apply (rule locally_compact_closedin_open)
    by (meson Int_lower2 assms(3) closedin_imp_subset closedin_subset_trans le_inf_iff openin_open)
  obtain f g where hom: "homeomorphism S S' f g"
    using assms by (force simp: homeomorphic_def)
  have contg: "continuous_on S' g"
    using hom homeomorphism_def by blast
  moreover have "g ` S' ⊆ S" by (metis hom equalityE homeomorphism_def)
  ultimately obtain h where conth: "continuous_on W h" and hg: "⋀x. x ∈ S' ⟹ h x = g x"
    using Tietze_unbounded [of S' g W] WS' by blast
  have "W ⊆ U" using UW openin_open by auto
  have "S' ⊆ W" using WS' closedin_closed by auto
  have him: "⋀x. x ∈ S' ⟹ h x ∈ X"
    by (metis (no_types) ‹S retract_of X› hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
  have "S' retract_of (W ∩ h -` X)"
  proof (simp add: retraction_def retract_of_def, intro exI conjI)
    show "S' ⊆ W" "S' ⊆ h -` X"
      using him WS' closedin_imp_subset by blast+
    show "continuous_on (W ∩ h -` X) (f ∘ r ∘ h)"
    proof (intro continuous_on_compose)
      show "continuous_on (W ∩ h -` X) h"
        by (meson conth continuous_on_subset inf_le1)
      show "continuous_on (h ` (W ∩ h -` X)) r"
      proof -
        have "h ` (W ∩ h -` X) ⊆ X"
          by blast
        then show "continuous_on (h ` (W ∩ h -` X)) r"
          by (meson ‹retraction X S r› continuous_on_subset retraction)
      qed
      show "continuous_on (r ` h ` (W ∩ h -` X)) f"
      proof (rule continuous_on_subset [of S])
        show "continuous_on S f"
          using hom homeomorphism_def by blast
        show "r ` h ` (W ∩ h -` X) ⊆ S"
          by (metis ‹retraction X S r› image_mono image_subset_iff_subset_vimage inf_le2 retraction)
      qed
    qed
    show "(f ∘ r ∘ h) ∈ (W ∩ h -` X) → S'"
      using ‹retraction X S r› hom
      by (auto simp: retraction_def homeomorphism_def)
    show "∀x∈S'. (f ∘ r ∘ h) x = x"
      using ‹retraction X S r› hom by (auto simp: retraction_def homeomorphism_def hg)
  qed
  then show ?thesis
    using UW ‹open X› conth continuous_openin_preimage_eq openin_trans that by blast
qed

corollary ENR_imp_absolute_neighbourhood_retract_UNIV:
  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
  assumes "ENR S" "S homeomorphic S'"
  obtains T' where "open T'" "S' retract_of T'"
by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV)

lemma ENR_homeomorphic_ENR:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "ENR T" "S homeomorphic T"
    shows "ENR S"
unfolding ENR_def
by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym)

lemma homeomorphic_ENR_iff_ENR:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "S homeomorphic T"
    shows "ENR S ⟷ ENR T"
by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)

lemma ENR_translation:
  fixes S :: "'a::euclidean_space set"
  shows "ENR(image (λx. a + x) S) ⟷ ENR S"
by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)

lemma ENR_linear_image_eq:
  fixes f :: "'a::euclidean_space ⇒ 'b::euclidean_space"
  assumes "linear f" "inj f"
  shows "ENR (image f S) ⟷ ENR S"
  by (meson assms homeomorphic_ENR_iff_ENR linear_homeomorphic_image)

text ‹Some relations among the concepts. We also relate AR to being a retract of UNIV, which is
often a more convenient proxy in the closed case.›

lemma AR_imp_ANR: "AR S ⟹ ANR S"
  using ANR_def AR_def by fastforce

lemma ENR_imp_ANR:
  fixes S :: "'a::euclidean_space set"
  shows "ENR S ⟹ ANR S"
  by (meson ANR_def ENR_imp_absolute_neighbourhood_retract closedin_imp_subset)

lemma ENR_ANR:
  fixes S :: "'a::euclidean_space set"
  shows "ENR S ⟷ ANR S ∧ locally compact S"
proof
  assume "ENR S"
  then have "locally compact S"
    using ENR_def open_imp_locally_compact retract_of_locally_compact by auto
  then show "ANR S ∧ locally compact S"
    using ENR_imp_ANR ‹ENR S› by blast
next
  assume "ANR S ∧ locally compact S"
  then have "ANR S" "locally compact S" by auto
  then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T"
    using locally_compact_homeomorphic_closed
    by (metis DIM_prod DIM_real Suc_eq_plus1 lessI)
  then show "ENR S"
    using ‹ANR S›
    by (meson ANR_imp_absolute_neighbourhood_retract_UNIV ENR_def ENR_homeomorphic_ENR)
qed


lemma AR_ANR:
  fixes S :: "'a::euclidean_space set"
  shows "AR S ⟷ ANR S ∧ contractible S ∧ S ≠ {}"
        (is "?lhs = ?rhs")
proof
  assume ?lhs
  have "aff_dim S < int DIM('a × real)"
      using aff_dim_le_DIM [of S] by auto
    then obtain C and S' :: "('a * real) set"
    where "convex C" "C ≠ {}" "closedin (top_of_set C) S'" "S homeomorphic S'"
    using homeomorphic_closedin_convex by blast
  with ‹AR S› have "contractible S"
    by (meson AR_def convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible)
  with ‹AR S› show ?rhs
    using AR_imp_ANR AR_imp_retract by fastforce
next
  assume ?rhs
  then obtain a and h:: "real × 'a ⇒ 'a"
      where conth: "continuous_on ({0..1} × S) h"
        and hS: "h ` ({0..1} × S) ⊆ S"
        and [simp]: "⋀x. h(0, x) = x"
        and [simp]: "⋀x. h(1, x) = a"
        and "ANR S" "S ≠ {}"
    by (auto simp: contractible_def homotopic_with_def)
  then have "a ∈ S"
    by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
  have "∃g. continuous_on W g ∧ g ∈ W → S ∧ (∀x∈T. g x = f x)"
         if      f: "continuous_on T f" "f ∈ T → S"
            and WT: "closedin (top_of_set W) T"
         for W T and f :: "'a × real ⇒ 'a"
  proof -
    obtain U g
      where "T ⊆ U" and WU: "openin (top_of_set W) U"
        and contg: "continuous_on U g"
        and "g ∈ U → S" and gf: "⋀x. x ∈ T ⟹ g x = f x"
      using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor ‹ANR S›, rule_format, OF f WT]
      by auto
    have WWU: "closedin (top_of_set W) (W - U)"
      using WU closedin_diff by fastforce
    moreover have "(W - U) ∩ T = {}"
      using ‹T ⊆ U› by auto
    ultimately obtain V V'
      where WV': "openin (top_of_set W) V'"
        and WV: "openin (top_of_set W) V"
        and "W - U ⊆ V'" "T ⊆ V" "V' ∩ V = {}"
      using separation_normal_local [of W "W-U" T] WT by blast
    then have WVT: "T ∩ (W - V) = {}"
      by auto
    have WWV: "closedin (top_of_set W) (W - V)"
      using WV closedin_diff by fastforce
    obtain j :: " 'a × real ⇒ real"
      where contj: "continuous_on W j"
        and j:  "⋀x. x ∈ W ⟹ j x ∈ {0..1}"
        and j0: "⋀x. x ∈ W - V ⟹ j x = 1"
        and j1: "⋀x. x ∈ T ⟹ j x = 0"
      by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
    have Weq: "W = (W - V) ∪ (W - V')"
      using ‹V' ∩ V = {}› by force
    show ?thesis
    proof (intro conjI exI)
      have *: "continuous_on (W - V') (λx. h (j x, g x))"
      proof (rule continuous_on_compose2 [OF conth continuous_on_Pair])
        show "continuous_on (W - V') j"
          by (rule continuous_on_subset [OF contj Diff_subset])
        show "continuous_on (W - V') g"
          by (metis Diff_subset_conv ‹W - U ⊆ V'› contg continuous_on_subset Un_commute)
        show "(λx. (j x, g x)) ` (W - V') ⊆ {0..1} × S"
          using j ‹g ∈ U → S› ‹W - U ⊆ V'› by fastforce
      qed
      show "continuous_on W (λx. if x ∈ W - V then a else h (j x, g x))"
      proof (subst Weq, rule continuous_on_cases_local)
        show "continuous_on (W - V') (λx. h (j x, g x))"
          using "*" by blast
      qed (use WWV WV' Weq j0 j1 in auto)
    next
      have "h (j (x, y), g (x, y)) ∈ S" if "(x, y) ∈ W" "(x, y) ∈ V" for x y
      proof -
        have "j(x, y) ∈ {0..1}"
          using j that by blast
        moreover have "g(x, y) ∈ S"
          using ‹V' ∩ V = {}› ‹W - U ⊆ V'› ‹g ∈ U → S› that by fastforce
        ultimately show ?thesis
          using hS by blast
      qed
      with ‹a ∈ S› ‹g ∈ U → S›
      show "(λx. if x ∈ W - V then a else h (j x, g x)) ∈ W → S"
        by auto
    next
      show "∀x∈T. (if x ∈ W - V then a else h (j x, g x)) = f x"
        using ‹T ⊆ V› by (auto simp: j0 j1 gf)
    qed
  qed
  then show ?lhs
    by (simp add: AR_eq_absolute_extensor image_subset_iff_funcset)
qed


lemma ANR_retract_of_ANR:
  fixes S :: "'a::euclidean_space set"
  assumes "ANR T" and ST: "S retract_of T"
  shows "ANR S"
proof (clarsimp simp add: ANR_eq_absolute_neighbourhood_extensor)
  fix f::"'a × real ⇒ 'a" and U W
  assume W: "continuous_on W f" "f ∈ W → S" "closedin (top_of_set U) W"
  then obtain r where "S ⊆ T" and r: "continuous_on T r" "r ∈ T → S" "∀x∈S. r x = x" "continuous_on W f" "f ∈ W → S"
                                     "closedin (top_of_set U) W"
    by (metis ST retract_of_def retraction_def)
  then have "f ` W ⊆ T"
    by blast
  with W obtain V g where V: "W ⊆ V" "openin (top_of_set U) V" "continuous_on V g" "g ∈ V → T" "∀x∈W. g x = f x"
    by (smt (verit) ANR_imp_absolute_neighbourhood_extensor Pi_I assms(1) funcset_mem image_subset_iff_funcset)
  with r have "continuous_on V (r ∘ g) ∧ (r ∘ g) ∈ V → S ∧ (∀x∈W. (r ∘ g) x = f x)"
    by (smt (verit, del_insts) Pi_iff comp_apply continuous_on_compose continuous_on_subset image_subset_iff_funcset)
  then show "∃V. W ⊆ V ∧ openin (top_of_set U) V ∧ (∃g. continuous_on V g ∧ g ∈ V → S ∧ (∀x∈W. g x = f x))"
    by (meson V)
qed

lemma AR_retract_of_AR:
  fixes S :: "'a::euclidean_space set"
  shows "⟦AR T; S retract_of T⟧ ⟹ AR S"
using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce

lemma ENR_retract_of_ENR:
   "⟦ENR T; S retract_of T⟧ ⟹ ENR S"
by (meson ENR_def retract_of_trans)

lemma retract_of_UNIV:
  fixes S :: "'a::euclidean_space set"
  shows "S retract_of UNIV ⟷ AR S ∧ closed S"
by (metis AR_ANR AR_imp_retract ENR_def ENR_imp_ANR closed_UNIV closed_closedin contractible_UNIV empty_not_UNIV open_UNIV retract_of_closed retract_of_contractible retract_of_empty(1) subtopology_UNIV)

lemma compact_AR:
  fixes S :: "'a::euclidean_space set"
  shows "compact S ∧ AR S ⟷ compact S ∧ S retract_of UNIV"
using compact_imp_closed retract_of_UNIV by blast

text ‹More properties of ARs, ANRs and ENRs›

lemma not_AR_empty [simp]: "¬ AR({})"
  by (auto simp: AR_def)

lemma ENR_empty [simp]: "ENR {}"
  by (simp add: ENR_def)

lemma ANR_empty [simp]: "ANR ({} :: 'a::euclidean_space set)"
  by (simp add: ENR_imp_ANR)

lemma convex_imp_AR:
  fixes S :: "'a::euclidean_space set"
  shows "⟦convex S; S ≠ {}⟧ ⟹ AR S"
  by (metis (mono_tags, lifting) Dugundji absolute_extensor_imp_AR)

lemma convex_imp_ANR:
  fixes S :: "'a::euclidean_space set"
  shows "convex S ⟹ ANR S"
using ANR_empty AR_imp_ANR convex_imp_AR by blast

lemma ENR_convex_closed:
  fixes S :: "'a::euclidean_space set"
  shows "⟦closed S; convex S⟧ ⟹ ENR S"
using ENR_def ENR_empty convex_imp_AR retract_of_UNIV by blast

lemma AR_UNIV [simp]: "AR (UNIV :: 'a::euclidean_space set)"
  using retract_of_UNIV by auto

lemma ANR_UNIV [simp]: "ANR (UNIV :: 'a::euclidean_space set)"
  by (simp add: AR_imp_ANR)

lemma ENR_UNIV [simp]:"ENR UNIV"
  using ENR_def by blast

lemma AR_singleton:
    fixes a :: "'a::euclidean_space"
    shows "AR {a}"
  using retract_of_UNIV by blast

lemma ANR_singleton:
    fixes a :: "'a::euclidean_space"
    shows "ANR {a}"
  by (simp add: AR_imp_ANR AR_singleton)

lemma ENR_singleton: "ENR {a}"
  using ENR_def by blast

text ‹ARs closed under union›

lemma AR_closed_Un_local_aux:
  fixes U :: "'a::euclidean_space set"
  assumes "closedin (top_of_set U) S"
          "closedin (top_of_set U) T"
          "AR S" "AR T" "AR(S ∩ T)"
  shows "(S ∪ T) retract_of U"
proof -
  have "S ∩ T ≠ {}"
    using assms AR_def by fastforce
  have "S ⊆ U" "T ⊆ U"
    using assms by (auto simp: closedin_imp_subset)
  define S' where "S' ≡ {x ∈ U. setdist {x} S ≤ setdist {x} T}"
  define T' where "T' ≡ {x ∈ U. setdist {x} T ≤ setdist {x} S}"
  define W  where "W ≡ {x ∈ U. setdist {x} S = setdist {x} T}"
  have US': "closedin (top_of_set U) S'"
    using continuous_closedin_preimage [of U "λx. setdist {x} S - setdist {x} T" "{..0}"]
    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
  have UT': "closedin (top_of_set U) T'"
    using continuous_closedin_preimage [of U "λx. setdist {x} T - setdist {x} S" "{..0}"]
    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
  have "S ⊆ S'"
    using S'_def ‹S ⊆ U› setdist_sing_in_set by fastforce
  have "T ⊆ T'"
    using T'_def ‹T ⊆ U› setdist_sing_in_set by fastforce
  have "S ∩ T ⊆ W" "W ⊆ U"
    using ‹S ⊆ U› by (auto simp: W_def setdist_sing_in_set)
  have "(S ∩ T) retract_of W"
  proof (rule AR_imp_absolute_retract [OF ‹AR(S ∩ T)›])
    show "S ∩ T homeomorphic S ∩ T"
      by (simp add: homeomorphic_refl)
    show "closedin (top_of_set W) (S ∩ T)"
      by (meson ‹S ∩ T ⊆ W› ‹W ⊆ U› assms closedin_Int closedin_subset_trans)
  qed
  then obtain r0
    where "S ∩ T ⊆ W" and contr0: "continuous_on W r0"
      and "r0 ` W ⊆ S ∩ T"
      and r0 [simp]: "⋀x. x ∈ S ∩ T ⟹ r0 x = x"
      by (auto simp: retract_of_def retraction_def)
  have ST: "x ∈ W ⟹ x ∈ S ⟷ x ∈ T" for x
    using setdist_eq_0_closedin ‹S ∩ T ≠ {}› assms
    by (force simp: W_def setdist_sing_in_set)
  have "S' ∩ T' = W"
    by (auto simp: S'_def T'_def W_def)
  then have cloUW: "closedin (top_of_set U) W"
    using closedin_Int US' UT' by blast
  define r where "r ≡ λx. if x ∈ W then r0 x else x"
  have contr: "continuous_on (W ∪ (S ∪ T)) r"
  unfolding r_def
  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
    show "closedin (top_of_set (W ∪ (S ∪ T))) W"
      using ‹S ⊆ U› ‹T ⊆ U› ‹W ⊆ U› ‹closedin (top_of_set U) W› closedin_subset_trans by fastforce
    show "closedin (top_of_set (W ∪ (S ∪ T))) (S ∪ T)"
      by (meson ‹S ⊆ U› ‹T ⊆ U› ‹W ⊆ U› assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
    show "⋀x. x ∈ W ∧ x ∉ W ∨ x ∈ S ∪ T ∧ x ∈ W ⟹ r0 x = x"
      by (auto simp: ST)
  qed
  have rim: "r ` (W ∪ S) ⊆ S" "r ` (W ∪ T) ⊆ T"
    using ‹r0 ` W ⊆ S ∩ T› r_def by auto
  have cloUWS: "closedin (top_of_set U) (W ∪ S)"
    by (simp add: cloUW assms closedin_Un)
  obtain g where contg: "continuous_on U g"
    and "g ` U ⊆ S" and geqr: "⋀x. x ∈ W ∪ S ⟹ g x = r x"
  proof (rule AR_imp_absolute_extensor [OF ‹AR S› _ _ cloUWS])
    show "continuous_on (W ∪ S) r"
      using continuous_on_subset contr sup_assoc by blast
  qed (use rim in auto)
  have cloUWT: "closedin (top_of_set U) (W ∪ T)"
    by (simp add: cloUW assms closedin_Un)
  obtain h where conth: "continuous_on U h"
             and "h ` U ⊆ T" and heqr: "⋀x. x ∈ W ∪ T ⟹ h x = r x"
  proof (rule AR_imp_absolute_extensor [OF ‹AR T› _ _ cloUWT])
    show "continuous_on (W ∪ T) r"
      using continuous_on_subset contr sup_assoc by blast
  qed (use rim in auto)
  have U: "U = S' ∪ T'"
    by (force simp: S'_def T'_def)
  have cont: "continuous_on U (λx. if x ∈ S' then g x else h x)"
    unfolding U
    apply (rule continuous_on_cases_local)
    using US' UT' ‹S' ∩ T' = W› ‹U = S' ∪ T'›
          contg conth continuous_on_subset geqr heqr by auto
  have UST: "(λx. if x ∈ S' then g x else h x) ` U ⊆ S ∪ T"
    using ‹g ` U ⊆ S› ‹h ` U ⊆ T› by auto
  show ?thesis
    apply (simp add: retract_of_def retraction_def ‹S ⊆ U› ‹T ⊆ U›)
    apply (rule_tac x="λx. if x ∈ S' then g x else h x" in exI)
    using ST UST ‹S ⊆ S'› ‹S' ∩ T' = W› ‹T ⊆ T'› cont geqr heqr r_def
    by (smt (verit, del_insts) IntI Pi_I Un_iff image_subset_iff r0 subsetD) 
qed


lemma AR_closed_Un_local:
  fixes S :: "'a::euclidean_space set"
  assumes STS: "closedin (top_of_set (S ∪ T)) S"
      and STT: "closedin (top_of_set (S ∪ T)) T"
      and "AR S" "AR T" "AR(S ∩ T)"
    shows "AR(S ∪ T)"
proof -
  have "C retract_of U"
       if hom: "S ∪ T homeomorphic C" and UC: "closedin (top_of_set U) C"
       for U and C :: "('a * real) set"
  proof -
    obtain f g where hom: "homeomorphism (S ∪ T) C f g"
      using hom by (force simp: homeomorphic_def)
    have US: "closedin (top_of_set U) (C ∩ g -` S)"
      by (metis STS continuous_on_imp_closedin hom homeomorphism_def closedin_trans [OF _ UC])
    have UT: "closedin (top_of_set U) (C ∩ g -` T)"
      by (metis STT continuous_on_closed hom homeomorphism_def closedin_trans [OF _ UC])
    have "homeomorphism (C ∩ g -` S) S g f"
      using hom 
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
      apply (rule_tac x="f x" in image_eqI, auto)
      done
    then have ARS: "AR (C ∩ g -` S)"
      using ‹AR S› homeomorphic_AR_iff_AR homeomorphic_def by blast
    have "homeomorphism (C ∩ g -` T) T g f"
      using hom 
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
      apply (rule_tac x="f x" in image_eqI, auto)
      done
    then have ART: "AR (C ∩ g -` T)"
      using ‹AR T› homeomorphic_AR_iff_AR homeomorphic_def by blast
    have "homeomorphism (C ∩ g -` S ∩ (C ∩ g -` T)) (S ∩ T) g f"
      using hom
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
      apply (rule_tac x="f x" in image_eqI, auto)
      done
    then have ARI: "AR ((C ∩ g -` S) ∩ (C ∩ g -` T))"
      using ‹AR (S ∩ T)› homeomorphic_AR_iff_AR homeomorphic_def by blast
    have "C = (C ∩ g -` S) ∪ (C ∩ g -` T)"
      using hom  by (auto simp: homeomorphism_def)
    then show ?thesis
      by (metis AR_closed_Un_local_aux [OF US UT ARS ART ARI])
  qed
  then show ?thesis
    by (force simp: AR_def)
qed

corollary AR_closed_Un:
  fixes S :: "'a::euclidean_space set"
  shows "⟦closed S; closed T; AR S; AR T; AR (S ∩ T)⟧ ⟹ AR (S ∪ T)"
by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV)

text ‹ANRs closed under union›

lemma ANR_closed_Un_local_aux:
  fixes U :: "'a::euclidean_space set"
  assumes US: "closedin (top_of_set U) S"
      and UT: "closedin (top_of_set U) T"
      and "ANR S" "ANR T" "ANR(S ∩ T)"
  obtains V where "openin (top_of_set U) V" "(S ∪ T) retract_of V"
proof (cases "S = {} ∨ T = {}")
  case True with assms that show ?thesis
    by (metis ANR_imp_neighbourhood_retract Un_commute inf_bot_right sup_inf_absorb)
next
  case False
  then have [simp]: "S ≠ {}" "T ≠ {}" by auto
  have "S ⊆ U" "T ⊆ U"
    using assms by (auto simp: closedin_imp_subset)
  define S' where "S' ≡ {x ∈ U. setdist {x} S ≤ setdist {x} T}"
  define T' where "T' ≡ {x ∈ U. setdist {x} T ≤ setdist {x} S}"
  define W  where "W ≡ {x ∈ U. setdist {x} S = setdist {x} T}"
  have cloUS': "closedin (top_of_set U) S'"
    using continuous_closedin_preimage [of U "λx. setdist {x} S - setdist {x} T" "{..0}"]
    by (simp add: S'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
  have cloUT': "closedin (top_of_set U) T'"
    using continuous_closedin_preimage [of U "λx. setdist {x} T - setdist {x} S" "{..0}"]
    by (simp add: T'_def vimage_def Collect_conj_eq continuous_on_diff continuous_on_setdist)
  have "S ⊆ S'"
    using S'_def ‹S ⊆ U› setdist_sing_in_set by fastforce
  have "T ⊆ T'"
    using T'_def ‹T ⊆ U› setdist_sing_in_set by fastforce
  have "S' ∪ T' = U"
    by (auto simp: S'_def T'_def)
  have "W ⊆ S'"
    by (simp add: Collect_mono S'_def W_def)
  have "W ⊆ T'"
    by (simp add: Collect_mono T'_def W_def)
  have ST_W: "S ∩ T ⊆ W" and "W ⊆ U"
    using ‹S ⊆ U› by (force simp: W_def setdist_sing_in_set)+
  have "S' ∩ T' = W"
    by (auto simp: S'_def T'_def W_def)
  then have cloUW: "closedin (top_of_set U) W"
    using closedin_Int cloUS' cloUT' by blast
  obtain W' W0 where "openin (top_of_set W) W'"
                 and cloWW0: "closedin (top_of_set W) W0"
                 and "S ∩ T ⊆ W'" "W' ⊆ W0"
                 and ret: "(S ∩ T) retract_of W0"
    by (meson ANR_imp_closed_neighbourhood_retract ST_W US UT ‹W ⊆ U› ‹ANR(S ∩ T)› closedin_Int closedin_subset_trans)
  then obtain U0 where opeUU0: "openin (top_of_set U) U0"
                   and U0: "S ∩ T ⊆ U0" "U0 ∩ W ⊆ W0"
    unfolding openin_open  using ‹W ⊆ U› by blast
  have "W0 ⊆ U"
    using ‹W ⊆ U› cloWW0 closedin_subset by fastforce
  obtain r0
    where "S ∩ T ⊆ W0" and contr0: "continuous_on W0 r0" and "r0 ∈ W0 → S ∩ T"
      and r0 [simp]: "⋀x. x ∈ S ∩ T ⟹ r0 x = x"
    using ret  by (force simp: retract_of_def retraction_def)
  have ST: "x ∈ W ⟹ x ∈ S ⟷ x ∈ T" for x
    using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
  define r where "r ≡ λx. if x ∈ W0 then r0 x else x"
  have "r ` (W0 ∪ S) ⊆ S" "r ` (W0 ∪ T) ⊆ T"
    using ‹r0 ∈ W0 → S ∩ T› r_def by auto
  have contr: "continuous_on (W0 ∪ (S ∪ T)) r"
  unfolding r_def
  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
    show "closedin (top_of_set (W0 ∪ (S ∪ T))) W0"
      using closedin_subset_trans [of U]
      by (metis le_sup_iff order_refl cloWW0 cloUW closedin_trans ‹W0 ⊆ U› ‹S ⊆ U› ‹T ⊆ U›)
    show "closedin (top_of_set (W0 ∪ (S ∪ T))) (S ∪ T)"
      by (meson ‹S ⊆ U› ‹T ⊆ U› ‹W0 ⊆ U› assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
    show "⋀x. x ∈ W0 ∧ x ∉ W0 ∨ x ∈ S ∪ T ∧ x ∈ W0 ⟹ r0 x = x"
      using ST cloWW0 closedin_subset by fastforce
  qed
  have cloS'WS: "closedin (top_of_set S') (W0 ∪ S)"
    by (meson closedin_subset_trans US cloUS' ‹S ⊆ S'› ‹W ⊆ S'› cloUW cloWW0 
              closedin_Un closedin_imp_subset closedin_trans)
  obtain W1 g where "W0 ∪ S ⊆ W1" and contg: "continuous_on W1 g"
                and opeSW1: "openin (top_of_set S') W1"
                and "g ∈ W1 → S" and geqr: "⋀x. x ∈ W0 ∪ S ⟹ g x = r x"
  proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› _ _ cloS'WS])
    show "continuous_on (W0 ∪ S) r"
      using continuous_on_subset contr sup_assoc by blast
  qed (use ‹r ` (W0 ∪ S) ⊆ S› in auto)
  have cloT'WT: "closedin (top_of_set T') (W0 ∪ T)"
    by (meson closedin_subset_trans UT cloUT' ‹T ⊆ T'› ‹W ⊆ T'› cloUW cloWW0 
              closedin_Un closedin_imp_subset closedin_trans)
  obtain W2 h where "W0 ∪ T ⊆ W2" and conth: "continuous_on W2 h"
                and opeSW2: "openin (top_of_set T') W2"
                and "h ` W2 ⊆ T" and heqr: "⋀x. x ∈ W0 ∪ T ⟹ h x = r x"
  proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› _ _ cloT'WT])
    show "continuous_on (W0 ∪ T) r"
      using continuous_on_subset contr sup_assoc by blast
  qed (use ‹r ` (W0 ∪ T) ⊆ T› in auto)
  have "S' ∩ T' = W"
    by (force simp: S'_def T'_def W_def)
  obtain O1 O2 where O12: "open O1" "W1 = S' ∩ O1" "open O2" "W2 = T' ∩ O2"
    using opeSW1 opeSW2 by (force simp: openin_open)
  show ?thesis
  proof
    have eq: "W1 - (W - U0) ∪ (W2 - (W - U0)) 
            = ((U - T') ∩ O1 ∪ (U - S') ∩ O2 ∪ U ∩ O1 ∩ O2) - (W - U0)" (is "?WW1 ∪ ?WW2 = ?rhs")
      using ‹U0 ∩ W ⊆ W0› ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2›
      by (auto simp: ‹S' ∪ T' = U› [symmetric] ‹S' ∩ T' = W› [symmetric] ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2›)
    show "openin (top_of_set U) (?WW1 ∪ ?WW2)"
      by (simp add: eq ‹open O1› ‹open O2› cloUS' cloUT' cloUW closedin_diff opeUU0 openin_Int_open openin_Un openin_diff)
    obtain SU' where "closed SU'" "S' = U ∩ SU'"
      using cloUS' by (auto simp add: closedin_closed)
    moreover have "?WW1 = (?WW1 ∪ ?WW2) ∩ SU'"
      using ‹S' = U ∩ SU'› ‹W1 = S' ∩ O1› ‹S' ∪ T' = U› ‹W2 = T' ∩ O2›  ‹S' ∩ T' = W› ‹W0 ∪ S ⊆ W1› U0
      by auto
    ultimately have cloW1: "closedin (top_of_set (W1 - (W - U0) ∪ (W2 - (W - U0)))) (W1 - (W - U0))"
      by (metis closedin_closed_Int)
    obtain TU' where "closed TU'" "T' = U ∩ TU'"
      using cloUT' by (auto simp add: closedin_closed)
    moreover have "?WW2 = (?WW1 ∪ ?WW2) ∩ TU'"
      using ‹T' = U ∩ TU'› ‹W1 = S' ∩ O1› ‹S' ∪ T' = U› ‹W2 = T' ∩ O2›  ‹S' ∩ T' = W› ‹W0 ∪ T ⊆ W2› U0
      by auto
    ultimately have cloW2: "closedin (top_of_set (?WW1 ∪ ?WW2)) ?WW2"
      by (metis closedin_closed_Int)
    let ?gh = "λx. if x ∈ S' then g x else h x"
    have "∃r. continuous_on (?WW1 ∪ ?WW2) r ∧ r ` (?WW1 ∪ ?WW2) ⊆ S ∪ T ∧ (∀x∈S ∪ T. r x = x)"
    proof (intro exI conjI)
      show "∀x∈S ∪ T. ?gh x = x"
        using ST ‹S' ∩ T' = W› geqr heqr O12  
        by (metis Int_iff Un_iff ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› r0 r_def sup.order_iff)  
      have "⋀x. x ∈ ?WW1 ∧ x ∉ S' ∨ x ∈ ?WW2 ∧ x ∈ S' ⟹ g x = h x"
        using O12
        by (metis (full_types) DiffD1 DiffD2 DiffI IntE IntI U0(2) UnCI ‹S' ∩ T' = W› geqr heqr in_mono)
      then show "continuous_on (?WW1 ∪ ?WW2) ?gh"
        using continuous_on_cases_local [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]]
        by simp
      show "?gh ` (?WW1 ∪ ?WW2) ⊆ S ∪ T"
        using ‹W1 = S' ∩ O1› ‹W2 = T' ∩ O2› ‹S' ∩ T' = W› ‹g ∈ W1 → S› ‹h ` W2 ⊆ T› ‹U0 ∩ W ⊆ W0› ‹W0 ∪ S ⊆ W1›  
        by (auto simp add: image_subset_iff)
    qed
    then show "S ∪ T retract_of ?WW1 ∪ ?WW2"
      using  ‹W0 ∪ S ⊆ W1› ‹W0 ∪ T ⊆ W2› ST opeUU0 U0
      by (auto simp: retract_of_def retraction_def image_subset_iff_funcset)
  qed
qed


lemma ANR_closed_Un_local:
  fixes S :: "'a::euclidean_space set"
  assumes STS: "closedin (top_of_set (S ∪ T)) S"
      and STT: "closedin (top_of_set (S ∪ T)) T"
      and "ANR S" "ANR T" "ANR(S ∩ T)" 
    shows "ANR(S ∪ T)"
proof -
  have "∃T. openin (top_of_set U) T ∧ C retract_of T"
       if hom: "S ∪ T homeomorphic C" and UC: "closedin (top_of_set U) C"
       for U and C :: "('a * real) set"
  proof -
    obtain f g where hom: "homeomorphism (S ∪ T) C f g"
      using hom by (force simp: homeomorphic_def)
    have US: "closedin (top_of_set U) (C ∩ g -` S)"
      by (metis STS UC closedin_trans continuous_on_imp_closedin hom homeomorphism_def)
    have UT: "closedin (top_of_set U) (C ∩ g -` T)"
      by (metis STT UC closedin_trans continuous_on_imp_closedin hom homeomorphism_def)
    have "homeomorphism (C ∩ g -` S) S g f"
      using hom 
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
      by (rule_tac x="f x" in image_eqI, auto)
    then have ANRS: "ANR (C ∩ g -` S)"
      using ‹ANR S› homeomorphic_ANR_iff_ANR homeomorphic_def by blast
    have "homeomorphism (C ∩ g -` T) T g f"
      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
      by (rule_tac x="f x" in image_eqI, auto)
    then have ANRT: "ANR (C ∩ g -` T)"
      using ‹ANR T› homeomorphic_ANR_iff_ANR homeomorphic_def by blast
    have "homeomorphism (C ∩ g -` S ∩ (C ∩ g -` T)) (S ∩ T) g f"
      using hom
      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
      by (rule_tac x="f x" in image_eqI, auto)
    then have ANRI: "ANR ((C ∩ g -` S) ∩ (C ∩ g -` T))"
      using ‹ANR (S ∩ T)› homeomorphic_ANR_iff_ANR homeomorphic_def by blast
    have "C = (C ∩ g -` S) ∪ (C ∩ g -` T)"
      using hom by (auto simp: homeomorphism_def)
    then show ?thesis
      by (metis ANR_closed_Un_local_aux [OF US UT ANRS ANRT ANRI])
  qed
  then show ?thesis
    by (auto simp: ANR_def)
qed    

corollary ANR_closed_Un:
  fixes S :: "'a::euclidean_space set"
  shows "⟦closed S; closed T; ANR S; ANR T; ANR (S ∩ T)⟧ ⟹ ANR (S ∪ T)"
by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int)

lemma ANR_openin:
  fixes S :: "'a::euclidean_space set"
  assumes "ANR T" and opeTS: "openin (top_of_set T) S"
  shows "ANR S"
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
  fix f :: "'a × real ⇒ 'a" and U C
  assume contf: "continuous_on C f" and fim: "f ∈ C → S"
     and cloUC: "closedin (top_of_set U) C"
  have "f ∈ C → T"
    using fim opeTS openin_imp_subset by blast
  obtain W g where "C ⊆ W"
               and UW: "openin (top_of_set U) W"
               and contg: "continuous_on W g"
               and gim: "g ∈ W → T"
               and geq: "⋀x. x ∈ C ⟹ g x = f x"
    using ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf ‹f ∈ C → T› cloUC] fim by auto
  show "∃V g. C ⊆ V ∧ openin (top_of_set U) V ∧ continuous_on V g ∧ g ∈ V → S ∧ (∀x∈C. g x = f x)"
  proof (intro exI conjI)
    show "C ⊆ W ∩ g -` S"
      using ‹C ⊆ W› fim geq by blast
    show "openin (top_of_set U) (W ∩ g -` S)"
      by (metis (mono_tags, lifting) UW contg continuous_openin_preimage gim opeTS openin_trans)
    show "continuous_on (W ∩ g -` S) g"
      by (blast intro: continuous_on_subset [OF contg])
    show "g ∈ (W ∩ g -` S) → S"
      using gim by blast
    show "∀x∈C. g x = f x"
      using geq by blast
  qed
qed

lemma ENR_openin:
    fixes S :: "'a::euclidean_space set"
    assumes "ENR T" "openin (top_of_set T) S"
    shows "ENR S"
  by (meson ANR_openin ENR_ANR assms locally_open_subset)

lemma ANR_neighborhood_retract:
    fixes S :: "'a::euclidean_space set"
    assumes "ANR U" "S retract_of T" "openin (top_of_set U) T"
    shows "ANR S"
  using ANR_openin ANR_retract_of_ANR assms by blast

lemma ENR_neighborhood_retract:
    fixes S :: "'a::euclidean_space set"
    assumes "ENR U" "S retract_of T" "openin (top_of_set U) T"
    shows "ENR S"
  using ENR_openin ENR_retract_of_ENR assms by blast

lemma ANR_rel_interior:
  fixes S :: "'a::euclidean_space set"
  shows "ANR S ⟹ ANR(rel_interior S)"
   by (blast intro: ANR_openin openin_set_rel_interior)

lemma ANR_delete:
  fixes S :: "'a::euclidean_space set"
  shows "ANR S ⟹ ANR(S - {a})"
   by (blast intro: ANR_openin openin_delete openin_subtopology_self)

lemma ENR_rel_interior:
  fixes S :: "'a::euclidean_space set"
  shows "ENR S ⟹ ENR(rel_interior S)"
   by (blast intro: ENR_openin openin_set_rel_interior)

lemma ENR_delete:
  fixes S :: "'a::euclidean_space set"
  shows "ENR S ⟹ ENR(S - {a})"
   by (blast intro: ENR_openin openin_delete openin_subtopology_self)

lemma open_imp_ENR: "open S ⟹ ENR S"
    using ENR_def by blast

lemma open_imp_ANR:
    fixes S :: "'a::euclidean_space set"
    shows "open S ⟹ ANR S"
  by (simp add: ENR_imp_ANR open_imp_ENR)

lemma ANR_ball [iff]:
    fixes a :: "'a::euclidean_space"
    shows "ANR(ball a r)"
  by (simp add: convex_imp_ANR)

lemma ENR_ball [iff]: "ENR(ball a r)"
  by (simp add: open_imp_ENR)

lemma AR_ball [simp]:
    fixes a :: "'a::euclidean_space"
    shows "AR(ball a r) ⟷ 0 < r"
  by (auto simp: AR_ANR convex_imp_contractible)

lemma ANR_cball [iff]:
    fixes a :: "'a::euclidean_space"
    shows "ANR(cball a r)"
  by (simp add: convex_imp_ANR)

lemma ENR_cball:
    fixes a :: "'a::euclidean_space"
    shows "ENR(cball a r)"
  using ENR_convex_closed by blast

lemma AR_cball [simp]:
    fixes a :: "'a::euclidean_space"
    shows "AR(cball a r) ⟷ 0 ≤ r"
  by (auto simp: AR_ANR convex_imp_contractible)

lemma ANR_box [iff]:
    fixes a :: "'a::euclidean_space"
    shows "ANR(cbox a b)" "ANR(box a b)"
  by (auto simp: convex_imp_ANR open_imp_ANR)

lemma ENR_box [iff]:
    fixes a :: "'a::euclidean_space"
    shows "ENR(cbox a b)" "ENR(box a b)"
  by (simp_all add: ENR_convex_closed closed_cbox open_box open_imp_ENR)

lemma AR_box [simp]:
    "AR(cbox a b) ⟷ cbox a b ≠ {}" "AR(box a b) ⟷ box a b ≠ {}"
  by (auto simp: AR_ANR convex_imp_contractible)

lemma ANR_interior:
     fixes S :: "'a::euclidean_space set"
     shows "ANR(interior S)"
  by (simp add: open_imp_ANR)

lemma ENR_interior:
     fixes S :: "'a::euclidean_space set"
     shows "ENR(interior S)"
  by (simp add: open_imp_ENR)

lemma AR_imp_contractible:
    fixes S :: "'a::euclidean_space set"
    shows "AR S ⟹ contractible S"
  by (simp add: AR_ANR)

lemma ENR_imp_locally_compact:
    fixes S :: "'a::euclidean_space set"
    shows "ENR S ⟹ locally compact S"
  by (simp add: ENR_ANR)

lemma ANR_imp_locally_path_connected:
  fixes S :: "'a::euclidean_space set"
  assumes "ANR S"
    shows "locally path_connected S"
proof -
  obtain U and T :: "('a × real) set"
     where "convex U" "U ≠ {}"
       and UT: "closedin (top_of_set U) T" and "S homeomorphic T"
  proof (rule homeomorphic_closedin_convex)
    show "aff_dim S < int DIM('a × real)"
      using aff_dim_le_DIM [of S] by auto
  qed auto
  then have "locally path_connected T"
    by (meson ANR_imp_absolute_neighbourhood_retract
        assms convex_imp_locally_path_connected locally_open_subset retract_of_locally_path_connected)
  then have S: "locally path_connected S"
      if "openin (top_of_set U) V" "T retract_of V" "U ≠ {}" for V
    using ‹S homeomorphic T› homeomorphic_locally homeomorphic_path_connectedness by blast
  obtain Ta where "(openin (top_of_set U) Ta ∧ T retract_of Ta)"
    using ANR_def UT ‹S homeomorphic T› assms by atomize_elim (auto simp: choice)
  then show ?thesis
    using S ‹U ≠ {}› by blast
qed

lemma ANR_imp_locally_connected:
  fixes S :: "'a::euclidean_space set"
  assumes "ANR S"
    shows "locally connected S"
using locally_path_connected_imp_locally_connected ANR_imp_locally_path_connected assms by auto

lemma AR_imp_locally_path_connected:
  fixes S :: "'a::euclidean_space set"
  assumes "AR S"
    shows "locally path_connected S"
by (simp add: ANR_imp_locally_path_connected AR_imp_ANR assms)

lemma AR_imp_locally_connected:
  fixes S :: "'a::euclidean_space set"
  assumes "AR S"
    shows "locally connected S"
using ANR_imp_locally_connected AR_ANR assms by blast

lemma ENR_imp_locally_path_connected:
  fixes S :: "'a::euclidean_space set"
  assumes "ENR S"
    shows "locally path_connected S"
by (simp add: ANR_imp_locally_path_connected ENR_imp_ANR assms)

lemma ENR_imp_locally_connected:
  fixes S :: "'a::euclidean_space set"
  assumes "ENR S"
    shows "locally connected S"
using ANR_imp_locally_connected ENR_ANR assms by blast

lemma ANR_Times:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "ANR S" "ANR T" shows "ANR(S × T)"
proof (clarsimp simp only: ANR_eq_absolute_neighbourhood_extensor)
  fix f :: " ('a × 'b) × real ⇒ 'a × 'b" and U C
  assume "continuous_on C f" and fim: "f ∈ C → S × T"
     and cloUC: "closedin (top_of_set U) C"
  have contf1: "continuous_on C (fst ∘ f)"
    by (simp add: ‹continuous_on C f› continuous_on_fst)
  obtain W1 g where "C ⊆ W1"
               and UW1: "openin (top_of_set U) W1"
               and contg: "continuous_on W1 g"
               and gim: "g ` W1 ⊆ S"
               and geq: "⋀x. x ∈ C ⟹ g x = (fst ∘ f) x"
  proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR S› contf1 _ cloUC])
    show "(fst ∘ f) ∈ C → S"
      using fim by force
  qed auto
  have contf2: "continuous_on C (snd ∘ f)"
    by (simp add: ‹continuous_on C f› continuous_on_snd)
  obtain W2 h where "C ⊆ W2"
               and UW2: "openin (top_of_set U) W2"
               and conth: "continuous_on W2 h"
               and him: "h ∈ W2 → T"
               and heq: "⋀x. x ∈ C ⟹ h x = (snd ∘ f) x"
  proof (rule ANR_imp_absolute_neighbourhood_extensor [OF ‹ANR T› contf2 _ cloUC])
    show "(snd ∘ f) ∈ C → T"
      using fim by force
  qed auto
  show "∃V g. C ⊆ V ∧
               openin (top_of_set U) V ∧
               continuous_on V g ∧ g ∈ V → S × T ∧ (∀x∈C. g x = f x)"
  proof (intro exI conjI)
    show "C ⊆ W1 ∩ W2"
      by (simp add: ‹C ⊆ W1› ‹C ⊆ W2›)
    show "openin (top_of_set U) (W1 ∩ W2)"
      by (simp add: UW1 UW2 openin_Int)
    show  "continuous_on (W1 ∩ W2) (λx. (g x, h x))"
      by (metis (no_types) contg conth continuous_on_Pair continuous_on_subset inf_commute inf_le1)
    show  "(λx. (g x, h x)) ∈ (W1 ∩ W2) → S × T"
      using gim him by blast
    show  "(∀x∈C. (g x, h x) = f x)"
      using geq heq by auto
  qed
qed

lemma AR_Times:
  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
  assumes "AR S" "AR T" shows "AR(S × T)"
  using assms by (simp add: AR_ANR ANR_Times contractible_Times)

(* Unused and requires ordered_euclidean_space
subsection✐‹tag unimportant›‹Retracts and intervals in ordered euclidean space›

lemma ANR_interval [iff]:
  fixes a :: "'a::ordered_euclidean_space"
  shows "ANR{a..b}"
  by (simp add: interval_cbox)

lemma ENR_interval [iff]:
  fixes a :: "'a::ordered_euclidean_space"
  shows "ENR{a..b}"
  by (auto simp: interval_cbox)
*)

subsection ‹More advanced properties of ANRs and ENRs›

lemma ENR_rel_frontier_convex:
  fixes S :: "'a::euclidean_space set"
  assumes "bounded S" "convex S"
    shows "ENR(rel_frontier S)"
proof (cases "S = {}")
  case True then show ?thesis
    by simp
next
  case False
  with assms have "rel_interior S ≠ {}"
    by (simp add: rel_interior_eq_empty)
  then obtain a where a: "a ∈ rel_interior S"
    by auto
  have ahS: "affine hull S - {a} ⊆ {x. closest_point (affine hull S) x ≠ a}"
    by (auto simp: closest_point_self)
  have "rel_frontier S retract_of affine hull S - {a}"
    by (simp add: assms a rel_frontier_retract_of_punctured_affine_hull)
  also have "… retract_of {x. closest_point (affine hull S) x ≠ a}"
    unfolding retract_of_def retraction_def ahS
    apply (rule_tac x="closest_point (affine hull S)" in exI)
    apply (auto simp: False closest_point_self affine_imp_convex closest_point_in_set continuous_on_closest_point)
    done
  finally have "rel_frontier S retract_of {x. closest_point (affine hull S) x ≠ a}" .
  moreover have "openin (top_of_set UNIV) (UNIV ∩ closest_point (affine hull S) -` (- {a}))"
    by (intro continuous_openin_preimage_gen) (auto simp: False affine_imp_convex continuous_on_closest_point)
  ultimately show ?thesis
    by (meson ENR_convex_closed ENR_delete ENR_retract_of_ENR ‹rel_frontier S retract_of affine hull S - {a}› 
              closed_affine_hull convex_affine_hull)
qed

lemma ANR_rel_frontier_convex:
                 fixes S :: "'a::euclidean_space set"
  assumes "bounded S" "convex S"
    shows "ANR(rel_frontier S)"
by (simp add: ENR_imp_ANR ENR_rel_frontier_convex assms)
    
lemma ENR_closedin_Un_local:
  fixes S :: "'a::euclidean_space set"
  shows "⟦ENR S; ENR T; ENR(S ∩ T);
          closedin (top_of_set (S ∪ T)) S; closedin (top_of_set (S ∪ T)) T⟧
        ⟹ ENR(S ∪ T)"
by (simp add: ENR_ANR ANR_closed_Un_local locally_compact_closedin_Un)

lemma ENR_closed_Un:
  fixes S :: "'a::euclidean_space set"
  shows "⟦closed S; closed T; ENR S; ENR T; ENR(S ∩ T)⟧ ⟹ ENR(S ∪ T)"
by (auto simp: closed_subset ENR_closedin_Un_local)

lemma absolute_retract_Un:
  fixes S :: "'a::euclidean_space set"
  shows "⟦S retract_of UNIV; T retract_of UNIV; (S ∩ T) retract_of UNIV⟧
         ⟹ (S ∪ T) retract_of UNIV"
  by (meson AR_closed_Un_local_aux closed_subset retract_of_UNIV retract_of_imp_subset)

lemma retract_from_Un_Int:
  fixes S :: "'a::euclidean_space set"
  assumes clS: "closedin (top_of_set (S ∪ T)) S"
      and clT: "closedin (top_of_set (S ∪ T)) T"
      and Un: "(S ∪ T) retract_of U" and Int: "(S ∩ T) retract_of T"
    shows "S retract_of U"
proof -
  obtain r where r: "continuous_on T r" "r ` T ⊆ S ∩ T" "∀x∈S ∩ T. r x = x"
    using Int by (auto simp: retraction_def retract_of_def)
  have "S retract_of S ∪ T"
    unfolding retraction_def retract_of_def
  proof (intro exI conjI)
    show "continuous_on (S ∪ T) (λx. if x ∈ S then x else r x)"
      using r by (intro continuous_on_cases_local [OF clS clT]) auto
  qed (use r in auto)
  also have "… retract_of U"
    by (rule Un)
  finally show ?thesis .
qed

lemma AR_from_Un_Int_local:
  fixes S :: "'a::euclidean_space set"
  assumes clS: "closedin (top_of_set (S ∪ T)) S"
      and clT: "closedin (top_of_set (S ∪ T)) T"
      and Un: "AR(S ∪ T)" and Int: "AR(S ∩ T)"
    shows "AR S"
  by (meson AR_imp_retract AR_retract_of_AR Un assms closedin_closed_subset local.Int 
            retract_from_Un_Int retract_of_refl sup_ge2)

lemma AR_from_Un_Int_local':
  fixes S :: "'a::euclidean_space set"
  assumes "closedin (top_of_set (S ∪ T)) S"
      and "closedin (top_of_set (S ∪ T)) T"
      and "AR(S ∪ T)" "AR(S ∩ T)"
    shows "AR T"
  using AR_from_Un_Int_local [of T S] assms by (simp add: Un_commute Int_commute)

lemma AR_from_Un_Int:
  fixes S :: "'a::euclidean_space set"
  assumes clo: "closed S" "closed T" and Un: "AR(S ∪ T)" and Int: "AR(S ∩ T)"
  shows "AR S"
  by (metis AR_from_Un_Int_local [OF _ _ Un Int] Un_commute clo closed_closedin closedin_closed_subset inf_sup_absorb subtopology_UNIV top_greatest)

lemma ANR_from_Un_Int_local:
  fixes S :: "'a::euclidean_space set"
  assumes clS: "closedin (top_of_set (S ∪ T)) S"
      and clT: "closedin (top_of_set (S ∪ T)) T"
      and Un: "ANR(S ∪ T)" and Int: "ANR(S ∩ T)"
    shows "ANR S"
proof -
  obtain V where clo: "closedin (top_of_set (S ∪ T)) (S ∩ T)"
             and ope: "openin (top_of_set (S ∪ T)) V"
             and ret: "S ∩ T retract_of V"
    using ANR_imp_neighbourhood_retract [OF Int] by (metis clS clT closedin_Int)
  then obtain r where r: "continuous_on V r" and rim: "r ` V ⊆ S ∩ T" and req: "∀x∈S ∩ T. r x = x"
    by (auto simp: retraction_def retract_of_def)
  have Vsub: "V ⊆ S ∪ T"
    by (meson ope openin_contains_cball)
  have Vsup: "S ∩ T ⊆ V"
    by (simp add: retract_of_imp_subset ret)
  then have eq: "S ∪ V = ((S ∪ T) - T) ∪ V"
    by auto
  have eq': "S ∪ V = S ∪ (V ∩ T)"
    using Vsub by blast
  have "continuous_on (S ∪ V ∩ T) (λx. if x ∈ S then x else r x)"
  proof (rule continuous_on_cases_local)
    show "closedin (top_of_set (S ∪ V ∩ T)) S"
      using clS closedin_subset_trans inf.boundedE by blast
    show "closedin (top_of_set (S ∪ V ∩ T)) (V ∩ T)"
      using clT Vsup by (auto simp: closedin_closed)
    show "continuous_on (V ∩ T) r"
      by (meson 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 using eq' by fastforce
  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, opaque_lifting) 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
    by (meson ENR_def Elementary_Metric_Spaces.open_ball bounded_Int bounded_ball inf_le2 le_inf_iff 
              open_Int r retract_of_imp_subset retract_of_subset)
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
  by (metis compact_AR homeomorphic_AR_iff_AR)

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"
  by (meson ANR_from_Un_Int_local ANR_imp_neighbourhood_retract ENR_ANR ENR_neighborhood_retract assms)


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})"
    using assms frontier_retract_of_punctured_universe interior_cball by blast
  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✐‹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 (fastforce 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)"
  proof (rule continuous_intros)+
    show "continuous_on (snd ` ({0} × T)) f"
      by (simp add: contf)
  qed
  ultimately have "continuous_on ({0..1} × S ∪ {0} × T) (λx. if snd x ∈ S then h x else (f ∘ snd) x)"
    by (auto intro!: continuous_on_cases_local conth simp: B_def Un_commute [of "{0} × T"])
  then have conth': "continuous_on B h'"
    by (simp add: h'_def B_def Un_commute [of "{0} × T"])
  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"
      unfolding B_def
    proof (rule ANR_closed_Un_local)
      show "closedin (top_of_set ({0} × T ∪ {0..1} × S)) ({0::real} × T)"
        by (metis cloBT B_def)
      show "closedin (top_of_set ({0} × T ∪ {0..1} × S)) ({0..1::real} × S)"
        by (metis Un_commute cloBS B_def)
    qed (simp_all add: ANR_Times convex_imp_ANR ANR_singleton ST eq)
    note Vk = that
    have *: thesis if "openin (top_of_set ({0..1::real} × T)) V"
                      "retraction V B r" for V r
    proof -
      have "continuous_on V (h' ∘ r)"
        using conth' continuous_on_compose retractionE that(2) by blast
      moreover have "(h' ∘ r) ` V ⊆ U"
        by (metis ‹h' ` B ⊆ U› image_comp retractionE that(2))
      ultimately show ?thesis
        using Vk [of V "h' ∘ r"] by (metis comp_apply retraction image_subset_iff_funcset that)
    qed
    show thesis
      by (meson "*" ANR_imp_neighbourhood_retract ‹ANR B› clo0TB retract_of_def)
  next
    assume "ANR U"
    with ANR_imp_absolute_neighbourhood_extensor ‹h' ` B ⊆ U› clo0TB conth' image_subset_iff_funcset that
    show ?thesis
      by (smt (verit) Pi_I funcset_mem) 
  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 using closedin_self opeTV 
    by (blast intro: closedin_compact_projection)
  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"
    by (rule Urysohn_local [OF cloTS cloTS' ‹S ∩ S' = {}›, of 1 0], blast)
  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
      by (metis (no_types, lifting) a0 DiffI 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 *⇩R (a ∘ snd) z, snd z)))"
        apply (intro continuous_on_compose continuous_intros)
        apply (force intro: inV continuous_on_subset [OF contk] continuous_on_subset [OF conta])+
        done
      show "(k ∘ (λz. (fst z *⇩R (a ∘ snd) z, snd z))) ` ({0..1} × T) ⊆ U"
        using inV kim by auto
      show "∀x∈T. (k ∘ (λz. (fst z *⇩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 *⇩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 image_subset_iff_funcset)
  qed
  show "⋀x. x ∈ S ⟹ k (a x, x) = g x"
    by (simp add: B_def a1 h'_def keq)
  qed
qed


corollary✐‹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"
  proof (rule Borsuk_homotopy_extension_homotopic)
    show "(λx. c) ∈ UNIV → T"
      using ‹S ≠ {}› c homotopic_with_imp_subset1 by fastforce
  qed (use assms c in auto)
  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✐‹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✐‹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
    by (metis ANR_sphere ‹closed S› ‹S ≠ {}› contf nullhomotopic_into_ANR_extension)
next
  case False
  then have eq: "sphere a r = rel_frontier (cball a r)" by simp
  show ?thesis
    using fim nullhomotopic_into_rel_frontier_extension [OF ‹closed S› contf convex_cball bounded_cball]
    by (simp add: ‹S ≠ {}› eq)
qed

proposition✐‹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)) *⇩R (x - a)) (λx. c))"
   (is "?lhs = ?rhs")
proof (cases "S = {}")
  case True then show ?thesis
    by (simp add: homotopic_on_emptyI)
next
  case False
  have "closed S" "bounded S"
    using ‹compact S› compact_eq_bounded_closed by auto
  have s01: "(λx. (x - a) /⇩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) /⇩R norm (x - a))"
      if "bounded (connected_component_set (- S) a)"
      using non_extensible_Borsuk_map [OF ‹compact S› componentsI _ aincc] ‹a ∉ S› that by auto
    obtain g where "range g ⊆ sphere 0 1" "continuous_on UNIV g"
                        "⋀x. x ∈ S ⟹ g x = (x - a) /⇩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"
      by (metis UNIV_I continuous_on_subset image_subset_iff nog subsetI)
  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) /⇩R norm (x - a))
                                                         (λx. (x - b) /⇩R norm (x - b))"
    proof -
      have "path_component (- S) a b"
        by (metis (full_types) ‹closed S› b mem_Collect_eq open_Compl open_path_connected_component)
      then show ?thesis
        using Borsuk_maps_homotopic_in_path_component by blast
    qed
    moreover
    obtain c where "homotopic_with_canon (λx. True) (ball 0 r) (sphere 0 1)
                                   (λx. inverse (norm (x - b)) *⇩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)) *⇩R (x - b))"
        by (rule continuous_on_Borsuk_map [OF bnot])
      show "(λx. (x - b) /⇩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) /⇩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) /⇩R norm (x - a))
                               (λx. (x - b) /⇩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) /⇩R norm (x - a))"
    using non_extensible_Borsuk_map [OF ‹compact S› _ boc] ‹a ∉ S›
    by (simp add: componentsI)
  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) /⇩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) /⇩R norm (x - b))"
      by (simp add: ‹b ∉ S› notcc continuous_on_Borsuk_map)
    show "(λx. (x - b) /⇩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) /⇩R norm (x - b)) (λx. (x - a) /⇩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) /⇩R norm (x - a))
                   (λx. (x - b) /⇩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"
      using Seq clo ope  by (intro continuous_on_cases_local) (auto simp: contf)
    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 image_subset_iff_funcset)
  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✐‹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"] image_subset_iff_funcset)
  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✐‹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<k. b ∉ 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<i. V 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<i. V m)))"
        by (force simp: Ball_def dest: wop)
      show "openin (top_of_set ({0..1} × ⋃(V ` UNIV))) 
                   ({0..1::real} × (V i - (⋃m<i. V m)))" for i
      proof (intro openin_Times openin_subtopology_self openin_diff)
        show "openin (top_of_set (⋃(V ` UNIV))) (V i)"
          using ope V eqU by auto
        show "closedin (top_of_set (⋃(V ` UNIV))) (⋃m<i. V m)"
          using V clo eqU by (force intro: closedin_Union)
      qed
      show "continuous_map (subtopology ?X ({0..1} × (V i - ⋃ (V ` {..<i})))) euclidean (h i)"  for i
        by (auto simp add: subtopology_subtopology intro!: continuous_on_subset [OF conth])
      show "⋀i j x. x ∈ topspace ?X ∩ {0..1} × (V i - (⋃m<i. V m)) ∩ {0..1} × (V j - (⋃m<j. V 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<k. y ∉ 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<k. y ∉ 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)
      using Seq cloφ opeφ homφ by (intro homotopic_on_clopen_Union) 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] contf contg continuous_on_subset fim gim in_components_subset
      by (smt (verit, del_insts) Pi_anti_mono subsetD 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
  proof (clarsimp simp: connected_iff_connected_component_eq)
    have "¬ bounded (connected_component_set (- S) x)" if "x ∉ S" for x
      by (meson Compl_iff assms componentsI that unbounded_components_complement_absolute_retract)
    then show "connected_component_set (- S) x = connected_component_set (- S) y" 
      if "x ∉ S" "y ∉ S" for x y
      using cobounded_unique_unbounded_component [OF _ 2]
      by (metis ‹compact S› compact_imp_bounded double_compl that)
  qed
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