diff -r 2594319ad9ee -r 37894dff0111 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu May 11 22:12:43 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon May 15 17:12:18 2023 +0100
@@ -296,6 +296,10 @@
   unfolding closedin_def topspace_subtopology
   by (auto simp: openin_subtopology)
 
+lemma closedin_subset_topspace:
+   "\<lbrakk>closedin X S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology X T) S"
+  using closedin_subtopology by fastforce
+
 lemma closedin_relative_to:
    "(closedin X relative_to S) = closedin (subtopology X S)"
   by (force simp: relative_to_def closedin_subtopology)
@@ -3378,6 +3382,10 @@
   qed
 qed
 
+lemma connected_space_quotient_map_image:
+   "\<lbrakk>quotient_map X X' q; connected_space X\<rbrakk> \<Longrightarrow> connected_space X'"
+  by (metis connectedin_continuous_map_image connectedin_topspace quotient_imp_continuous_map quotient_imp_surjective_map)
+
 lemma homeomorphic_connected_space:
      "X homeomorphic_space Y \<Longrightarrow> connected_space X \<longleftrightarrow> connected_space Y"
   unfolding homeomorphic_space_def homeomorphic_maps_def