# HG changeset patch
# User immler <immler@in.tum.de>
# Date 1548443959 18000
# Node ID ac9704fd0935eb61eed408602257dd79fb7689ed
# Parent  18d383f41477940818c3128ee99d1a10a53f804c
generalized

diff -r 18d383f41477 -r ac9704fd0935 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Jan 25 15:57:24 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Jan 25 14:19:19 2019 -0500
@@ -2359,8 +2359,8 @@
 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"
+  fixes S :: "'a::topological_space set"
+    and T :: "'b::topological_space set"
   assumes contt: "continuous_on T i"
     and "i ` T \<subseteq> S"
     and contr: "continuous_on S r"
@@ -2388,8 +2388,8 @@
 qed
 
 lemma homeomorphic_fixpoint_property:
-  fixes S :: "'a::euclidean_space set"
-    and T :: "'b::euclidean_space set"
+  fixes S :: "'a::topological_space set"
+    and T :: "'b::topological_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))"
@@ -2412,7 +2412,7 @@
 qed
 
 lemma retract_fixpoint_property:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_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"
@@ -2515,26 +2515,28 @@
 using assms by (auto simp: retract_of_def intro: retraction_comp)
 
 lemma closedin_retract:
-  fixes S :: "'a :: real_normed_vector set"
+  fixes S :: "'a :: t2_space 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"
+  obtain r where r: "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)
+  have "S = {x\<in>T. x = r x}"
+    using r by auto
+  also have "\<dots> = T \<inter> ((\<lambda>x. (x, r x)) -` ({y. \<exists>x. y = (x, x)}))"
+    unfolding vimage_def mem_Times_iff fst_conv snd_conv
+    using r
+    by auto
+  also have "closedin (top_of_set T) \<dots>"
+    by (rule continuous_closedin_preimage) (auto intro!: closed_diagonal continuous_on_Pair r)
+  finally show ?thesis .
 qed
 
-lemma closedin_self [simp]:
-    fixes S :: "'a :: real_normed_vector set"
-    shows "closedin (subtopology euclidean S) S"
-  by (simp add: closedin_retract)
+lemma closedin_self [simp]: "closedin (subtopology euclidean S) S"
+  by simp
 
 lemma retract_of_closed:
-    fixes S :: "'a :: real_normed_vector set"
+    fixes S :: "'a :: t2_space set"
     shows "\<lbrakk>closed T; S retract_of T\<rbrakk> \<Longrightarrow> closed S"
   by (metis closedin_retract closedin_closed_eq)