diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Mar 21 19:46:26 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -84,7 +84,7 @@
     done
 qed
 
-lemma retraction_imp_quotient_map:
+lemma retraction_openin_vimage_iff:
   "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
   if retraction: "retraction S T r" and "U \<subseteq> T"
   using retraction apply (rule retractionE)
@@ -110,13 +110,13 @@
   assumes "locally connected T" "S retract_of T"
   shows "locally connected S"
   using assms
-  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image retract_ofE)
+  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
 
 lemma retract_of_locally_path_connected:
   assumes "locally path_connected T" "S retract_of T"
   shows "locally path_connected S"
   using assms
-  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image retract_ofE)
+  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
 
 text \<open>A few simple lemmas about deformation retracts\<close>