# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1466002344 -3600
# Node ID 3b69758756331faf4c267e4051862fe7f0eef9dc
# Parent  00a135c0a17fe1c9215dc4119ed19a95feaad171
Urysohn's lemma, Dugundji extension theorem and many other proofs

diff -r 00a135c0a17f -r 3b6975875633 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Jun 14 20:48:42 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Jun 15 15:52:24 2016 +0100
@@ -1,5 +1,5 @@
 (*  Author:     John Harrison
-    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light)
+    Author:     Robert Himmelmann, TU Muenchen (Translation from HOL light) and LCP
 *)
 
 (* ========================================================================= *)
@@ -2293,4 +2293,1073 @@
     by blast
 qed
 
+subsection\<open>Absolute retracts, Etc.\<close>
+
+text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
+ Euclidean neighbourhood retracts (ENR). We define AR and ANR by
+ specializing the standard definitions for a set to embedding in
+spaces of higher dimension. This turns out to be sufficient (since any set in
+R^n can be embedded as a closed subset of a convex subset of R^{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.\<close>
+
+definition AR :: "'a::topological_space set => bool"
+  where
+   "AR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
+                \<longrightarrow> S' retract_of U"
+
+definition ANR :: "'a::topological_space set => bool"
+  where
+   "ANR S \<equiv> \<forall>U. \<forall>S'::('a * real) set. S homeomorphic S' \<and> closedin (subtopology euclidean U) S'
+                \<longrightarrow> (\<exists>T. openin (subtopology euclidean U) T \<and>
+                        S' retract_of T)"
+
+definition ENR :: "'a::topological_space set => bool"
+  where "ENR S \<equiv> \<exists>U. open U \<and> S retract_of U"
+
+text\<open> First, show that we do indeed get the "usual" properties of ARs and ANRs.\<close>
+
+proposition AR_imp_absolute_extensor:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "AR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
+      and cloUT: "closedin (subtopology euclidean U) T"
+  obtains g where "continuous_on U g" "g ` U \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
+proof -
+  have "aff_dim S < int (DIM('b \<times> real))"
+    using aff_dim_le_DIM [of S] by simp
+  then obtain C and S' :: "('b * real) set"
+          where C: "convex C" "C \<noteq> {}"
+            and cloCS: "closedin (subtopology euclidean C) S'"
+            and hom: "S homeomorphic S'"
+    by (metis that homeomorphic_closedin_convex)
+  then have "S' retract_of C"
+    using \<open>AR S\<close> by (simp add: AR_def)
+  then obtain r where "S' \<subseteq> C" and contr: "continuous_on C r"
+                  and "r ` C \<subseteq> S'" and rid: "\<And>x. x\<in>S' \<Longrightarrow> r x = x"
+    by (auto simp: retraction_def retract_of_def)
+  obtain g h where "homeomorphism S S' g h"
+    using hom by (force simp: homeomorphic_def)
+  then have "continuous_on (f ` T) g"
+    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def)
+  then have contgf: "continuous_on T (g o f)"
+    by (metis continuous_on_compose contf)
+  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
+  proof -
+    have "g ` S = S'"
+      by (metis (no_types) \<open>homeomorphism S S' g h\<close> homeomorphism_def)
+    with \<open>S' \<subseteq> C\<close> \<open>f ` T \<subseteq> S\<close> show ?thesis by force
+  qed
+  obtain f' where f': "continuous_on U f'"  "f' ` U \<subseteq> C"
+                      "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
+    by (metis Dugundji [OF C cloUT contgf gfTC])
+  show ?thesis
+  proof (rule_tac g = "h o r o f'" in that)
+    show "continuous_on U (h \<circ> r \<circ> f')"
+      apply (intro continuous_on_compose f')
+       using continuous_on_subset contr f' apply blast
+      by (meson \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> continuous_on_subset \<open>f' ` U \<subseteq> C\<close> homeomorphism_def image_mono)
+    show "(h \<circ> r \<circ> f') ` U \<subseteq> S"
+      using \<open>homeomorphism S S' g h\<close> \<open>r ` C \<subseteq> S'\<close> \<open>f' ` U \<subseteq> C\<close>
+      by (fastforce simp: homeomorphism_def)
+    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
+      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> f'
+      by (auto simp: rid homeomorphism_def)
+  qed
+qed
+
+lemma AR_imp_absolute_retract:
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  assumes "AR S" "S homeomorphic S'"
+      and clo: "closedin (subtopology euclidean U) S'"
+    shows "S' retract_of U"
+proof -
+  obtain g h where hom: "homeomorphism S S' g h"
+    using assms by (force simp: homeomorphic_def)
+  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
+    using hom homeomorphism_def apply blast
+    apply (metis hom equalityE homeomorphism_def)
+    done
+  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
+              and h'h: "\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
+    by (blast intro: AR_imp_absolute_extensor [OF \<open>AR S\<close> h clo])
+  have [simp]: "S' \<subseteq> U" using clo closedin_limpt by blast
+  show ?thesis
+  proof (simp add: retraction_def retract_of_def, intro exI conjI)
+    show "continuous_on U (g o h')"
+      apply (intro continuous_on_compose h')
+      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
+      done
+    show "(g \<circ> h') ` U \<subseteq> S'"
+      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
+    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
+      by clarsimp (metis h'h hom homeomorphism_def)
+  qed
+qed
+
+lemma AR_imp_absolute_retract_UNIV:
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  assumes "AR S" and hom: "S homeomorphic S'"
+      and clo: "closed S'"
+    shows "S' retract_of UNIV"
+apply (rule AR_imp_absolute_retract [OF \<open>AR S\<close> hom])
+using clo closed_closedin by auto
+
+lemma absolute_extensor_imp_AR:
+  fixes S :: "'a::euclidean_space set"
+  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
+           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
+                  closedin (subtopology euclidean U) T\<rbrakk>
+                 \<Longrightarrow> \<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
+  shows "AR S"
+proof (clarsimp simp: AR_def)
+  fix U and T :: "('a * real) set"
+  assume "S homeomorphic T" and clo: "closedin (subtopology euclidean U) T"
+  then obtain g h where hom: "homeomorphism S T g h"
+    by (force simp: homeomorphic_def)
+  have h: "continuous_on T h" " h ` T \<subseteq> S"
+    using hom homeomorphism_def apply blast
+    apply (metis hom equalityE homeomorphism_def)
+    done
+  obtain h' where h': "continuous_on U h'" "h' ` U \<subseteq> S"
+              and h'h: "\<forall>x\<in>T. h' x = h x"
+    using assms [OF h clo] by blast
+  have [simp]: "T \<subseteq> U"
+    using clo closedin_imp_subset by auto
+  show "T retract_of U"
+  proof (simp add: retraction_def retract_of_def, intro exI conjI)
+    show "continuous_on U (g o h')"
+      apply (intro continuous_on_compose h')
+      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
+      done
+    show "(g \<circ> h') ` U \<subseteq> T"
+      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
+    show "\<forall>x\<in>T. (g \<circ> h') x = x"
+      by clarsimp (metis h'h hom homeomorphism_def)
+  qed
+qed
+
+lemma AR_eq_absolute_extensor:
+  fixes S :: "'a::euclidean_space set"
+  shows "AR S \<longleftrightarrow>
+       (\<forall>f :: 'a * real \<Rightarrow> 'a.
+        \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
+               closedin (subtopology euclidean U) T \<longrightarrow>
+                (\<exists>g. continuous_on U g \<and> g ` U \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
+apply (rule iffI)
+ apply (metis AR_imp_absolute_extensor)
+apply (simp add: absolute_extensor_imp_AR)
+done
+
+lemma AR_imp_retract:
+  fixes S :: "'a::euclidean_space set"
+  assumes "AR S \<and> closedin (subtopology euclidean U) S"
+    shows "S retract_of U"
+using AR_imp_absolute_retract assms homeomorphic_refl by blast
+
+lemma AR_homeomorphic_AR:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "AR T" "S homeomorphic T"
+    shows "AR S"
+unfolding AR_def
+by (metis assms AR_imp_absolute_retract homeomorphic_trans [of _ S] homeomorphic_sym)
+
+lemma homeomorphic_AR_iff_AR:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  shows "S homeomorphic T \<Longrightarrow> AR S \<longleftrightarrow> AR T"
+by (metis AR_homeomorphic_AR homeomorphic_sym)
+
+
+proposition ANR_imp_absolute_neighbourhood_extensor:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "ANR S" and contf: "continuous_on T f" and "f ` T \<subseteq> S"
+      and cloUT: "closedin (subtopology euclidean U) T"
+  obtains V g where "T \<subseteq> V" "openin (subtopology euclidean U) V"
+                    "continuous_on V g"
+                    "g ` V \<subseteq> S" "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
+proof -
+  have "aff_dim S < int (DIM('b \<times> real))"
+    using aff_dim_le_DIM [of S] by simp
+  then obtain C and S' :: "('b * real) set"
+          where C: "convex C" "C \<noteq> {}"
+            and cloCS: "closedin (subtopology euclidean C) S'"
+            and hom: "S homeomorphic S'"
+    by (metis that homeomorphic_closedin_convex)
+  then obtain D where opD: "openin (subtopology euclidean C) D" and "S' retract_of D"
+    using \<open>ANR S\<close> by (auto simp: ANR_def)
+  then obtain r where "S' \<subseteq> D" and contr: "continuous_on D r"
+                  and "r ` D \<subseteq> S'" and rid: "\<And>x. x \<in> S' \<Longrightarrow> r x = x"
+    by (auto simp: retraction_def retract_of_def)
+  obtain g h where homgh: "homeomorphism S S' g h"
+    using hom by (force simp: homeomorphic_def)
+  have "continuous_on (f ` T) g"
+    by (meson \<open>f ` T \<subseteq> S\<close> continuous_on_subset homeomorphism_def homgh)
+  then have contgf: "continuous_on T (g o f)"
+    by (intro continuous_on_compose contf)
+  have gfTC: "(g \<circ> f) ` T \<subseteq> C"
+  proof -
+    have "g ` S = S'"
+      by (metis (no_types) homeomorphism_def homgh)
+    then show ?thesis
+      by (metis (no_types) assms(3) cloCS closedin_def image_comp image_mono order.trans topspace_euclidean_subtopology)
+  qed
+  obtain f' where contf': "continuous_on U f'"
+              and "f' ` U \<subseteq> C"
+              and eq: "\<And>x. x \<in> T \<Longrightarrow> f' x = (g \<circ> f) x"
+    by (metis Dugundji [OF C cloUT contgf gfTC])
+  show ?thesis
+  proof (rule_tac V = "{x \<in> U. f' x \<in> D}" and g = "h o r o f'" in that)
+    show "T \<subseteq> {x \<in> U. f' x \<in> D}"
+      using cloUT closedin_imp_subset \<open>S' \<subseteq> D\<close> \<open>f ` T \<subseteq> S\<close> eq homeomorphism_image1 homgh
+      by fastforce
+    show ope: "openin (subtopology euclidean U) {x \<in> U. f' x \<in> D}"
+      using  \<open>f' ` U \<subseteq> C\<close> by (auto simp: opD contf' continuous_openin_preimage)
+    have conth: "continuous_on (r ` f' ` {x \<in> U. f' x \<in> D}) h"
+      apply (rule continuous_on_subset [of S'])
+      using homeomorphism_def homgh apply blast
+      using \<open>r ` D \<subseteq> S'\<close> by blast
+    show "continuous_on {x \<in> U. f' x \<in> D} (h \<circ> r \<circ> f')"
+      apply (intro continuous_on_compose conth
+                   continuous_on_subset [OF contr] continuous_on_subset [OF contf'], auto)
+      done
+    show "(h \<circ> r \<circ> f') ` {x \<in> U. f' x \<in> D} \<subseteq> S"
+      using \<open>homeomorphism S S' g h\<close>  \<open>f' ` U \<subseteq> C\<close>  \<open>r ` D \<subseteq> S'\<close>
+      by (auto simp: homeomorphism_def)
+    show "\<And>x. x \<in> T \<Longrightarrow> (h \<circ> r \<circ> f') x = f x"
+      using \<open>homeomorphism S S' g h\<close> \<open>f ` T \<subseteq> S\<close> eq
+      by (auto simp: rid homeomorphism_def)
+  qed
+qed
+
+
+corollary ANR_imp_absolute_neighbourhood_retract:
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  assumes "ANR S" "S homeomorphic S'"
+      and clo: "closedin (subtopology euclidean U) S'"
+  obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
+proof -
+  obtain g h where hom: "homeomorphism S S' g h"
+    using assms by (force simp: homeomorphic_def)
+  have h: "continuous_on S' h" " h ` S' \<subseteq> S"
+    using hom homeomorphism_def apply blast
+    apply (metis hom equalityE homeomorphism_def)
+    done
+    from ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo]
+  obtain V h' where "S' \<subseteq> V" and opUV: "openin (subtopology euclidean U) V"
+                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
+                and h'h:"\<And>x. x \<in> S' \<Longrightarrow> h' x = h x"
+    by (blast intro: ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> h clo])
+  have "S' retract_of V"
+  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>S' \<subseteq> V\<close>)
+    show "continuous_on V (g o h')"
+      apply (intro continuous_on_compose h')
+      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
+      done
+    show "(g \<circ> h') ` V \<subseteq> S'"
+      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
+    show "\<forall>x\<in>S'. (g \<circ> h') x = x"
+      by clarsimp (metis h'h hom homeomorphism_def)
+  qed
+  then show ?thesis
+    by (rule that [OF opUV])
+qed
+
+corollary ANR_imp_absolute_neighbourhood_retract_UNIV:
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  assumes "ANR S" and hom: "S homeomorphic S'" and clo: "closed S'"
+  obtains V where "open V" "S' retract_of V"
+  using ANR_imp_absolute_neighbourhood_retract [OF \<open>ANR S\<close> hom]
+by (metis clo closed_closedin open_openin subtopology_UNIV)
+
+lemma absolute_neighbourhood_extensor_imp_ANR:
+  fixes S :: "'a::euclidean_space set"
+  assumes "\<And>f :: 'a * real \<Rightarrow> 'a.
+           \<And>U T. \<lbrakk>continuous_on T f;  f ` T \<subseteq> S;
+                  closedin (subtopology euclidean U) T\<rbrakk>
+                 \<Longrightarrow> \<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
+                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)"
+  shows "ANR S"
+proof (clarsimp simp: ANR_def)
+  fix U and T :: "('a * real) set"
+  assume "S homeomorphic T" and clo: "closedin (subtopology euclidean U) T"
+  then obtain g h where hom: "homeomorphism S T g h"
+    by (force simp: homeomorphic_def)
+  have h: "continuous_on T h" " h ` T \<subseteq> S"
+    using hom homeomorphism_def apply blast
+    apply (metis hom equalityE homeomorphism_def)
+    done
+  obtain V h' where "T \<subseteq> V" and opV: "openin (subtopology euclidean U) V"
+                and h': "continuous_on V h'" "h' ` V \<subseteq> S"
+              and h'h: "\<forall>x\<in>T. h' x = h x"
+    using assms [OF h clo] by blast
+  have [simp]: "T \<subseteq> U"
+    using clo closedin_imp_subset by auto
+  have "T retract_of V"
+  proof (simp add: retraction_def retract_of_def, intro exI conjI \<open>T \<subseteq> V\<close>)
+    show "continuous_on V (g o h')"
+      apply (intro continuous_on_compose h')
+      apply (meson hom continuous_on_subset h' homeomorphism_cont1)
+      done
+    show "(g \<circ> h') ` V \<subseteq> T"
+      using h'  by clarsimp (metis hom subsetD homeomorphism_def imageI)
+    show "\<forall>x\<in>T. (g \<circ> h') x = x"
+      by clarsimp (metis h'h hom homeomorphism_def)
+  qed
+  then show "\<exists>V. openin (subtopology euclidean U) V \<and> T retract_of V"
+    using opV by blast
+qed
+
+lemma ANR_eq_absolute_neighbourhood_extensor:
+  fixes S :: "'a::euclidean_space set"
+  shows "ANR S \<longleftrightarrow>
+         (\<forall>f :: 'a * real \<Rightarrow> 'a.
+          \<forall>U T. continuous_on T f \<longrightarrow> f ` T \<subseteq> S \<longrightarrow>
+                closedin (subtopology euclidean U) T \<longrightarrow>
+               (\<exists>V g. T \<subseteq> V \<and> openin (subtopology euclidean U) V \<and>
+                       continuous_on V g \<and> g ` V \<subseteq> S \<and> (\<forall>x \<in> T. g x = f x)))"
+apply (rule iffI)
+ apply (metis ANR_imp_absolute_neighbourhood_extensor)
+apply (simp add: absolute_neighbourhood_extensor_imp_ANR)
+done
+
+lemma ANR_imp_neighbourhood_retract:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ANR S" "closedin (subtopology euclidean U) S"
+  obtains V where "openin (subtopology euclidean 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 (subtopology euclidean U) S'"
+  obtains V W
+    where "openin (subtopology euclidean U) V"
+          "closedin (subtopology euclidean U) W"
+          "S' \<subseteq> V" "V \<subseteq> W" "S' retract_of W"
+proof -
+  obtain Z where "openin (subtopology euclidean U) Z" and S'Z: "S' retract_of Z"
+    by (blast intro: assms ANR_imp_absolute_neighbourhood_retract)
+  then have UUZ: "closedin (subtopology euclidean U) (U - Z)"
+    by auto
+  have "S' \<inter> (U - Z) = {}"
+    using \<open>S' retract_of Z\<close> closedin_retract closedin_subtopology by fastforce
+  then obtain V W
+      where "openin (subtopology euclidean U) V"
+        and "openin (subtopology euclidean U) W"
+        and "S' \<subseteq> V" "U - Z \<subseteq> W" "V \<inter> W = {}"
+      using separation_normal_local [OF US' UUZ]  by auto
+  moreover have "S' retract_of U - W"
+    apply (rule retract_of_subset [OF S'Z])
+    using US' \<open>S' \<subseteq> V\<close> \<open>V \<inter> W = {}\<close> closedin_subset apply fastforce
+    using Diff_subset_conv \<open>U - Z \<subseteq> W\<close> by blast
+  ultimately show ?thesis
+    apply (rule_tac V=V and W = "U-W" in that)
+    using openin_imp_subset apply (force simp:)+
+    done
+qed
+
+lemma ANR_imp_closed_neighbourhood_retract:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ANR S" "closedin (subtopology euclidean U) S"
+  obtains V W where "openin (subtopology euclidean U) V"
+                    "closedin (subtopology euclidean U) W"
+                    "S \<subseteq> V" "V \<subseteq> W" "S retract_of W"
+by (meson ANR_imp_absolute_closed_neighbourhood_retract assms homeomorphic_refl)
+
+lemma ANR_homeomorphic_ANR:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "ANR T" "S homeomorphic T"
+    shows "ANR S"
+unfolding ANR_def
+by (metis assms ANR_imp_absolute_neighbourhood_retract homeomorphic_trans [of _ S] homeomorphic_sym)
+
+lemma homeomorphic_ANR_iff_ANR:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
+by (metis ANR_homeomorphic_ANR homeomorphic_sym)
+
+subsection\<open> Analogous properties of ENRs.\<close>
+
+proposition ENR_imp_absolute_neighbourhood_retract:
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  assumes "ENR S" and hom: "S homeomorphic S'"
+      and "S' \<subseteq> U"
+  obtains V where "openin (subtopology euclidean U) V" "S' retract_of V"
+proof -
+  obtain X where "open X" "S retract_of X"
+    using \<open>ENR S\<close> by (auto simp: ENR_def)
+  then obtain r where "retraction X S r"
+    by (auto simp: retract_of_def)
+  have "locally compact S'"
+    using retract_of_locally_compact open_imp_locally_compact
+          homeomorphic_local_compactness \<open>S retract_of X\<close> \<open>open X\<close> hom by blast
+  then obtain W where UW: "openin (subtopology euclidean U) W"
+                  and WS': "closedin (subtopology euclidean W) S'"
+    apply (rule locally_compact_closedin_open)
+    apply (rename_tac W)
+    apply (rule_tac W = "U \<inter> W" in that, blast)
+    by (simp add: \<open>S' \<subseteq> U\<close> closedin_limpt)
+  obtain f g where hom: "homeomorphism S S' f g"
+    using assms by (force simp: homeomorphic_def)
+  have contg: "continuous_on S' g"
+    using hom homeomorphism_def by blast
+  moreover have "g ` S' \<subseteq> S" by (metis hom equalityE homeomorphism_def)
+  ultimately obtain h where conth: "continuous_on W h" and hg: "\<And>x. x \<in> S' \<Longrightarrow> h x = g x"
+    using Tietze_unbounded [of S' g W] WS' by blast
+  have "W \<subseteq> U" using UW openin_open by auto
+  have "S' \<subseteq> W" using WS' closedin_closed by auto
+  have him: "\<And>x. x \<in> S' \<Longrightarrow> h x \<in> X"
+    by (metis (no_types) \<open>S retract_of X\<close> hg hom homeomorphism_def image_insert insert_absorb insert_iff retract_of_imp_subset subset_eq)
+  have "S' retract_of {x \<in> W. h x \<in> X}"
+  proof (simp add: retraction_def retract_of_def, intro exI conjI)
+    show "S' \<subseteq> {x \<in> W. h x \<in> X}"
+      using him WS' closedin_imp_subset by blast
+    show "continuous_on {x \<in> W. h x \<in> X} (f o r o h)"
+    proof (intro continuous_on_compose)
+      show "continuous_on {x \<in> W. h x \<in> X} h"
+        by (metis (no_types) Collect_restrict conth continuous_on_subset)
+      show "continuous_on (h ` {x \<in> W. h x \<in> X}) r"
+      proof -
+        have "h ` {b \<in> W. h b \<in> X} \<subseteq> X"
+          by blast
+        then show "continuous_on (h ` {b \<in> W. h b \<in> X}) r"
+          by (meson \<open>retraction X S r\<close> continuous_on_subset retraction)
+      qed
+      show "continuous_on (r ` h ` {x \<in> W. h x \<in> X}) f"
+        apply (rule continuous_on_subset [of S])
+         using hom homeomorphism_def apply blast
+        apply clarify
+        apply (meson \<open>retraction X S r\<close> subsetD imageI retraction_def)
+        done
+    qed
+    show "(f \<circ> r \<circ> h) ` {x \<in> W. h x \<in> X} \<subseteq> S'"
+      using \<open>retraction X S r\<close> hom
+      by (auto simp: retraction_def homeomorphism_def)
+    show "\<forall>x\<in>S'. (f \<circ> r \<circ> h) x = x"
+      using \<open>retraction X S r\<close> hom by (auto simp: retraction_def homeomorphism_def hg)
+  qed
+  then show ?thesis
+    apply (rule_tac V = "{x. x \<in> W \<and> h x \<in> X}" in that)
+     apply (rule openin_trans [OF _ UW])
+     using \<open>continuous_on W h\<close> \<open>open X\<close> continuous_openin_preimage_eq apply blast+
+     done
+qed
+
+corollary ENR_imp_absolute_neighbourhood_retract_UNIV:
+  fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
+  assumes "ENR S" "S homeomorphic S'"
+  obtains T' where "open T'" "S' retract_of T'"
+by (metis ENR_imp_absolute_neighbourhood_retract UNIV_I assms(1) assms(2) open_openin subsetI subtopology_UNIV)
+
+lemma ENR_homeomorphic_ENR:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "ENR T" "S homeomorphic T"
+    shows "ENR S"
+unfolding ENR_def
+by (meson ENR_imp_absolute_neighbourhood_retract_UNIV assms homeomorphic_sym)
+
+lemma homeomorphic_ENR_iff_ENR:
+  fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+  assumes "S homeomorphic T"
+    shows "ENR S \<longleftrightarrow> ENR T"
+by (meson ENR_homeomorphic_ENR assms homeomorphic_sym)
+
+lemma ENR_translation:
+  fixes S :: "'a::euclidean_space set"
+  shows "ENR(image (\<lambda>x. a + x) S) \<longleftrightarrow> ENR S"
+by (meson homeomorphic_sym homeomorphic_translation homeomorphic_ENR_iff_ENR)
+
+lemma ENR_linear_image_eq:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "inj f"
+  shows "ENR (image f S) \<longleftrightarrow> ENR S"
+apply (rule homeomorphic_ENR_iff_ENR)
+using assms homeomorphic_sym linear_homeomorphic_image by auto
+
+subsection\<open>Some relations among the concepts\<close>
+
+text\<open>We also relate AR to being a retract of UNIV, which is often a more convenient proxy in the closed case.\<close>
+
+lemma AR_imp_ANR: "AR S \<Longrightarrow> ANR S"
+  using ANR_def AR_def by fastforce
+
+lemma ENR_imp_ANR:
+  fixes S :: "'a::euclidean_space set"
+  shows "ENR S \<Longrightarrow> ANR S"
+apply (simp add: ANR_def)
+by (metis ENR_imp_absolute_neighbourhood_retract closedin_imp_subset)
+
+lemma ENR_ANR:
+  fixes S :: "'a::euclidean_space set"
+  shows "ENR S \<longleftrightarrow> ANR S \<and> locally compact S"
+proof
+  assume "ENR S"
+  then have "locally compact S"
+    using ENR_def open_imp_locally_compact retract_of_locally_compact by auto
+  then show "ANR S \<and> locally compact S"
+    using ENR_imp_ANR \<open>ENR S\<close> by blast
+next
+  assume "ANR S \<and> locally compact S"
+  then have "ANR S" "locally compact S" by auto
+  then obtain T :: "('a * real) set" where "closed T" "S homeomorphic T"
+    using locally_compact_homeomorphic_closed
+    by (metis DIM_prod DIM_real Suc_eq_plus1 lessI)
+  then show "ENR S"
+    using \<open>ANR S\<close>
+    apply (simp add: ANR_def)
+    apply (drule_tac x=UNIV in spec)
+    apply (drule_tac x=T in spec)
+    apply (auto simp: closed_closedin)
+    apply (meson ENR_def ENR_homeomorphic_ENR open_openin)
+    done
+qed
+
+
+proposition AR_ANR:
+  fixes S :: "'a::euclidean_space set"
+  shows "AR S \<longleftrightarrow> ANR S \<and> contractible S \<and> S \<noteq> {}"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  obtain C and S' :: "('a * real) set"
+    where "convex C" "C \<noteq> {}" "closedin (subtopology euclidean C) S'" "S homeomorphic S'"
+      apply (rule homeomorphic_closedin_convex [of S, where 'n = "'a * real"])
+      using aff_dim_le_DIM [of S] by auto
+  with \<open>AR S\<close> have "contractible S"
+    apply (simp add: AR_def)
+    apply (drule_tac x=C in spec)
+    apply (drule_tac x="S'" in spec, simp)
+    using convex_imp_contractible homeomorphic_contractible_eq retract_of_contractible by fastforce
+  with \<open>AR S\<close> show ?rhs
+    apply (auto simp: AR_imp_ANR)
+    apply (force simp: AR_def)
+    done
+next
+  assume ?rhs
+  then obtain a and h:: "real \<times> 'a \<Rightarrow> 'a"
+      where conth: "continuous_on ({0..1} \<times> S) h"
+        and hS: "h ` ({0..1} \<times> S) \<subseteq> S"
+        and [simp]: "\<And>x. h(0, x) = x"
+        and [simp]: "\<And>x. h(1, x) = a"
+        and "ANR S" "S \<noteq> {}"
+    by (auto simp: contractible_def homotopic_with_def)
+  then have "a \<in> S"
+    by (metis all_not_in_conv atLeastAtMost_iff image_subset_iff mem_Sigma_iff order_refl zero_le_one)
+  have "\<exists>g. continuous_on W g \<and> g ` W \<subseteq> S \<and> (\<forall>x\<in>T. g x = f x)"
+         if      f: "continuous_on T f" "f ` T \<subseteq> S"
+            and WT: "closedin (subtopology euclidean W) T"
+         for W T and f :: "'a \<times> real \<Rightarrow> 'a"
+  proof -
+    obtain U g
+      where "T \<subseteq> U" and WU: "openin (subtopology euclidean W) U"
+        and contg: "continuous_on U g"
+        and "g ` U \<subseteq> S" and gf: "\<And>x. x \<in> T \<Longrightarrow> g x = f x"
+      using iffD1 [OF ANR_eq_absolute_neighbourhood_extensor \<open>ANR S\<close>, rule_format, OF f WT]
+      by auto
+    have WWU: "closedin (subtopology euclidean W) (W - U)"
+      using WU closedin_diff by fastforce
+    moreover have "(W - U) \<inter> T = {}"
+      using \<open>T \<subseteq> U\<close> by auto
+    ultimately obtain V V'
+      where WV': "openin (subtopology euclidean W) V'"
+        and WV: "openin (subtopology euclidean W) V"
+        and "W - U \<subseteq> V'" "T \<subseteq> V" "V' \<inter> V = {}"
+      using separation_normal_local [of W "W-U" T] WT by blast
+    then have WVT: "T \<inter> (W - V) = {}"
+      by auto
+    have WWV: "closedin (subtopology euclidean W) (W - V)"
+      using WV closedin_diff by fastforce
+    obtain j :: " 'a \<times> real \<Rightarrow> real"
+      where contj: "continuous_on W j"
+        and j:  "\<And>x. x \<in> W \<Longrightarrow> j x \<in> {0..1}"
+        and j0: "\<And>x. x \<in> W - V \<Longrightarrow> j x = 1"
+        and j1: "\<And>x. x \<in> T \<Longrightarrow> j x = 0"
+      by (rule Urysohn_local [OF WT WWV WVT, of 0 "1::real"]) (auto simp: in_segment)
+    have Weq: "W = (W - V) \<union> (W - V')"
+      using \<open>V' \<inter> V = {}\<close> by force
+    show ?thesis
+    proof (intro conjI exI)
+      have *: "continuous_on (W - V') (\<lambda>x. h (j x, g x))"
+        apply (rule continuous_on_compose2 [OF conth continuous_on_Pair])
+          apply (rule continuous_on_subset [OF contj Diff_subset])
+         apply (rule continuous_on_subset [OF contg])
+         apply (metis Diff_subset_conv Un_commute \<open>W - U \<subseteq> V'\<close>)
+        using j \<open>g ` U \<subseteq> S\<close> \<open>W - U \<subseteq> V'\<close> apply fastforce
+        done
+      show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
+        apply (subst Weq)
+        apply (rule continuous_on_cases_local)
+            apply (simp_all add: Weq [symmetric] WWV continuous_on_const *)
+          using WV' closedin_diff apply fastforce
+         apply (auto simp: j0 j1)
+        done
+    next
+      have "h (j (x, y), g (x, y)) \<in> S" if "(x, y) \<in> W" "(x, y) \<in> V" for x y
+      proof -
+        have "j(x, y) \<in> {0..1}"
+          using j that by blast
+        moreover have "g(x, y) \<in> S"
+          using \<open>V' \<inter> V = {}\<close> \<open>W - U \<subseteq> V'\<close> \<open>g ` U \<subseteq> S\<close> that by fastforce
+        ultimately show ?thesis
+          using hS by blast
+      qed
+      with \<open>a \<in> S\<close> \<open>g ` U \<subseteq> S\<close>
+      show "(\<lambda>x. if x \<in> W - V then a else h (j x, g x)) ` W \<subseteq> S"
+        by auto
+    next
+      show "\<forall>x\<in>T. (if x \<in> W - V then a else h (j x, g x)) = f x"
+        using \<open>T \<subseteq> V\<close> by (auto simp: j0 j1 gf)
+    qed
+  qed
+  then show ?lhs
+    by (simp add: AR_eq_absolute_extensor)
+qed
+
+
+lemma ANR_retract_of_ANR:
+  fixes S :: "'a::euclidean_space set"
+  assumes "ANR T" "S retract_of T"
+  shows "ANR S"
+using assms
+apply (simp add: ANR_eq_absolute_neighbourhood_extensor retract_of_def retraction_def)
+apply (clarsimp elim!: all_forward)
+apply (erule impCE, metis subset_trans)
+apply (clarsimp elim!: ex_forward)
+apply (rule_tac x="r o g" in exI)
+by (metis comp_apply continuous_on_compose continuous_on_subset subsetD imageI image_comp image_mono subset_trans)
+
+lemma AR_retract_of_AR:
+  fixes S :: "'a::euclidean_space set"
+  shows "\<lbrakk>AR T; S retract_of T\<rbrakk> \<Longrightarrow> AR S"
+using ANR_retract_of_ANR AR_ANR retract_of_contractible by fastforce
+
+lemma ENR_retract_of_ENR:
+   "\<lbrakk>ENR T; S retract_of T\<rbrakk> \<Longrightarrow> ENR S"
+by (meson ENR_def retract_of_trans)
+
+lemma retract_of_UNIV:
+  fixes S :: "'a::euclidean_space set"
+  shows "S retract_of UNIV \<longleftrightarrow> AR S \<and> 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 [simp]:
+  fixes S :: "'a::euclidean_space set"
+  shows "compact S \<and> AR S \<longleftrightarrow> compact S \<and> S retract_of UNIV"
+using compact_imp_closed retract_of_UNIV by blast
+
+subsection\<open>More properties of ARs, ANRs and ENRs\<close>
+
+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 "\<lbrakk>convex S; S \<noteq> {}\<rbrakk> \<Longrightarrow> AR S"
+apply (rule absolute_extensor_imp_AR)
+apply (rule Dugundji, assumption+)
+by blast
+
+lemma convex_imp_ANR:
+  fixes S :: "'a::euclidean_space set"
+  shows "convex S \<Longrightarrow> ANR S"
+using ANR_empty AR_imp_ANR convex_imp_AR by blast
+
+lemma ENR_convex_closed:
+  fixes S :: "'a::euclidean_space set"
+  shows "\<lbrakk>closed S; convex S\<rbrakk> \<Longrightarrow> 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
+
+subsection\<open>ARs closed under union\<close>
+
+lemma AR_closed_Un_local_aux:
+  fixes U :: "'a::euclidean_space set"
+  assumes "closedin (subtopology euclidean U) S"
+          "closedin (subtopology euclidean U) T"
+          "AR S" "AR T" "AR(S \<inter> T)"
+  shows "(S \<union> T) retract_of U"
+proof -
+  have "S \<inter> T \<noteq> {}"
+    using assms AR_def by fastforce
+  have "S \<subseteq> U" "T \<subseteq> U"
+    using assms by (auto simp: closedin_imp_subset)
+  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
+  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
+  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
+  have US': "closedin (subtopology euclidean U) S'"
+    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
+    by (simp add: S'_def continuous_intros)
+  have UT': "closedin (subtopology euclidean U) T'"
+    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
+    by (simp add: T'_def continuous_intros)
+  have "S \<subseteq> S'"
+    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
+  have "T \<subseteq> T'"
+    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
+  have "S \<inter> T \<subseteq> W" "W \<subseteq> U"
+    using \<open>S \<subseteq> U\<close> by (auto simp: W_def setdist_sing_in_set)
+  have "(S \<inter> T) retract_of W"
+    apply (rule AR_imp_absolute_retract [OF \<open>AR(S \<inter> T)\<close>])
+     apply (simp add: homeomorphic_refl)
+    apply (rule closedin_subset_trans [of U])
+    apply (simp_all add: assms closedin_Int \<open>S \<inter> T \<subseteq> W\<close> \<open>W \<subseteq> U\<close>)
+    done
+  then obtain r0
+    where "S \<inter> T \<subseteq> W" and contr0: "continuous_on W r0"
+      and "r0 ` W \<subseteq> S \<inter> T"
+      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
+      by (auto simp: retract_of_def retraction_def)
+  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
+    using setdist_eq_0_closedin \<open>S \<inter> T \<noteq> {}\<close> assms
+    by (force simp: W_def setdist_sing_in_set)
+  have "S' \<inter> T' = W"
+    by (auto simp: S'_def T'_def W_def)
+  then have cloUW: "closedin (subtopology euclidean U) W"
+    using closedin_Int US' UT' by blast
+  define r where "r \<equiv> \<lambda>x. if x \<in> W then r0 x else x"
+  have "r ` (W \<union> S) \<subseteq> S" "r ` (W \<union> T) \<subseteq> T"
+    using \<open>r0 ` W \<subseteq> S \<inter> T\<close> r_def by auto
+  have contr: "continuous_on (W \<union> (S \<union> T)) r"
+  unfolding r_def
+  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
+    show "closedin (subtopology euclidean (W \<union> (S \<union> T))) W"
+      using \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> \<open>closedin (subtopology euclidean U) W\<close> closedin_subset_trans by fastforce
+    show "closedin (subtopology euclidean (W \<union> (S \<union> T))) (S \<union> T)"
+      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
+    show "\<And>x. x \<in> W \<and> x \<notin> W \<or> x \<in> S \<union> T \<and> x \<in> W \<Longrightarrow> r0 x = x"
+      by (auto simp: ST)
+  qed
+  have cloUWS: "closedin (subtopology euclidean U) (W \<union> S)"
+    by (simp add: cloUW assms closedin_Un)
+  obtain g where contg: "continuous_on U g"
+             and "g ` U \<subseteq> S" and geqr: "\<And>x. x \<in> W \<union> S \<Longrightarrow> g x = r x"
+    apply (rule AR_imp_absolute_extensor [OF \<open>AR S\<close> _ _ cloUWS])
+      apply (rule continuous_on_subset [OF contr])
+      using \<open>r ` (W \<union> S) \<subseteq> S\<close> apply auto
+    done
+  have cloUWT: "closedin (subtopology euclidean U) (W \<union> T)"
+    by (simp add: cloUW assms closedin_Un)
+  obtain h where conth: "continuous_on U h"
+             and "h ` U \<subseteq> T" and heqr: "\<And>x. x \<in> W \<union> T \<Longrightarrow> h x = r x"
+    apply (rule AR_imp_absolute_extensor [OF \<open>AR T\<close> _ _ cloUWT])
+      apply (rule continuous_on_subset [OF contr])
+      using \<open>r ` (W \<union> T) \<subseteq> T\<close> apply auto
+    done
+  have "U = S' \<union> T'"
+    by (force simp: S'_def T'_def)
+  then have cont: "continuous_on U (\<lambda>x. if x \<in> S' then g x else h x)"
+    apply (rule ssubst)
+    apply (rule continuous_on_cases_local)
+    using US' UT' \<open>S' \<inter> T' = W\<close> \<open>U = S' \<union> T'\<close>
+          contg conth continuous_on_subset geqr heqr apply auto
+    done
+  have UST: "(\<lambda>x. if x \<in> S' then g x else h x) ` U \<subseteq> S \<union> T"
+    using \<open>g ` U \<subseteq> S\<close> \<open>h ` U \<subseteq> T\<close> by auto
+  show ?thesis
+    apply (simp add: retract_of_def retraction_def \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close>)
+    apply (rule_tac x="\<lambda>x. if x \<in> S' then g x else h x" in exI)
+    apply (intro conjI cont UST)
+    by (metis IntI ST Un_iff \<open>S \<subseteq> S'\<close> \<open>S' \<inter> T' = W\<close> \<open>T \<subseteq> T'\<close> subsetD geqr heqr r0 r_def)
+qed
+
+
+proposition AR_closed_Un_local:
+  fixes S :: "'a::euclidean_space set"
+  assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
+      and STT: "closedin (subtopology euclidean (S \<union> T)) T"
+      and "AR S" "AR T" "AR(S \<inter> T)"
+    shows "AR(S \<union> T)"
+proof -
+  have "C retract_of U"
+       if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
+       for U and C :: "('a * real) set"
+  proof -
+    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
+      using hom by (force simp: homeomorphic_def)
+    have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
+      apply (rule closedin_trans [OF _ UC])
+      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
+      using hom homeomorphism_def apply blast
+      apply (metis hom homeomorphism_def set_eq_subset)
+      done
+    have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
+      apply (rule closedin_trans [OF _ UC])
+      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
+      using hom homeomorphism_def apply blast
+      apply (metis hom homeomorphism_def set_eq_subset)
+      done
+    have ARS: "AR {x \<in> C. g x \<in> S}"
+      apply (rule AR_homeomorphic_AR [OF \<open>AR S\<close>])
+      apply (simp add: homeomorphic_def)
+      apply (rule_tac x=g in exI)
+      apply (rule_tac x=f in exI)
+      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+      apply (rule_tac x="f x" in image_eqI, auto)
+      done
+    have ART: "AR {x \<in> C. g x \<in> T}"
+      apply (rule AR_homeomorphic_AR [OF \<open>AR T\<close>])
+      apply (simp add: homeomorphic_def)
+      apply (rule_tac x=g in exI)
+      apply (rule_tac x=f in exI)
+      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+      apply (rule_tac x="f x" in image_eqI, auto)
+      done
+    have ARI: "AR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
+      apply (rule AR_homeomorphic_AR [OF \<open>AR (S \<inter> T)\<close>])
+      apply (simp add: homeomorphic_def)
+      apply (rule_tac x=g in exI)
+      apply (rule_tac x=f in exI)
+      using hom
+      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+      apply (rule_tac x="f x" in image_eqI, auto)
+      done
+    have "C = {x \<in> C. g x \<in> S} \<union> {x \<in> C. g x \<in> 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 "\<lbrakk>closed S; closed T; AR S; AR T; AR (S \<inter> T)\<rbrakk> \<Longrightarrow> AR (S \<union> T)"
+by (metis AR_closed_Un_local_aux closed_closedin retract_of_UNIV subtopology_UNIV)
+
+subsection\<open>ANRs closed under union\<close>
+
+lemma ANR_closed_Un_local_aux:
+  fixes U :: "'a::euclidean_space set"
+  assumes US: "closedin (subtopology euclidean U) S"
+      and UT: "closedin (subtopology euclidean U) T"
+      and "ANR S" "ANR T" "ANR(S \<inter> T)"
+  obtains V where "openin (subtopology euclidean U) V" "(S \<union> T) retract_of V"
+proof (cases "S = {} \<or> T = {}")
+  case True with assms that show ?thesis
+    by (auto simp: intro: ANR_imp_neighbourhood_retract)
+next
+  case False
+  then have [simp]: "S \<noteq> {}" "T \<noteq> {}" by auto
+  have "S \<subseteq> U" "T \<subseteq> U"
+    using assms by (auto simp: closedin_imp_subset)
+  define S' where "S' \<equiv> {x \<in> U. setdist {x} S \<le> setdist {x} T}"
+  define T' where "T' \<equiv> {x \<in> U. setdist {x} T \<le> setdist {x} S}"
+  define W  where "W \<equiv> {x \<in> U. setdist {x} S = setdist {x} T}"
+  have cloUS': "closedin (subtopology euclidean U) S'"
+    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} S - setdist {x} T" "{..0}"]
+    by (simp add: S'_def continuous_intros)
+  have cloUT': "closedin (subtopology euclidean U) T'"
+    using continuous_closedin_preimage [of U "\<lambda>x. setdist {x} T - setdist {x} S" "{..0}"]
+    by (simp add: T'_def continuous_intros)
+  have "S \<subseteq> S'"
+    using S'_def \<open>S \<subseteq> U\<close> setdist_sing_in_set by fastforce
+  have "T \<subseteq> T'"
+    using T'_def \<open>T \<subseteq> U\<close> setdist_sing_in_set by fastforce
+  have "S' \<union> T' = U"
+    by (auto simp: S'_def T'_def)
+  have "W \<subseteq> S'"
+    by (simp add: Collect_mono S'_def W_def)
+  have "W \<subseteq> T'"
+    by (simp add: Collect_mono T'_def W_def)
+  have ST_W: "S \<inter> T \<subseteq> W" and "W \<subseteq> U"
+    using \<open>S \<subseteq> U\<close> by (force simp: W_def setdist_sing_in_set)+
+  have "S' \<inter> T' = W"
+    by (auto simp: S'_def T'_def W_def)
+  then have cloUW: "closedin (subtopology euclidean U) W"
+    using closedin_Int cloUS' cloUT' by blast
+  obtain W' W0 where "openin (subtopology euclidean W) W'"
+                 and cloWW0: "closedin (subtopology euclidean W) W0"
+                 and "S \<inter> T \<subseteq> W'" "W' \<subseteq> W0"
+                 and ret: "(S \<inter> T) retract_of W0"
+    apply (rule ANR_imp_closed_neighbourhood_retract [OF \<open>ANR(S \<inter> T)\<close>])
+    apply (rule closedin_subset_trans [of U, OF _ ST_W \<open>W \<subseteq> U\<close>])
+    apply (blast intro: assms)+
+    done
+  then obtain U0 where opeUU0: "openin (subtopology euclidean U) U0"
+                   and U0: "S \<inter> T \<subseteq> U0" "U0 \<inter> W \<subseteq> W0"
+    unfolding openin_open  using \<open>W \<subseteq> U\<close> by blast
+  have "W0 \<subseteq> U"
+    using \<open>W \<subseteq> U\<close> cloWW0 closedin_subset by fastforce
+  obtain r0
+    where "S \<inter> T \<subseteq> W0" and contr0: "continuous_on W0 r0" and "r0 ` W0 \<subseteq> S \<inter> T"
+      and r0 [simp]: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> r0 x = x"
+    using ret  by (force simp add: retract_of_def retraction_def)
+  have ST: "x \<in> W \<Longrightarrow> x \<in> S \<longleftrightarrow> x \<in> T" for x
+    using assms by (auto simp: W_def setdist_sing_in_set dest!: setdist_eq_0_closedin)
+  define r where "r \<equiv> \<lambda>x. if x \<in> W0 then r0 x else x"
+  have "r ` (W0 \<union> S) \<subseteq> S" "r ` (W0 \<union> T) \<subseteq> T"
+    using \<open>r0 ` W0 \<subseteq> S \<inter> T\<close> r_def by auto
+  have contr: "continuous_on (W0 \<union> (S \<union> T)) r"
+  unfolding r_def
+  proof (rule continuous_on_cases_local [OF _ _ contr0 continuous_on_id])
+    show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) W0"
+      apply (rule closedin_subset_trans [of U])
+      using cloWW0 cloUW closedin_trans \<open>W0 \<subseteq> U\<close> \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> apply blast+
+      done
+    show "closedin (subtopology euclidean (W0 \<union> (S \<union> T))) (S \<union> T)"
+      by (meson \<open>S \<subseteq> U\<close> \<open>T \<subseteq> U\<close> \<open>W0 \<subseteq> U\<close> assms closedin_Un closedin_subset_trans sup.bounded_iff sup.cobounded2)
+    show "\<And>x. x \<in> W0 \<and> x \<notin> W0 \<or> x \<in> S \<union> T \<and> x \<in> W0 \<Longrightarrow> r0 x = x"
+      using ST cloWW0 closedin_subset by fastforce
+  qed
+  have cloS'WS: "closedin (subtopology euclidean S') (W0 \<union> S)"
+    by (meson closedin_subset_trans US cloUS' \<open>S \<subseteq> S'\<close> \<open>W \<subseteq> S'\<close> cloUW cloWW0 
+              closedin_Un closedin_imp_subset closedin_trans)
+  obtain W1 g where "W0 \<union> S \<subseteq> W1" and contg: "continuous_on W1 g"
+                and opeSW1: "openin (subtopology euclidean S') W1"
+                and "g ` W1 \<subseteq> S" and geqr: "\<And>x. x \<in> W0 \<union> S \<Longrightarrow> g x = r x"
+    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR S\<close> _ \<open>r ` (W0 \<union> S) \<subseteq> S\<close> cloS'WS])
+     apply (rule continuous_on_subset [OF contr])
+    apply (blast intro:  elim: )+
+    done
+  have cloT'WT: "closedin (subtopology euclidean T') (W0 \<union> T)"
+    by (meson closedin_subset_trans UT cloUT' \<open>T \<subseteq> T'\<close> \<open>W \<subseteq> T'\<close> cloUW cloWW0 
+              closedin_Un closedin_imp_subset closedin_trans)
+  obtain W2 h where "W0 \<union> T \<subseteq> W2" and conth: "continuous_on W2 h"
+                and opeSW2: "openin (subtopology euclidean T') W2"
+                and "h ` W2 \<subseteq> T" and heqr: "\<And>x. x \<in> W0 \<union> T \<Longrightarrow> h x = r x"
+    apply (rule ANR_imp_absolute_neighbourhood_extensor [OF \<open>ANR T\<close> _ \<open>r ` (W0 \<union> T) \<subseteq> T\<close> cloT'WT])
+     apply (rule continuous_on_subset [OF contr])
+    apply (blast intro:  elim: )+
+    done
+  have "S' \<inter> T' = W"
+    by (force simp: S'_def T'_def W_def)
+  obtain O1 O2 where "open O1" "W1 = S' \<inter> O1" "open O2" "W2 = T' \<inter> O2"
+    using opeSW1 opeSW2 by (force simp add: openin_open)
+  show ?thesis
+  proof
+    have eq: "W1 - (W - U0) \<union> (W2 - (W - U0)) =
+         ((U - T') \<inter> O1 \<union> (U - S') \<inter> O2 \<union> U \<inter> O1 \<inter> O2) - (W - U0)"
+     using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close>
+      by (auto simp: \<open>S' \<union> T' = U\<close> [symmetric] \<open>S' \<inter> T' = W\<close> [symmetric] \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close>)
+    show "openin (subtopology euclidean U) (W1 - (W - U0) \<union> (W2 - (W - U0)))"
+      apply (subst eq)
+      apply (intro openin_Un openin_Int_open openin_diff closedin_diff cloUW opeUU0 cloUS' cloUT' \<open>open O1\<close> \<open>open O2\<close>)
+      apply simp_all
+      done
+    have cloW1: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W1 - (W - U0))"
+      using cloUS' apply (simp add: closedin_closed)
+      apply (erule ex_forward)
+      using U0 \<open>W0 \<union> S \<subseteq> W1\<close>
+      apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
+      done
+    have cloW2: "closedin (subtopology euclidean (W1 - (W - U0) \<union> (W2 - (W - U0)))) (W2 - (W - U0))"
+      using cloUT' apply (simp add: closedin_closed)
+      apply (erule ex_forward)
+      using U0 \<open>W0 \<union> T \<subseteq> W2\<close>
+      apply (auto simp add: \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<union> T' = U\<close> [symmetric]\<open>S' \<inter> T' = W\<close> [symmetric])
+      done
+    have *: "\<forall>x\<in>S \<union> T. (if x \<in> S' then g x else h x) = x"
+      using ST \<open>S' \<inter> T' = W\<close> cloT'WT closedin_subset geqr heqr 
+      apply (auto simp: r_def)
+       apply fastforce
+      using \<open>S \<subseteq> S'\<close> \<open>T \<subseteq> T'\<close> \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W1 = S' \<inter> O1\<close>  by auto
+    have "\<exists>r. continuous_on (W1 - (W - U0) \<union> (W2 - (W - U0))) r \<and>
+              r ` (W1 - (W - U0) \<union> (W2 - (W - U0))) \<subseteq> S \<union> T \<and> 
+              (\<forall>x\<in>S \<union> T. r x = x)"
+      apply (rule_tac x = "\<lambda>x. if  x \<in> S' then g x else h x" in exI)
+      apply (intro conjI *)
+      apply (rule continuous_on_cases_local 
+                  [OF cloW1 cloW2 continuous_on_subset [OF contg] continuous_on_subset [OF conth]])
+      using \<open>W1 = S' \<inter> O1\<close> \<open>W2 = T' \<inter> O2\<close> \<open>S' \<inter> T' = W\<close>
+            \<open>g ` W1 \<subseteq> S\<close> \<open>h ` W2 \<subseteq> T\<close> apply auto
+      using \<open>U0 \<inter> W \<subseteq> W0\<close> \<open>W0 \<union> S \<subseteq> W1\<close> apply (fastforce simp add: geqr heqr)+
+      done
+    then show "S \<union> T retract_of W1 - (W - U0) \<union> (W2 - (W - U0))"
+      using  \<open>W0 \<union> S \<subseteq> W1\<close> \<open>W0 \<union> T \<subseteq> W2\<close> ST opeUU0 U0
+      by (auto simp add: retract_of_def retraction_def)
+  qed
+qed
+
+
+proposition ANR_closed_Un_local:
+  fixes S :: "'a::euclidean_space set"
+  assumes STS: "closedin (subtopology euclidean (S \<union> T)) S"
+      and STT: "closedin (subtopology euclidean (S \<union> T)) T"
+      and "ANR S" "ANR T" "ANR(S \<inter> T)" 
+    shows "ANR(S \<union> T)"
+proof -
+  have "\<exists>T. openin (subtopology euclidean U) T \<and> C retract_of T"
+       if hom: "S \<union> T homeomorphic C" and UC: "closedin (subtopology euclidean U) C"
+       for U and C :: "('a * real) set"
+  proof -
+    obtain f g where hom: "homeomorphism (S \<union> T) C f g"
+      using hom by (force simp: homeomorphic_def)
+    have US: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> S}"
+      apply (rule closedin_trans [OF _ UC])
+      apply (rule continuous_closedin_preimage_gen [OF _ _ STS])
+      using hom [unfolded homeomorphism_def] apply blast
+      apply (metis hom homeomorphism_def set_eq_subset)
+      done
+    have UT: "closedin (subtopology euclidean U) {x \<in> C. g x \<in> T}"
+      apply (rule closedin_trans [OF _ UC])
+      apply (rule continuous_closedin_preimage_gen [OF _ _ STT])
+      using hom [unfolded homeomorphism_def] apply blast
+      apply (metis hom homeomorphism_def set_eq_subset)
+      done
+    have ANRS: "ANR {x \<in> C. g x \<in> S}"
+      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR S\<close>])
+      apply (simp add: homeomorphic_def)
+      apply (rule_tac x=g in exI)
+      apply (rule_tac x=f in exI)
+      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+      apply (rule_tac x="f x" in image_eqI, auto)
+      done
+    have ANRT: "ANR {x \<in> C. g x \<in> T}"
+      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR T\<close>])
+      apply (simp add: homeomorphic_def)
+      apply (rule_tac x=g in exI)
+      apply (rule_tac x=f in exI)
+      using hom apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+      apply (rule_tac x="f x" in image_eqI, auto)
+      done
+    have ANRI: "ANR ({x \<in> C. g x \<in> S} \<inter> {x \<in> C. g x \<in> T})"
+      apply (rule ANR_homeomorphic_ANR [OF \<open>ANR (S \<inter> T)\<close>])
+      apply (simp add: homeomorphic_def)
+      apply (rule_tac x=g in exI)
+      apply (rule_tac x=f in exI)
+      using hom
+      apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
+      apply (rule_tac x="f x" in image_eqI, auto)
+      done
+    have "C = {x. x \<in> C \<and> g x \<in> S} \<union> {x. x \<in> C \<and> g x \<in> T}"
+      by auto (metis Un_iff hom homeomorphism_def imageI)
+    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 "\<lbrakk>closed S; closed T; ANR S; ANR T; ANR (S \<inter> T)\<rbrakk> \<Longrightarrow> ANR (S \<union> T)"
+by (simp add: ANR_closed_Un_local closedin_def diff_eq open_Compl openin_open_Int)
+
 end
diff -r 00a135c0a17f -r 3b6975875633 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Jun 14 20:48:42 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Jun 15 15:52:24 2016 +0100
@@ -11,6 +11,25 @@
   "~~/src/HOL/Library/Set_Algebras"
 begin
 
+(*FIXME move up e.g. to Library/Convex.thy, but requires the "support" primitive*)
+lemma convex_supp_setsum:
+  assumes "convex S" and 1: "supp_setsum u I = 1"
+      and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
+    shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
+proof -
+  have fin: "finite {i \<in> I. u i \<noteq> 0}"
+    using 1 setsum.infinite by (force simp: supp_setsum_def support_def)
+  then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I =
+            setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
+    by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def)
+  show ?thesis
+    apply (simp add: eq)
+    apply (rule convex_setsum [OF fin \<open>convex S\<close>])
+    using 1 assms apply (auto simp: supp_setsum_def support_def)
+    done
+qed
+
+
 lemma dim_image_eq:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   assumes lf: "linear f"
diff -r 00a135c0a17f -r 3b6975875633 src/HOL/Multivariate_Analysis/Extension.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Extension.thy	Wed Jun 15 15:52:24 2016 +0100
@@ -0,0 +1,547 @@
+(*  Title:      HOL/Multivariate_Analysis/Extension.thy
+    Authors:    LC Paulson, based on material from HOL Light
+*)
+
+section \<open>Continuous extensions of functions: Urysohn's lemma, Dugundji extension theorem, Tietze\<close>
+
+theory Extension
+imports Convex_Euclidean_Space
+begin
+
+subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>
+
+text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
+   so the "support" must be made explicit in the summation below!\<close>
+
+proposition subordinate_partition_of_unity:
+  fixes S :: "'a :: euclidean_space set"
+  assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
+      and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
+  obtains F :: "['a set, 'a] \<Rightarrow> real"
+    where "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x \<in> S. 0 \<le> F U x)"
+      and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
+      and "\<And>x. x \<in> S \<Longrightarrow> supp_setsum (\<lambda>W. F W x) \<C> = 1"
+      and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
+proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
+  case True
+    then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
+    then show ?thesis
+      apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
+      apply (auto simp: continuous_on_const supp_setsum_def support_def)
+      done
+next
+  case False
+    have nonneg: "0 \<le> supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
+      by (simp add: supp_setsum_def setsum_nonneg)
+    have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
+    proof -
+      have "closedin (subtopology euclidean S) (S - V)"
+        by (simp add: Diff_Diff_Int Diff_subset closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
+      with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
+        show ?thesis
+          by (simp add: order_class.order.order_iff_strict)
+    qed
+    have ss_pos: "0 < supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
+    proof -
+      obtain U where "U \<in> \<C>" "x \<in> U" using \<open>x \<in> S\<close> \<open>S \<subseteq> \<Union>\<C>\<close>
+        by blast
+      obtain V where "open V" "x \<in> V" "finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
+        using \<open>x \<in> S\<close> fin by blast
+      then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
+        using closure_def that by (blast intro: rev_finite_subset)
+      have "x \<notin> closure (S - U)"
+        by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
+      then show ?thesis
+        apply (simp add: setdist_eq_0_sing_1 supp_setsum_def support_def)
+        apply (rule ordered_comm_monoid_add_class.setsum_pos2 [OF *, of U])
+        using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
+        apply (auto simp: setdist_pos_le sd_pos that)
+        done
+    qed
+    define F where
+      "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>
+                 else 0"
+    show ?thesis
+    proof (rule_tac F = F in that)
+      have "continuous_on S (F U)" if "U \<in> \<C>" for U
+      proof -
+        have *: "continuous_on S (\<lambda>x. supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>)"
+        proof (clarsimp simp add: continuous_on_eq_continuous_within)
+          fix x assume "x \<in> S"
+          then obtain X where "open X" and x: "x \<in> S \<inter> X" and finX: "finite {U \<in> \<C>. U \<inter> X \<noteq> {}}"
+            using assms by blast
+          then have OSX: "openin (subtopology euclidean S) (S \<inter> X)" by blast
+          have sumeq: "\<And>x. x \<in> S \<inter> X \<Longrightarrow>
+                     (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V))
+                     = supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>"
+            apply (simp add: supp_setsum_def)
+            apply (rule setsum.mono_neutral_right [OF finX])
+            apply (auto simp: setdist_eq_0_sing_1 support_def subset_iff)
+            apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE)
+            done
+          show "continuous (at x within S) (\<lambda>x. supp_setsum (\<lambda>V. setdist {x} (S - V)) \<C>)"
+            apply (rule continuous_transform_within_openin
+                     [where f = "\<lambda>x. (setsum (\<lambda>V. setdist {x} (S - V)) {V \<in> \<C>. V \<inter> X \<noteq> {}})"
+                        and S ="S \<inter> X"])
+            apply (rule continuous_intros continuous_at_setdist continuous_at_imp_continuous_at_within OSX x)+
+            apply (simp add: sumeq)
+            done
+        qed
+        show ?thesis
+          apply (simp add: F_def)
+          apply (rule continuous_intros *)+
+          using ss_pos apply force
+          done
+      qed
+      moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x
+        using nonneg [of x] by (simp add: F_def divide_simps setdist_pos_le)
+      ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
+        by metis
+    next
+      show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
+        by (simp add: setdist_eq_0_sing_1 closure_def F_def)
+    next
+      show "supp_setsum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x
+        using that ss_pos [OF that]
+        by (simp add: F_def divide_simps supp_setsum_divide_distrib [symmetric])
+    next
+      show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x
+        using fin [OF that] that
+        by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset)
+    qed
+qed
+
+
+subsection\<open>Urysohn's lemma (for real^N, where the proof is easy using distances)\<close>
+
+lemma Urysohn_both_ne:
+  assumes US: "closedin (subtopology euclidean U) S"
+      and UT: "closedin (subtopology euclidean U) T"
+      and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b"
+  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
+    where "continuous_on U f"
+          "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
+          "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
+          "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
+proof -
+  have S0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} S = 0 \<longleftrightarrow> x \<in> S"
+    using \<open>S \<noteq> {}\<close>  US setdist_eq_0_closedin  by auto
+  have T0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} T = 0 \<longleftrightarrow> x \<in> T"
+    using \<open>T \<noteq> {}\<close>  UT setdist_eq_0_closedin  by auto
+  have sdpos: "0 < setdist {x} S + setdist {x} T" if "x \<in> U" for x
+  proof -
+    have "~ (setdist {x} S = 0 \<and> setdist {x} T = 0)"
+      using assms by (metis IntI empty_iff setdist_eq_0_closedin that)
+    then show ?thesis
+      by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le)
+  qed
+  define f where "f \<equiv> \<lambda>x. a + (setdist {x} S / (setdist {x} S + setdist {x} T)) *\<^sub>R (b - a)"
+  show ?thesis
+  proof (rule_tac f = f in that)
+    show "continuous_on U f"
+      using sdpos unfolding f_def
+      by (intro continuous_intros | force)+
+    show "f x \<in> closed_segment a b" if "x \<in> U" for x
+        unfolding f_def
+      apply (simp add: closed_segment_def)
+      apply (rule_tac x="(setdist {x} S / (setdist {x} S + setdist {x} T))" in exI)
+      using sdpos that apply (simp add: algebra_simps)
+      done
+    show "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
+      using S0 \<open>a \<noteq> b\<close> f_def sdpos by force
+    show "(f x = b \<longleftrightarrow> x \<in> T)" if "x \<in> U" for x
+    proof -
+      have "f x = b \<longleftrightarrow> (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1"
+        unfolding f_def
+        apply (rule iffI)
+         apply (metis  \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force)
+        done
+      also have "...  \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0"
+        using sdpos that
+        by (simp add: divide_simps) linarith
+      also have "...  \<longleftrightarrow> x \<in> T"
+        using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that
+        by (force simp: S0 T0)
+      finally show ?thesis .
+    qed
+  qed
+qed
+
+proposition Urysohn_local_strong:
+  assumes US: "closedin (subtopology euclidean U) S"
+      and UT: "closedin (subtopology euclidean U) T"
+      and "S \<inter> T = {}" "a \<noteq> b"
+  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    where "continuous_on U f"
+          "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
+          "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
+          "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
+proof (cases "S = {}")
+  case True show ?thesis
+  proof (cases "T = {}")
+    case True show ?thesis
+    proof (rule_tac f = "\<lambda>x. midpoint a b" in that)
+      show "continuous_on U (\<lambda>x. midpoint a b)"
+        by (intro continuous_intros)
+      show "midpoint a b \<in> closed_segment a b"
+        using csegment_midpoint_subset by blast
+      show "(midpoint a b = a) = (x \<in> S)" for x
+        using \<open>S = {}\<close> \<open>a \<noteq> b\<close> by simp
+      show "(midpoint a b = b) = (x \<in> T)" for x
+        using \<open>T = {}\<close> \<open>a \<noteq> b\<close> by simp
+    qed
+  next
+    case False
+    show ?thesis
+    proof (cases "T = U")
+      case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
+        by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+    next
+      case False
+      with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
+        by fastforce
+      obtain f where f: "continuous_on U f"
+                "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment (midpoint a b) b"
+                "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
+                "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
+        apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"])
+        using c \<open>T \<noteq> {}\<close> assms apply simp_all
+        done
+      show ?thesis
+        apply (rule_tac f=f in that)
+        using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>]
+        apply force+
+        done
+    qed
+  qed
+next
+  case False
+  show ?thesis
+  proof (cases "T = {}")
+    case True show ?thesis
+    proof (cases "S = U")
+      case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
+        by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
+    next
+      case False
+      with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
+        by fastforce
+      obtain f where f: "continuous_on U f"
+                "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)"
+                "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
+                "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
+        apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"])
+        using c \<open>S \<noteq> {}\<close> assms apply simp_all
+        apply (metis midpoint_eq_endpoint)
+        done
+      show ?thesis
+        apply (rule_tac f=f in that)
+        using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f  \<open>a \<noteq> b\<close>
+        apply simp_all
+        apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff)
+        apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint)
+        done
+    qed
+  next
+    case False
+    show ?thesis
+      using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that
+      by blast
+  qed
+qed
+
+lemma Urysohn_local:
+  assumes US: "closedin (subtopology euclidean U) S"
+      and UT: "closedin (subtopology euclidean U) T"
+      and "S \<inter> T = {}"
+  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    where "continuous_on U f"
+          "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
+          "\<And>x. x \<in> S \<Longrightarrow> f x = a"
+          "\<And>x. x \<in> T \<Longrightarrow> f x = b"
+proof (cases "a = b")
+  case True then show ?thesis
+    by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+next
+  case False
+  then show ?thesis
+    apply (rule Urysohn_local_strong [OF assms])
+    apply (erule that, assumption)
+    apply (meson US closedin_singleton closedin_trans)
+    apply (meson UT closedin_singleton closedin_trans)
+    done
+qed
+
+lemma Urysohn_strong:
+  assumes US: "closed S"
+      and UT: "closed T"
+      and "S \<inter> T = {}" "a \<noteq> b"
+  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    where "continuous_on UNIV f"
+          "\<And>x. f x \<in> closed_segment a b"
+          "\<And>x. f x = a \<longleftrightarrow> x \<in> S"
+          "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
+apply (rule Urysohn_local_strong [of UNIV S T])
+using assms
+apply (auto simp: closed_closedin)
+done
+
+proposition Urysohn:
+  assumes US: "closed S"
+      and UT: "closed T"
+      and "S \<inter> T = {}"
+  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+    where "continuous_on UNIV f"
+          "\<And>x. f x \<in> closed_segment a b"
+          "\<And>x. x \<in> S \<Longrightarrow> f x = a"
+          "\<And>x. x \<in> T \<Longrightarrow> f x = b"
+apply (rule Urysohn_local [of UNIV S T a b])
+using assms
+apply (auto simp: closed_closedin)
+done
+
+
+subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
+
+text\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
+http://projecteuclid.org/euclid.pjm/1103052106\<close>
+
+theorem Dugundji:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  assumes "convex C" "C \<noteq> {}"
+      and cloin: "closedin (subtopology euclidean U) S"
+      and contf: "continuous_on S f" and "f ` S \<subseteq> C"
+  obtains g where "continuous_on U g" "g ` U \<subseteq> C"
+                  "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof (cases "S = {}")
+  case True then show thesis
+    apply (rule_tac g="\<lambda>x. @y. y \<in> C" in that)
+      apply (rule continuous_intros)
+     apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
+    done
+next
+  case False
+  then have sd_pos: "\<And>x. \<lbrakk>x \<in> U; x \<notin> S\<rbrakk> \<Longrightarrow> 0 < setdist {x} S"
+    using setdist_eq_0_closedin [OF cloin] le_less setdist_pos_le by fastforce
+  define \<B> where "\<B> = {ball x (setdist {x} S / 2) |x. x \<in> U - S}"
+  have [simp]: "\<And>T. T \<in> \<B> \<Longrightarrow> open T"
+    by (auto simp: \<B>_def)
+  have USS: "U - S \<subseteq> \<Union>\<B>"
+    by (auto simp: sd_pos \<B>_def)
+  obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
+       and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
+       and fin: "\<And>x. x \<in> U - S
+                     \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
+    using paracompact [OF USS] by auto
+  have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
+              T \<subseteq> ball v (setdist {v} S / 2) \<and>
+              dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
+  proof -
+    obtain v where v: "T \<subseteq> ball v (setdist {v} S / 2)" "v \<in> U" "v \<notin> S"
+      using \<open>T \<in> \<C>\<close> nbrhd by (force simp: \<B>_def)
+    then obtain a where "a \<in> S" "dist v a < 2 * setdist {v} S"
+      using setdist_ltE [of "{v}" S "2 * setdist {v} S"]
+      using False sd_pos by force
+    with v show ?thesis
+      apply (rule_tac x=v in exI)
+      apply (rule_tac x=a in exI, auto)
+      done
+  qed
+  then obtain \<V> \<A> where
+    VA: "\<And>T. T \<in> \<C> \<Longrightarrow> \<V> T \<in> U \<and> \<V> T \<notin> S \<and> \<A> T \<in> S \<and>
+              T \<subseteq> ball (\<V> T) (setdist {\<V> T} S / 2) \<and>
+              dist (\<V> T) (\<A> T) \<le> 2 * setdist {\<V> T} S"
+    by metis
+  have sdle: "setdist {\<V> T} S \<le> 2 * setdist {v} S" if "T \<in> \<C>" "v \<in> T" for T v
+    using setdist_Lipschitz [of "\<V> T" S v] VA [OF \<open>T \<in> \<C>\<close>] \<open>v \<in> T\<close> by auto
+  have d6: "dist a (\<A> T) \<le> 6 * dist a v" if "T \<in> \<C>" "v \<in> T" "a \<in> S" for T v a
+  proof -
+    have "dist (\<V> T) v < setdist {\<V> T} S / 2"
+      using that VA mem_ball by blast
+    also have "... \<le> setdist {v} S"
+      using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
+    also have vS: "setdist {v} S \<le> dist a v"
+      by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
+    finally have VTV: "dist (\<V> T) v < dist a v" .
+    have VTS: "setdist {\<V> T} S \<le> 2 * dist a v"
+      using sdle that vS by force
+    have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
+      by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
+    also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
+      using VTV by (simp add: dist_commute)
+    also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
+      using VA [OF \<open>T \<in> \<C>\<close>] by auto
+    finally show ?thesis
+      using VTS by linarith
+  qed
+  obtain H :: "['a set, 'a] \<Rightarrow> real"
+    where Hcont: "\<And>Z. Z \<in> \<C> \<Longrightarrow> continuous_on (U-S) (H Z)"
+      and Hge0: "\<And>Z x. \<lbrakk>Z \<in> \<C>; x \<in> U-S\<rbrakk> \<Longrightarrow> 0 \<le> H Z x"
+      and Heq0: "\<And>x Z. \<lbrakk>Z \<in> \<C>; x \<in> U-S; x \<notin> Z\<rbrakk> \<Longrightarrow> H Z x = 0"
+      and H1: "\<And>x. x \<in> U-S \<Longrightarrow> supp_setsum (\<lambda>W. H W x) \<C> = 1"
+      and Hfin: "\<And>x. x \<in> U-S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. H U x \<noteq> 0}"
+    apply (rule subordinate_partition_of_unity [OF USsub _ fin])
+    using nbrhd by auto
+  define g where "g \<equiv> \<lambda>x. if x \<in> S then f x else supp_setsum (\<lambda>T. H T x *\<^sub>R f(\<A> T)) \<C>"
+  show ?thesis
+  proof (rule that)
+    show "continuous_on U g"
+    proof (clarsimp simp: continuous_on_eq_continuous_within)
+      fix a assume "a \<in> U"
+      show "continuous (at a within U) g"
+      proof (cases "a \<in> S")
+        case True show ?thesis
+        proof (clarsimp simp add: continuous_within_topological)
+          fix W
+          assume "open W" "g a \<in> W"
+          then obtain e where "0 < e" and e: "ball (f a) e \<subseteq> W"
+            using openE True g_def by auto
+          have "continuous (at a within S) f"
+            using True contf continuous_on_eq_continuous_within by blast
+          then obtain d where "0 < d"
+                        and d: "\<And>x. \<lbrakk>x \<in> S; dist x a < d\<rbrakk> \<Longrightarrow> dist (f x) (f a) < e"
+            using continuous_within_eps_delta \<open>0 < e\<close> by force
+          have "g y \<in> ball (f a) e" if "y \<in> U" and y: "y \<in> ball a (d / 6)" for y
+          proof (cases "y \<in> S")
+            case True
+            then have "dist (f a) (f y) < e"
+              by (metis ball_divide_subset_numeral dist_commute in_mono mem_ball y d)
+            then show ?thesis
+              by (simp add: True g_def)
+          next
+            case False
+            have *: "dist (f (\<A> T)) (f a) < e" if "T \<in> \<C>" "H T y \<noteq> 0" for T
+            proof -
+              have "y \<in> T"
+                using Heq0 that False \<open>y \<in> U\<close> by blast
+              have "dist (\<A> T) a < d"
+                using d6 [OF \<open>T \<in> \<C>\<close> \<open>y \<in> T\<close> \<open>a \<in> S\<close>] y
+                by (simp add: dist_commute mult.commute)
+              then show ?thesis
+                using VA [OF \<open>T \<in> \<C>\<close>] by (auto simp: d)
+            qed
+            have "supp_setsum (\<lambda>T. H T y *\<^sub>R f (\<A> T)) \<C> \<in> ball (f a) e"
+              apply (rule convex_supp_setsum [OF convex_ball])
+              apply (simp_all add: False H1 Hge0 \<open>y \<in> U\<close>)
+              by (metis dist_commute *)
+            then show ?thesis
+              by (simp add: False g_def)
+          qed
+          then show "\<exists>A. open A \<and> a \<in> A \<and> (\<forall>y\<in>U. y \<in> A \<longrightarrow> g y \<in> W)"
+            apply (rule_tac x = "ball a (d / 6)" in exI)
+            using e \<open>0 < d\<close> by fastforce
+        qed
+      next
+        case False
+        obtain N where N: "open N" "a \<in> N"
+                   and finN: "finite {U \<in> \<C>. \<exists>a\<in>N. H U a \<noteq> 0}"
+          using Hfin False \<open>a \<in> U\<close> by auto
+        have oUS: "openin (subtopology euclidean U) (U - S)"
+          using cloin by (simp add: openin_diff)
+        have HcontU: "continuous (at a within U) (H T)" if "T \<in> \<C>" for T
+          using Hcont [OF \<open>T \<in> \<C>\<close>] False  \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close>
+          apply (simp add: continuous_on_eq_continuous_within continuous_within)
+          apply (rule Lim_transform_within_set)
+          using oUS
+            apply (force simp: eventually_at openin_contains_ball dist_commute dest!: bspec)+
+          done
+        show ?thesis
+        proof (rule continuous_transform_within_openin [OF _ oUS])
+          show "continuous (at a within U) (\<lambda>x. supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>)"
+          proof (rule continuous_transform_within_openin)
+            show "continuous (at a within U)
+                    (\<lambda>x. \<Sum>T\<in>{U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))"
+              by (force intro: continuous_intros HcontU)+
+          next
+            show "openin (subtopology euclidean U) ((U - S) \<inter> N)"
+              using N oUS openin_trans by blast
+          next
+            show "a \<in> (U - S) \<inter> N" using False \<open>a \<in> U\<close> N by blast
+          next
+            show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow>
+                         (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))
+                         = supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>"
+              by (auto simp: supp_setsum_def support_def
+                       intro: setsum.mono_neutral_right [OF finN])
+          qed
+        next
+          show "a \<in> U - S" using False \<open>a \<in> U\<close> by blast
+        next
+          show "\<And>x. x \<in> U - S \<Longrightarrow> supp_setsum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C> = g x"
+            by (simp add: g_def)
+        qed
+      qed
+    qed
+    show "g ` U \<subseteq> C"
+      using \<open>f ` S \<subseteq> C\<close> VA
+      by (fastforce simp: g_def Hge0 intro!: convex_supp_setsum [OF \<open>convex C\<close>] H1)
+    show "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+      by (simp add: g_def)
+  qed
+qed
+
+
+corollary Tietze:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  assumes "continuous_on S f"
+      and "closedin (subtopology euclidean U) S"
+      and "0 \<le> B"
+      and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
+  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+                  "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
+using assms
+by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
+
+corollary Tietze_closed_interval:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "continuous_on S f"
+      and "closedin (subtopology euclidean U) S"
+      and "cbox a b \<noteq> {}"
+      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
+  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
+apply (rule Dugundji [of "cbox a b" U S f])
+using assms by auto
+
+corollary Tietze_closed_interval_1:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes "continuous_on S f"
+      and "closedin (subtopology euclidean U) S"
+      and "a \<le> b"
+      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
+  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
+apply (rule Dugundji [of "cbox a b" U S f])
+using assms by (auto simp: image_subset_iff)
+
+corollary Tietze_open_interval:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "continuous_on S f"
+      and "closedin (subtopology euclidean U) S"
+      and "box a b \<noteq> {}"
+      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
+  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
+apply (rule Dugundji [of "box a b" U S f])
+using assms by auto
+
+corollary Tietze_open_interval_1:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes "continuous_on S f"
+      and "closedin (subtopology euclidean U) S"
+      and "a < b"
+      and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
+  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
+apply (rule Dugundji [of "box a b" U S f])
+using assms by (auto simp: image_subset_iff)
+
+corollary Tietze_unbounded:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
+  assumes "continuous_on S f"
+      and "closedin (subtopology euclidean U) S"
+  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+apply (rule Dugundji [of UNIV U S f])
+using assms by auto
+
+end
diff -r 00a135c0a17f -r 3b6975875633 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 14 20:48:42 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Jun 15 15:52:24 2016 +0100
@@ -11,173 +11,6 @@
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
-(*FIXME: move elsewhere and use the existing locales*)
-
-subsection \<open>Using additivity of lifted function to encode definedness.\<close>
-
-definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
-
-fun lifted where
-  "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
-| "lifted opp None _ = (None::'b option)"
-| "lifted opp _ None = None"
-
-lemma lifted_simp_1[simp]: "lifted opp v None = None"
-  by (induct v) auto
-
-definition "monoidal opp \<longleftrightarrow>
-  (\<forall>x y. opp x y = opp y x) \<and>
-  (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
-  (\<forall>x. opp (neutral opp) x = x)"
-
-lemma monoidalI:
-  assumes "\<And>x y. opp x y = opp y x"
-    and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
-    and "\<And>x. opp (neutral opp) x = x"
-  shows "monoidal opp"
-  unfolding monoidal_def using assms by fastforce
-
-lemma monoidal_ac:
-  assumes "monoidal opp"
-  shows [simp]: "opp (neutral opp) a = a"
-    and [simp]: "opp a (neutral opp) = a"
-    and "opp a b = opp b a"
-    and "opp (opp a b) c = opp a (opp b c)"
-    and "opp a (opp b c) = opp b (opp a c)"
-  using assms unfolding monoidal_def by metis+
-
-lemma neutral_lifted [cong]:
-  assumes "monoidal opp"
-  shows "neutral (lifted opp) = Some (neutral opp)"
-proof -
-  { fix x
-    assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
-    then have "Some (neutral opp) = x"
-      apply (induct x)
-      apply force
-      by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
-  note [simp] = this
-  show ?thesis
-    apply (subst neutral_def)
-    apply (intro some_equality allI)
-    apply (induct_tac y)
-    apply (auto simp add:monoidal_ac[OF assms])
-    done
-qed
-
-lemma monoidal_lifted[intro]:
-  assumes "monoidal opp"
-  shows "monoidal (lifted opp)"
-  unfolding monoidal_def split_option_all neutral_lifted[OF assms]
-  using monoidal_ac[OF assms]
-  by auto
-
-definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
-definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
-definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
-
-lemma support_subset[intro]: "support opp f s \<subseteq> s"
-  unfolding support_def by auto
-
-lemma support_empty[simp]: "support opp f {} = {}"
-  using support_subset[of opp f "{}"] by auto
-
-lemma comp_fun_commute_monoidal[intro]:
-  assumes "monoidal opp"
-  shows "comp_fun_commute opp"
-  unfolding comp_fun_commute_def
-  using monoidal_ac[OF assms]
-  by auto
-
-lemma support_clauses:
-  "\<And>f g s. support opp f {} = {}"
-  "\<And>f g s. support opp f (insert x s) =
-    (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
-  "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
-  "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
-  "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
-  "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
-  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
-  unfolding support_def by auto
-
-lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
-  unfolding support_def by auto
-
-lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
-  unfolding iterate_def fold'_def by auto
-
-lemma iterate_insert[simp]:
-  assumes "monoidal opp"
-    and "finite s"
-  shows "iterate opp (insert x s) f =
-         (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
-proof (cases "x \<in> s")
-  case True
-  then show ?thesis by (auto simp: insert_absorb iterate_def)
-next
-  case False
-  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
-  show ?thesis
-  proof (cases "f x = neutral opp")
-    case True
-    then show ?thesis
-      using assms \<open>x \<notin> s\<close>
-      by (auto simp: iterate_def support_clauses)
-  next
-    case False
-    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
-      apply (simp add: iterate_def fold'_def support_clauses)
-      apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
-      apply (force simp add: )+
-      done
-  qed
-qed
-
-lemma iterate_some:
-    "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
-  by (erule finite_induct) (auto simp: monoidal_lifted)
-
-lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
-  unfolding neutral_def
-  by (force elim: allE [where x=0])
-
-lemma support_if: "a \<noteq> neutral opp \<Longrightarrow> support opp (\<lambda>x. if P x then a else neutral opp) A = {x \<in> A. P x}"
-unfolding support_def
-by (force intro: Collect_cong)
-
-lemma support_if_subset: "support opp (\<lambda>x. if P x then a else neutral opp) A \<subseteq> {x \<in> A. P x}"
-by (simp add: subset_iff support_def)
-
-definition supp_setsum where "supp_setsum f A \<equiv> setsum f (support op+ f A)"
-
-lemma supp_setsum_divide_distrib:
-    "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A"
-apply (cases "r = 0")
-apply (simp add: supp_setsum_def)
-apply (simp add: supp_setsum_def setsum_divide_distrib support_def)
-done
-
-(*FIXME move up e.g. to Library/Convex.thy*)
-lemma convex_supp_setsum:
-  assumes "convex S" and 1: "supp_setsum u I = 1"
-      and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)"
-    shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S"
-proof -
-  have fin: "finite {i \<in> I. u i \<noteq> 0}"
-    using 1 setsum.infinite by (force simp: supp_setsum_def support_def)
-  then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I =
-            setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}"
-    by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def)
-  show ?thesis
-    apply (simp add: eq)
-    apply (rule convex_setsum [OF fin \<open>convex S\<close>])
-    using 1 assms apply (auto simp: supp_setsum_def support_def)
-    done
-qed
-
-(*END OF SUPPORT, ETC.*)
-
-
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
diff -r 00a135c0a17f -r 3b6975875633 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Jun 14 20:48:42 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Jun 15 15:52:24 2016 +0100
@@ -5,7 +5,7 @@
 section \<open>Continuous paths and path-connected sets\<close>
 
 theory Path_Connected
-imports Convex_Euclidean_Space
+imports Extension
 begin
 
 subsection \<open>Paths and Arcs\<close>
@@ -5763,4 +5763,251 @@
     "S homeomorphic T \<Longrightarrow> (simply_connected S \<longleftrightarrow> simply_connected T)"
   by (metis homeomorphic_simply_connected homeomorphic_sym)
 
+subsection\<open>Homotopy equivalence\<close>
+
+definition homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
+             (infix "homotopy'_eqv" 50)
+  where "S homotopy_eqv T \<equiv>
+        \<exists>f g. continuous_on S f \<and> f ` S \<subseteq> T \<and>
+              continuous_on T g \<and> g ` T \<subseteq> S \<and>
+              homotopic_with (\<lambda>x. True) S S (g o f) id \<and>
+              homotopic_with (\<lambda>x. True) T T (f o g) id"
+
+lemma homeomorphic_imp_homotopy_eqv: "S homeomorphic T \<Longrightarrow> S homotopy_eqv T"
+  unfolding homeomorphic_def homotopy_eqv_def homeomorphism_def
+  by (fastforce intro!: homotopic_with_equal continuous_on_compose)
+
+lemma homotopy_eqv_refl: "S homotopy_eqv S"
+  by (rule homeomorphic_imp_homotopy_eqv homeomorphic_refl)+
+
+lemma homotopy_eqv_sym: "S homotopy_eqv T \<longleftrightarrow> T homotopy_eqv S"
+  by (auto simp: homotopy_eqv_def)
+
+lemma homotopy_eqv_trans [trans]:
+    fixes S :: "'a::real_normed_vector set" and U :: "'c::real_normed_vector set"
+  assumes ST: "S homotopy_eqv T" and TU: "T homotopy_eqv U"
+    shows "S homotopy_eqv U"
+proof -
+  obtain f1 g1 where f1: "continuous_on S f1" "f1 ` S \<subseteq> T"
+                 and g1: "continuous_on T g1" "g1 ` T \<subseteq> S"
+                 and hom1: "homotopic_with (\<lambda>x. True) S S (g1 o f1) id"
+                           "homotopic_with (\<lambda>x. True) T T (f1 o g1) id"
+    using ST by (auto simp: homotopy_eqv_def)
+  obtain f2 g2 where f2: "continuous_on T f2" "f2 ` T \<subseteq> U"
+                 and g2: "continuous_on U g2" "g2 ` U \<subseteq> T"
+                 and hom2: "homotopic_with (\<lambda>x. True) T T (g2 o f2) id"
+                           "homotopic_with (\<lambda>x. True) U U (f2 o g2) id"
+    using TU by (auto simp: homotopy_eqv_def)
+  have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> f2 \<circ> f1) (id \<circ> f1)"
+    by (rule homotopic_with_compose_continuous_right hom2 f1)+
+  then have "homotopic_with (\<lambda>f. True) S T (g2 \<circ> (f2 \<circ> f1)) (id \<circ> f1)"
+    by (simp add: o_assoc)
+  then have "homotopic_with (\<lambda>x. True) S S
+         (g1 \<circ> (g2 \<circ> (f2 \<circ> f1))) (g1 o (id o f1))"
+    by (simp add: g1 homotopic_with_compose_continuous_left)
+  moreover have "homotopic_with (\<lambda>x. True) S S (g1 o id o f1) id"
+    using hom1 by simp
+  ultimately have SS: "homotopic_with (\<lambda>x. True) S S (g1 \<circ> g2 \<circ> (f2 \<circ> f1)) id"
+    apply (simp add: o_assoc)
+    apply (blast intro: homotopic_with_trans)
+    done
+  have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> g1 \<circ> g2) (id \<circ> g2)"
+    by (rule homotopic_with_compose_continuous_right hom1 g2)+
+  then have "homotopic_with (\<lambda>f. True) U T (f1 \<circ> (g1 \<circ> g2)) (id \<circ> g2)"
+    by (simp add: o_assoc)
+  then have "homotopic_with (\<lambda>x. True) U U
+         (f2 \<circ> (f1 \<circ> (g1 \<circ> g2))) (f2 o (id o g2))"
+    by (simp add: f2 homotopic_with_compose_continuous_left)
+  moreover have "homotopic_with (\<lambda>x. True) U U (f2 o id o g2) id"
+    using hom2 by simp
+  ultimately have UU: "homotopic_with (\<lambda>x. True) U U (f2 \<circ> f1 \<circ> (g1 \<circ> g2)) id"
+    apply (simp add: o_assoc)
+    apply (blast intro: homotopic_with_trans)
+    done
+  show ?thesis
+    unfolding homotopy_eqv_def
+    apply (rule_tac x = "f2 \<circ> f1" in exI)
+    apply (rule_tac x = "g1 \<circ> g2" in exI)
+    apply (intro conjI continuous_on_compose SS UU)
+    using f1 f2 g1 g2  apply (force simp: elim!: continuous_on_subset)+
+    done
+qed
+
+lemma homotopy_eqv_inj_linear_image:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "inj f"
+    shows "(f ` S) homotopy_eqv S"
+apply (rule homeomorphic_imp_homotopy_eqv)
+using assms homeomorphic_sym linear_homeomorphic_image by auto
+
+lemma homotopy_eqv_translation:
+    fixes S :: "'a::real_normed_vector set"
+    shows "op + a ` S homotopy_eqv S"
+  apply (rule homeomorphic_imp_homotopy_eqv)
+  using homeomorphic_translation homeomorphic_sym by blast
+
+lemma homotopy_eqv_homotopic_triviality_imp:
+  fixes S :: "'a::real_normed_vector set"
+    and T :: "'b::real_normed_vector set"
+    and U :: "'c::real_normed_vector set"
+  assumes "S homotopy_eqv T"
+      and f: "continuous_on U f" "f ` U \<subseteq> T"
+      and g: "continuous_on U g" "g ` U \<subseteq> T"
+      and homUS: "\<And>f g. \<lbrakk>continuous_on U f; f ` U \<subseteq> S;
+                         continuous_on U g; g ` U \<subseteq> S\<rbrakk>
+                         \<Longrightarrow> homotopic_with (\<lambda>x. True) U S f g"
+    shows "homotopic_with (\<lambda>x. True) U T f g"
+proof -
+  obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
+               and k: "continuous_on T k" "k ` T \<subseteq> S"
+               and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id"
+                        "homotopic_with (\<lambda>x. True) T T (h o k) id"
+    using assms by (auto simp: homotopy_eqv_def)
+  have "homotopic_with (\<lambda>f. True) U S (k \<circ> f) (k \<circ> g)"
+    apply (rule homUS)
+    using f g k
+    apply (safe intro!: continuous_on_compose h k f elim!: continuous_on_subset)
+    apply (force simp: o_def)+
+    done
+  then have "homotopic_with (\<lambda>x. True) U T (h o (k o f)) (h o (k o g))"
+    apply (rule homotopic_with_compose_continuous_left)
+    apply (simp_all add: h)
+    done
+  moreover have "homotopic_with (\<lambda>x. True) U T (h o k o f) (id o f)"
+    apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
+    apply (auto simp: hom f)
+    done
+  moreover have "homotopic_with (\<lambda>x. True) U T (h o k o g) (id o g)"
+    apply (rule homotopic_with_compose_continuous_right [where X=T and Y=T])
+    apply (auto simp: hom g)
+    done
+  ultimately show "homotopic_with (\<lambda>x. True) U T f g"
+    apply (simp add: o_assoc)
+    using homotopic_with_trans homotopic_with_sym by blast
+qed
+
+lemma homotopy_eqv_homotopic_triviality:
+  fixes S :: "'a::real_normed_vector set"
+    and T :: "'b::real_normed_vector set"
+    and U :: "'c::real_normed_vector set"
+  assumes "S homotopy_eqv T"
+    shows "(\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> S \<and>
+                   continuous_on U g \<and> g ` U \<subseteq> S
+                   \<longrightarrow> homotopic_with (\<lambda>x. True) U S f g) \<longleftrightarrow>
+           (\<forall>f g. continuous_on U f \<and> f ` U \<subseteq> T \<and>
+                  continuous_on U g \<and> g ` U \<subseteq> T
+                  \<longrightarrow> homotopic_with (\<lambda>x. True) U T f g)"
+apply (rule iffI)
+apply (metis assms homotopy_eqv_homotopic_triviality_imp)
+by (metis (no_types) assms homotopy_eqv_homotopic_triviality_imp homotopy_eqv_sym)
+
+
+lemma homotopy_eqv_cohomotopic_triviality_null_imp:
+  fixes S :: "'a::real_normed_vector set"
+    and T :: "'b::real_normed_vector set"
+    and U :: "'c::real_normed_vector set"
+  assumes "S homotopy_eqv T"
+      and f: "continuous_on T f" "f ` T \<subseteq> U"
+      and homSU: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> U\<rbrakk>
+                      \<Longrightarrow> \<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c)"
+  obtains c where "homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)"
+proof -
+  obtain h k where h: "continuous_on S h" "h ` S \<subseteq> T"
+               and k: "continuous_on T k" "k ` T \<subseteq> S"
+               and hom: "homotopic_with (\<lambda>x. True) S S (k o h) id"
+                        "homotopic_with (\<lambda>x. True) T T (h o k) id"
+    using assms by (auto simp: homotopy_eqv_def)
+  obtain c where "homotopic_with (\<lambda>x. True) S U (f \<circ> h) (\<lambda>x. c)"
+    apply (rule exE [OF homSU [of "f \<circ> h"]])
+    apply (intro continuous_on_compose h)
+    using h f  apply (force elim!: continuous_on_subset)+
+    done
+  then have "homotopic_with (\<lambda>x. True) T U ((f o h) o k) ((\<lambda>x. c) o k)"
+    apply (rule homotopic_with_compose_continuous_right [where X=S])
+    using k by auto
+  moreover have "homotopic_with (\<lambda>x. True) T U (f \<circ> id) (f \<circ> (h \<circ> k))"
+    apply (rule homotopic_with_compose_continuous_left [where Y=T])
+      apply (simp add: hom homotopic_with_symD)
+     using f apply auto
+    done
+  ultimately show ?thesis
+    apply (rule_tac c=c in that)
+    apply (simp add: o_def)
+    using homotopic_with_trans by blast
+qed
+
+lemma homotopy_eqv_cohomotopic_triviality_null:
+  fixes S :: "'a::real_normed_vector set"
+    and T :: "'b::real_normed_vector set"
+    and U :: "'c::real_normed_vector set"
+  assumes "S homotopy_eqv T"
+    shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> U
+                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) S U f (\<lambda>x. c))) \<longleftrightarrow>
+           (\<forall>f. continuous_on T f \<and> f ` T \<subseteq> U
+                \<longrightarrow> (\<exists>c. homotopic_with (\<lambda>x. True) T U f (\<lambda>x. c)))"
+apply (rule iffI)
+apply (metis assms homotopy_eqv_cohomotopic_triviality_null_imp)
+by (metis assms homotopy_eqv_cohomotopic_triviality_null_imp homotopy_eqv_sym)
+
+
+lemma homotopy_eqv_contractible_sets:
+  fixes S :: "'a::real_normed_vector set"
+    and T :: "'b::real_normed_vector set"
+  assumes "contractible S" "contractible T" "S = {} \<longleftrightarrow> T = {}"
+    shows "S homotopy_eqv T"
+proof (cases "S = {}")
+  case True with assms show ?thesis
+    by (simp add: homeomorphic_imp_homotopy_eqv)
+next
+  case False
+  with assms obtain a b where "a \<in> S" "b \<in> T"
+    by auto
+  then show ?thesis
+    unfolding homotopy_eqv_def
+    apply (rule_tac x="\<lambda>x. b" in exI)
+    apply (rule_tac x="\<lambda>x. a" in exI)
+    apply (intro assms conjI continuous_on_id' homotopic_into_contractible)
+    apply (auto simp: o_def continuous_on_const)
+    done
+qed
+
+lemma homotopy_eqv_empty1 [simp]:
+  fixes S :: "'a::real_normed_vector set"
+  shows "S homotopy_eqv ({}::'b::real_normed_vector set) \<longleftrightarrow> S = {}"
+apply (rule iffI)
+using homotopy_eqv_def apply fastforce
+by (simp add: homotopy_eqv_contractible_sets contractible_empty)
+
+lemma homotopy_eqv_empty2 [simp]:
+  fixes S :: "'a::real_normed_vector set"
+  shows "({}::'b::real_normed_vector set) homotopy_eqv S \<longleftrightarrow> S = {}"
+by (metis homotopy_eqv_empty1 homotopy_eqv_sym)
+
+lemma homotopy_eqv_contractibility:
+  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+  shows "S homotopy_eqv T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)"
+unfolding homotopy_eqv_def
+by (blast intro: homotopy_dominated_contractibility)
+
+lemma homotopy_eqv_sing:
+  fixes S :: "'a::real_normed_vector set" and a :: "'b::real_normed_vector"
+  shows "S homotopy_eqv {a} \<longleftrightarrow> S \<noteq> {} \<and> contractible S"
+proof (cases "S = {}")
+  case True then show ?thesis
+    by simp
+next
+  case False then show ?thesis
+    by (metis contractible_sing empty_not_insert homotopy_eqv_contractibility homotopy_eqv_contractible_sets)
+qed
+
+lemma homeomorphic_contractible_eq:
+  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+  shows "S homeomorphic T \<Longrightarrow> (contractible S \<longleftrightarrow> contractible T)"
+by (simp add: homeomorphic_imp_homotopy_eqv homotopy_eqv_contractibility)
+
+lemma homeomorphic_contractible:
+  fixes S :: "'a::real_normed_vector set" and T :: "'b::real_normed_vector set"
+  shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
+by (metis homeomorphic_contractible_eq)
+
 end
diff -r 00a135c0a17f -r 3b6975875633 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Jun 14 20:48:42 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Jun 15 15:52:24 2016 +0100
@@ -15,6 +15,157 @@
   Norm_Arith
 begin
 
+
+(*FIXME: move elsewhere and use the existing locales*)
+
+subsection \<open>Using additivity of lifted function to encode definedness.\<close>
+
+definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)"
+
+fun lifted where
+  "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)"
+| "lifted opp None _ = (None::'b option)"
+| "lifted opp _ None = None"
+
+lemma lifted_simp_1[simp]: "lifted opp v None = None"
+  by (induct v) auto
+
+definition "monoidal opp \<longleftrightarrow>
+  (\<forall>x y. opp x y = opp y x) \<and>
+  (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
+  (\<forall>x. opp (neutral opp) x = x)"
+
+lemma monoidalI:
+  assumes "\<And>x y. opp x y = opp y x"
+    and "\<And>x y z. opp x (opp y z) = opp (opp x y) z"
+    and "\<And>x. opp (neutral opp) x = x"
+  shows "monoidal opp"
+  unfolding monoidal_def using assms by fastforce
+
+lemma monoidal_ac:
+  assumes "monoidal opp"
+  shows [simp]: "opp (neutral opp) a = a"
+    and [simp]: "opp a (neutral opp) = a"
+    and "opp a b = opp b a"
+    and "opp (opp a b) c = opp a (opp b c)"
+    and "opp a (opp b c) = opp b (opp a c)"
+  using assms unfolding monoidal_def by metis+
+
+lemma neutral_lifted [cong]:
+  assumes "monoidal opp"
+  shows "neutral (lifted opp) = Some (neutral opp)"
+proof -
+  { fix x
+    assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+    then have "Some (neutral opp) = x"
+      apply (induct x)
+      apply force
+      by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) }
+  note [simp] = this
+  show ?thesis
+    apply (subst neutral_def)
+    apply (intro some_equality allI)
+    apply (induct_tac y)
+    apply (auto simp add:monoidal_ac[OF assms])
+    done
+qed
+
+lemma monoidal_lifted[intro]:
+  assumes "monoidal opp"
+  shows "monoidal (lifted opp)"
+  unfolding monoidal_def split_option_all neutral_lifted[OF assms]
+  using monoidal_ac[OF assms]
+  by auto
+
+definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
+definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)"
+definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
+
+lemma support_subset[intro]: "support opp f s \<subseteq> s"
+  unfolding support_def by auto
+
+lemma support_empty[simp]: "support opp f {} = {}"
+  using support_subset[of opp f "{}"] by auto
+
+lemma comp_fun_commute_monoidal[intro]:
+  assumes "monoidal opp"
+  shows "comp_fun_commute opp"
+  unfolding comp_fun_commute_def
+  using monoidal_ac[OF assms]
+  by auto
+
+lemma support_clauses:
+  "\<And>f g s. support opp f {} = {}"
+  "\<And>f g s. support opp f (insert x s) =
+    (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
+  "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
+  "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
+  "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
+  "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)"
+  "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)"
+  unfolding support_def by auto
+
+lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)"
+  unfolding support_def by auto
+
+lemma iterate_empty[simp]: "iterate opp {} f = neutral opp"
+  unfolding iterate_def fold'_def by auto
+
+lemma iterate_insert[simp]:
+  assumes "monoidal opp"
+    and "finite s"
+  shows "iterate opp (insert x s) f =
+         (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))"
+proof (cases "x \<in> s")
+  case True
+  then show ?thesis by (auto simp: insert_absorb iterate_def)
+next
+  case False
+  note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]]
+  show ?thesis
+  proof (cases "f x = neutral opp")
+    case True
+    then show ?thesis
+      using assms \<open>x \<notin> s\<close>
+      by (auto simp: iterate_def support_clauses)
+  next
+    case False
+    with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis
+      apply (simp add: iterate_def fold'_def support_clauses)
+      apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def])
+      apply (force simp add: )+
+      done
+  qed
+qed
+
+lemma iterate_some:
+    "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)"
+  by (erule finite_induct) (auto simp: monoidal_lifted)
+
+lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)"
+  unfolding neutral_def
+  by (force elim: allE [where x=0])
+
+lemma support_if: "a \<noteq> neutral opp \<Longrightarrow> support opp (\<lambda>x. if P x then a else neutral opp) A = {x \<in> A. P x}"
+unfolding support_def
+by (force intro: Collect_cong)
+
+lemma support_if_subset: "support opp (\<lambda>x. if P x then a else neutral opp) A \<subseteq> {x \<in> A. P x}"
+by (simp add: subset_iff support_def)
+
+definition supp_setsum where "supp_setsum f A \<equiv> setsum f (support op+ f A)"
+
+lemma supp_setsum_divide_distrib:
+    "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A"
+apply (cases "r = 0")
+apply (simp add: supp_setsum_def)
+apply (simp add: supp_setsum_def setsum_divide_distrib support_def)
+done
+
+(*END OF SUPPORT, ETC.*)
+
+
+
 lemma image_affinity_interval:
   fixes c :: "'a::ordered_real_vector"
   shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}
@@ -691,6 +842,11 @@
 lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
   by (auto simp add: openin_subtopology open_openin[symmetric])
 
+lemma openin_Int_open:
+   "\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk>
+        \<Longrightarrow> openin (subtopology euclidean U) (S \<inter> T)"
+by (metis open_Int Int_assoc openin_open)
+
 lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
   by (auto simp add: openin_open)
 
@@ -714,6 +870,11 @@
 lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
   by (auto simp add: closedin_closed)
 
+lemma closedin_singleton [simp]:
+  fixes a :: "'a::t1_space"
+  shows "closedin (subtopology euclidean U) {a} \<longleftrightarrow> a \<in> U"
+using closedin_subset  by (force intro: closed_subset)
+
 lemma openin_euclidean_subtopology_iff:
   fixes S U :: "'a::metric_space set"
   shows "openin (subtopology euclidean U) S \<longleftrightarrow>