--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Jan 25 02:38:26 2019 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Fri Jan 25 13:19:16 2019 +0100
@@ -21,196 +21,8 @@
Continuous_Extension
begin
-(* FIXME mv topology euclidean space *)
subsection \<open>Retractions\<close>
-definition%important retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
-where "retraction S T r \<longleftrightarrow>
- T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
-
-definition%important retract_of (infixl "retract'_of" 50) where
-"T retract_of S \<longleftrightarrow> (\<exists>r. retraction S T r)"
-
-lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow> r (r x) = r x"
- unfolding retraction_def by auto
-
-text \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
-
-lemma invertible_fixpoint_property:
- fixes S :: "'a::euclidean_space set"
- and T :: "'b::euclidean_space set"
- assumes contt: "continuous_on T i"
- and "i ` T \<subseteq> S"
- and contr: "continuous_on S r"
- and "r ` S \<subseteq> T"
- and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
- and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
- and contg: "continuous_on T g"
- and "g ` T \<subseteq> T"
- obtains y where "y \<in> T" and "g y = y"
-proof -
- have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
- proof (rule FP)
- show "continuous_on S (i \<circ> g \<circ> r)"
- by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
- show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
- using assms(2,4,8) by force
- qed
- then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
- then have *: "g (r x) \<in> T"
- using assms(4,8) by auto
- have "r ((i \<circ> g \<circ> r) x) = r x"
- using x by auto
- then show ?thesis
- using "*" ri that by auto
-qed
-
-lemma homeomorphic_fixpoint_property:
- fixes S :: "'a::euclidean_space set"
- and T :: "'b::euclidean_space set"
- assumes "S homeomorphic T"
- shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
- (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
- (is "?lhs = ?rhs")
-proof -
- obtain r i where r:
- "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
- "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
- using assms unfolding homeomorphic_def homeomorphism_def by blast
- show ?thesis
- proof
- assume ?lhs
- with r show ?rhs
- by (metis invertible_fixpoint_property[of T i S r] order_refl)
- next
- assume ?rhs
- with r show ?lhs
- by (metis invertible_fixpoint_property[of S r T i] order_refl)
- qed
-qed
-
-lemma retract_fixpoint_property:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- and S :: "'a set"
- assumes "T retract_of S"
- and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
- and contg: "continuous_on T g"
- and "g ` T \<subseteq> T"
- obtains y where "y \<in> T" and "g y = y"
-proof -
- obtain h where "retraction S T h"
- using assms(1) unfolding retract_of_def ..
- then show ?thesis
- unfolding retraction_def
- using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
- by (metis assms(4) contg image_ident that)
-qed
-
-lemma retraction:
- "retraction S T r \<longleftrightarrow>
- T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
- by (force simp: retraction_def)
-
-lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
- assumes "retraction S T r"
- obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
-proof (rule that)
- from retraction [of S T r] assms
- have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x"
- by simp_all
- then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r"
- by simp_all
- from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x
- using that by simp
- with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x
- using that by auto
-qed
-
-lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
- assumes "T retract_of S"
- obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
-proof -
- from assms obtain r where "retraction S T r"
- by (auto simp add: retract_of_def)
- with that show thesis
- by (auto elim: retractionE)
-qed
-
-lemma retract_of_imp_extensible:
- assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
- obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
-proof -
- from \<open>S retract_of T\<close> obtain r where "retraction T S r"
- by (auto simp add: retract_of_def)
- show thesis
- by (rule that [of "f \<circ> r"])
- (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
-qed
-
-lemma idempotent_imp_retraction:
- assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
- shows "retraction S (f ` S) f"
-by (simp add: assms retraction)
-
-lemma retraction_subset:
- assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
- shows "retraction s' T r"
- unfolding retraction_def
- by (metis assms continuous_on_subset image_mono retraction)
-
-lemma retract_of_subset:
- assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
- shows "T retract_of s'"
-by (meson assms retract_of_def retraction_subset)
-
-lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
-by (simp add: continuous_on_id retraction)
-
-lemma retract_of_refl [iff]: "S retract_of S"
- unfolding retract_of_def retraction_def
- using continuous_on_id by blast
-
-lemma retract_of_imp_subset:
- "S retract_of T \<Longrightarrow> S \<subseteq> T"
-by (simp add: retract_of_def retraction_def)
-
-lemma retract_of_empty [simp]:
- "({} retract_of S) \<longleftrightarrow> S = {}" "(S retract_of {}) \<longleftrightarrow> S = {}"
-by (auto simp: retract_of_def retraction_def)
-
-lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
- unfolding retract_of_def retraction_def by force
-
-lemma retraction_comp:
- "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
- \<Longrightarrow> retraction S U (g \<circ> f)"
-apply (auto simp: retraction_def intro: continuous_on_compose2)
-by blast
-
-lemma retract_of_trans [trans]:
- assumes "S retract_of T" and "T retract_of U"
- shows "S retract_of U"
-using assms by (auto simp: retract_of_def intro: retraction_comp)
-
-lemma closedin_retract:
- fixes S :: "'a :: real_normed_vector set"
- assumes "S retract_of T"
- shows "closedin (subtopology euclidean T) S"
-proof -
- obtain r where "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
- using assms by (auto simp: retract_of_def retraction_def)
- then have S: "S = {x \<in> T. (norm(r x - x)) = 0}" by auto
- show ?thesis
- apply (subst S)
- apply (rule continuous_closedin_preimage_constant)
- by (simp add: \<open>continuous_on T r\<close> continuous_on_diff continuous_on_id continuous_on_norm)
-qed
-
-lemma closedin_self [simp]:
- fixes S :: "'a :: real_normed_vector set"
- shows "closedin (subtopology euclidean S) S"
- by (simp add: closedin_retract)
-
lemma retract_of_contractible:
assumes "contractible T" "S retract_of T"
shows "contractible S"
@@ -222,19 +34,6 @@
apply (erule continuous_on_subset | force)+
done
-lemma retract_of_compact:
- "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
- by (metis compact_continuous_image retract_of_def retraction)
-
-lemma retract_of_closed:
- fixes S :: "'a :: real_normed_vector set"
- shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
- by (metis closedin_retract closedin_closed_eq)
-
-lemma retract_of_connected:
- "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
- by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
-
lemma retract_of_path_connected:
"\<lbrakk>path_connected T; S retract_of T\<rbrakk> \<Longrightarrow> path_connected S"
by (metis path_connected_continuous_image retract_of_def retraction)
@@ -243,7 +42,7 @@
"\<lbrakk>simply_connected T; S retract_of T\<rbrakk> \<Longrightarrow> simply_connected S"
apply (simp add: retract_of_def retraction_def, clarify)
apply (rule simply_connected_retraction_gen)
-apply (force simp: continuous_on_id elim!: continuous_on_subset)+
+apply (force elim!: continuous_on_subset)+
done
lemma retract_of_homotopically_trivial:
@@ -298,14 +97,6 @@
shows "\<lbrakk> locally compact S; T retract_of S\<rbrakk> \<Longrightarrow> locally compact T"
by (metis locally_compact_closedin closedin_retract)
-lemma retract_of_Times:
- "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
-apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
-apply (rename_tac f g)
-apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
-apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
-done
-
lemma homotopic_into_retract:
"\<lbrakk>f ` S \<subseteq> T; g ` S \<subseteq> T; T retract_of U; homotopic_with (\<lambda>x. True) S U f g\<rbrakk>
\<Longrightarrow> homotopic_with (\<lambda>x. True) S T f g"
@@ -375,7 +166,7 @@
by (simp add: \<open>a \<in> S\<close>)
moreover have "homotopic_with (\<lambda>x. True) S S id (\<lambda>x. a)"
using assms
- by (auto simp: contractible_def continuous_on_const continuous_on_id homotopic_into_contractible image_subset_iff)
+ by (auto simp: contractible_def homotopic_into_contractible image_subset_iff)
moreover have "(\<lambda>x. a) ` S \<subseteq> {a}"
by (simp add: image_subsetI)
ultimately show ?thesis
@@ -1788,32 +1579,6 @@
using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
qed auto
-(* FIXME mv *)
-lemma brouwer_compactness_lemma:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
- assumes "compact s"
- and "continuous_on s f"
- and "\<not> (\<exists>x\<in>s. f x = 0)"
- obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
-proof (cases "s = {}")
- case True
- show thesis
- by (rule that [of 1]) (auto simp: True)
-next
- case False
- have "continuous_on s (norm \<circ> f)"
- by (rule continuous_intros continuous_on_norm assms(2))+
- with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
- using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
- unfolding o_def
- by auto
- have "(norm \<circ> f) x > 0"
- using assms(3) and x(1)
- by auto
- then show ?thesis
- by (rule that) (insert x(2), auto simp: o_def)
-qed
-
lemma kuhn_labelling_lemma:
fixes P Q :: "'a::euclidean_space \<Rightarrow> bool"
assumes "\<forall>x. P x \<longrightarrow> P (f x)"
--- a/src/HOL/Analysis/Elementary_Topology.thy Fri Jan 25 02:38:26 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy Fri Jan 25 13:19:16 2019 +0100
@@ -1558,6 +1558,31 @@
subsection \<open>Compactness\<close>
+lemma brouwer_compactness_lemma:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+ assumes "compact s"
+ and "continuous_on s f"
+ and "\<not> (\<exists>x\<in>s. f x = 0)"
+ obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
+proof (cases "s = {}")
+ case True
+ show thesis
+ by (rule that [of 1]) (auto simp: True)
+next
+ case False
+ have "continuous_on s (norm \<circ> f)"
+ by (rule continuous_intros continuous_on_norm assms(2))+
+ with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
+ using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
+ unfolding o_def
+ by auto
+ have "(norm \<circ> f) x > 0"
+ using assms(3) and x(1)
+ by auto
+ then show ?thesis
+ by (rule that) (insert x(2), auto simp: o_def)
+qed
+
subsubsection \<open>Bolzano-Weierstrass property\<close>
proposition Heine_Borel_imp_Bolzano_Weierstrass:
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jan 25 02:38:26 2019 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jan 25 13:19:16 2019 +0100
@@ -2343,4 +2343,224 @@
no_notation
eucl_less (infix "<e" 50)
+
+subsection \<open>Retractions\<close>
+
+definition%important retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+where "retraction S T r \<longleftrightarrow>
+ T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
+
+definition%important retract_of (infixl "retract'_of" 50) where
+"T retract_of S \<longleftrightarrow> (\<exists>r. retraction S T r)"
+
+lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow> r (r x) = r x"
+ unfolding retraction_def by auto
+
+text \<open>Preservation of fixpoints under (more general notion of) retraction\<close>
+
+lemma invertible_fixpoint_property:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'b::euclidean_space set"
+ assumes contt: "continuous_on T i"
+ and "i ` T \<subseteq> S"
+ and contr: "continuous_on S r"
+ and "r ` S \<subseteq> T"
+ and ri: "\<And>y. y \<in> T \<Longrightarrow> r (i y) = y"
+ and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
+ and contg: "continuous_on T g"
+ and "g ` T \<subseteq> T"
+ obtains y where "y \<in> T" and "g y = y"
+proof -
+ have "\<exists>x\<in>S. (i \<circ> g \<circ> r) x = x"
+ proof (rule FP)
+ show "continuous_on S (i \<circ> g \<circ> r)"
+ by (meson contt contr assms(4) contg assms(8) continuous_on_compose continuous_on_subset)
+ show "(i \<circ> g \<circ> r) ` S \<subseteq> S"
+ using assms(2,4,8) by force
+ qed
+ then obtain x where x: "x \<in> S" "(i \<circ> g \<circ> r) x = x" ..
+ then have *: "g (r x) \<in> T"
+ using assms(4,8) by auto
+ have "r ((i \<circ> g \<circ> r) x) = r x"
+ using x by auto
+ then show ?thesis
+ using "*" ri that by auto
+qed
+
+lemma homeomorphic_fixpoint_property:
+ fixes S :: "'a::euclidean_space set"
+ and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T"
+ shows "(\<forall>f. continuous_on S f \<and> f ` S \<subseteq> S \<longrightarrow> (\<exists>x\<in>S. f x = x)) \<longleftrightarrow>
+ (\<forall>g. continuous_on T g \<and> g ` T \<subseteq> T \<longrightarrow> (\<exists>y\<in>T. g y = y))"
+ (is "?lhs = ?rhs")
+proof -
+ obtain r i where r:
+ "\<forall>x\<in>S. i (r x) = x" "r ` S = T" "continuous_on S r"
+ "\<forall>y\<in>T. r (i y) = y" "i ` T = S" "continuous_on T i"
+ using assms unfolding homeomorphic_def homeomorphism_def by blast
+ show ?thesis
+ proof
+ assume ?lhs
+ with r show ?rhs
+ by (metis invertible_fixpoint_property[of T i S r] order_refl)
+ next
+ assume ?rhs
+ with r show ?lhs
+ by (metis invertible_fixpoint_property[of S r T i] order_refl)
+ qed
+qed
+
+lemma retract_fixpoint_property:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ and S :: "'a set"
+ assumes "T retract_of S"
+ and FP: "\<And>f. \<lbrakk>continuous_on S f; f ` S \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. f x = x"
+ and contg: "continuous_on T g"
+ and "g ` T \<subseteq> T"
+ obtains y where "y \<in> T" and "g y = y"
+proof -
+ obtain h where "retraction S T h"
+ using assms(1) unfolding retract_of_def ..
+ then show ?thesis
+ unfolding retraction_def
+ using invertible_fixpoint_property[OF continuous_on_id _ _ _ _ FP]
+ by (metis assms(4) contg image_ident that)
+qed
+
+lemma retraction:
+ "retraction S T r \<longleftrightarrow>
+ T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
+ by (force simp: retraction_def)
+
+lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
+ assumes "retraction S T r"
+ obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
+proof (rule that)
+ from retraction [of S T r] assms
+ have "T \<subseteq> S" "continuous_on S r" "r ` S = T" and "\<forall>x \<in> T. r x = x"
+ by simp_all
+ then show "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r"
+ by simp_all
+ from \<open>\<forall>x \<in> T. r x = x\<close> have "r x = x" if "x \<in> T" for x
+ using that by simp
+ with \<open>r ` S = T\<close> show "r (r x) = r x" if "x \<in> S" for x
+ using that by auto
+qed
+
+lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
+ assumes "T retract_of S"
+ obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
+proof -
+ from assms obtain r where "retraction S T r"
+ by (auto simp add: retract_of_def)
+ with that show thesis
+ by (auto elim: retractionE)
+qed
+
+lemma retract_of_imp_extensible:
+ assumes "S retract_of T" and "continuous_on S f" and "f ` S \<subseteq> U"
+ obtains g where "continuous_on T g" "g ` T \<subseteq> U" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+ from \<open>S retract_of T\<close> obtain r where "retraction T S r"
+ by (auto simp add: retract_of_def)
+ show thesis
+ by (rule that [of "f \<circ> r"])
+ (use \<open>continuous_on S f\<close> \<open>f ` S \<subseteq> U\<close> \<open>retraction T S r\<close> in \<open>auto simp: continuous_on_compose2 retraction\<close>)
+qed
+
+lemma idempotent_imp_retraction:
+ assumes "continuous_on S f" and "f ` S \<subseteq> S" and "\<And>x. x \<in> S \<Longrightarrow> f(f x) = f x"
+ shows "retraction S (f ` S) f"
+by (simp add: assms retraction)
+
+lemma retraction_subset:
+ assumes "retraction S T r" and "T \<subseteq> s'" and "s' \<subseteq> S"
+ shows "retraction s' T r"
+ unfolding retraction_def
+ by (metis assms continuous_on_subset image_mono retraction)
+
+lemma retract_of_subset:
+ assumes "T retract_of S" and "T \<subseteq> s'" and "s' \<subseteq> S"
+ shows "T retract_of s'"
+by (meson assms retract_of_def retraction_subset)
+
+lemma retraction_refl [simp]: "retraction S S (\<lambda>x. x)"
+by (simp add: retraction)
+
+lemma retract_of_refl [iff]: "S retract_of S"
+ unfolding retract_of_def retraction_def
+ using continuous_on_id by blast
+
+lemma retract_of_imp_subset:
+ "S retract_of T \<Longrightarrow> S \<subseteq> T"
+by (simp add: retract_of_def retraction_def)
+
+lemma retract_of_empty [simp]:
+ "({} retract_of S) \<longleftrightarrow> S = {}" "(S retract_of {}) \<longleftrightarrow> S = {}"
+by (auto simp: retract_of_def retraction_def)
+
+lemma retract_of_singleton [iff]: "({x} retract_of S) \<longleftrightarrow> x \<in> S"
+ unfolding retract_of_def retraction_def by force
+
+lemma retraction_comp:
+ "\<lbrakk>retraction S T f; retraction T U g\<rbrakk>
+ \<Longrightarrow> retraction S U (g \<circ> f)"
+apply (auto simp: retraction_def intro: continuous_on_compose2)
+by blast
+
+lemma retract_of_trans [trans]:
+ assumes "S retract_of T" and "T retract_of U"
+ shows "S retract_of U"
+using assms by (auto simp: retract_of_def intro: retraction_comp)
+
+lemma closedin_retract:
+ fixes S :: "'a :: real_normed_vector set"
+ assumes "S retract_of T"
+ shows "closedin (subtopology euclidean T) S"
+proof -
+ obtain r where "S \<subseteq> T" "continuous_on T r" "r ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> r x = x"
+ using assms by (auto simp: retract_of_def retraction_def)
+ then have S: "S = {x \<in> T. (norm(r x - x)) = 0}" by auto
+ show ?thesis
+ apply (subst S)
+ apply (rule continuous_closedin_preimage_constant)
+ by (simp add: \<open>continuous_on T r\<close> continuous_on_diff continuous_on_norm)
+qed
+
+lemma closedin_self [simp]:
+ fixes S :: "'a :: real_normed_vector set"
+ shows "closedin (subtopology euclidean S) S"
+ by (simp add: closedin_retract)
+
+lemma retract_of_closed:
+ fixes S :: "'a :: real_normed_vector set"
+ shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
+ by (metis closedin_retract closedin_closed_eq)
+
+lemma retract_of_compact:
+ "\<lbrakk>compact T; S retract_of T\<rbrakk> \<Longrightarrow> compact S"
+ by (metis compact_continuous_image retract_of_def retraction)
+
+lemma retract_of_connected:
+ "\<lbrakk>connected T; S retract_of T\<rbrakk> \<Longrightarrow> connected S"
+ by (metis Topological_Spaces.connected_continuous_image retract_of_def retraction)
+
+lemma retraction_imp_quotient_map:
+ "openin (subtopology euclidean S) (S \<inter> r -` U) \<longleftrightarrow> openin (subtopology euclidean T) U"
+ if retraction: "retraction S T r" and "U \<subseteq> T"
+ using retraction apply (rule retractionE)
+ apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
+ using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
+ done
+
+lemma retract_of_Times:
+ "\<lbrakk>S retract_of s'; T retract_of t'\<rbrakk> \<Longrightarrow> (S \<times> T) retract_of (s' \<times> t')"
+apply (simp add: retract_of_def retraction_def Sigma_mono, clarify)
+apply (rename_tac f g)
+apply (rule_tac x="\<lambda>z. ((f \<circ> fst) z, (g \<circ> snd) z)" in exI)
+apply (rule conjI continuous_intros | erule continuous_on_subset | force)+
+done
+
+
end