diff -r b67bab2b132c -r 4900351361b0 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Apr 16 19:50:30 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Wed Apr 17 17:48:28 2019 +0100
@@ -1107,7 +1107,7 @@
     "\<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:
+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)