diff -r 3529946fca19 -r b022c013b04b src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Mar 23 19:26:23 2025 +0000
@@ -1567,12 +1567,12 @@
     by (smt (verit, ccfv_threshold) assms continuous_map image_eqI image_subset_iff in_closure_of mem_Collect_eq)
 qed
 
-lemma continuous_map_subset_aux1: "continuous_map X Y f \<Longrightarrow>
-       (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+lemma continuous_map_subset_aux1: 
+  "continuous_map X Y f \<Longrightarrow> (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
   using continuous_map_image_closure_subset by blast
 
 lemma continuous_map_subset_aux2:
-  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S"
+  assumes "\<forall>S. S \<subseteq> topspace X \<longrightarrow> f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S"
   shows "continuous_map X Y f"
   unfolding continuous_map_closedin
 proof (intro conjI ballI allI impI)
@@ -1598,18 +1598,18 @@
 qed
 
 lemma continuous_map_eq_image_closure_subset:
-     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
 
 lemma continuous_map_eq_image_closure_subset_alt:
-     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
+     "continuous_map X Y f \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
   using continuous_map_subset_aux1 continuous_map_subset_aux2 by metis
 
 lemma continuous_map_eq_image_closure_subset_gen:
      "continuous_map X Y f \<longleftrightarrow>
         f \<in> topspace X \<rightarrow> topspace Y \<and>
-        (\<forall>S. f ` (X closure_of S) \<subseteq> Y closure_of f ` S)"
-  by (meson Pi_iff continuous_map continuous_map_eq_image_closure_subset image_subset_iff)
+        (\<forall>S. f \<in> (X closure_of S) \<rightarrow> Y closure_of f ` S)"
+  by (metis continuous_map_eq_image_closure_subset continuous_map_funspace)
 
 lemma continuous_map_closure_preimage_subset:
    "continuous_map X Y f
@@ -1697,16 +1697,18 @@
   by (auto simp: elim!: continuous_map_eq)
 
 lemma continuous_map_in_subtopology:
-  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f ` (topspace X) \<subseteq> S"
+  "continuous_map X (subtopology X' S) f \<longleftrightarrow> continuous_map X X' f \<and> f \<in> (topspace X) \<rightarrow> S"
   (is "?lhs = ?rhs")
 proof
   assume L: ?lhs
   show ?rhs
   proof -
-    have "\<And>A. f ` (X closure_of A) \<subseteq> subtopology X' S closure_of f ` A"
-      by (meson L continuous_map_image_closure_subset)
+    have "\<And>A. f \<in> (X closure_of A) \<rightarrow> subtopology X' S closure_of f ` A"
+      by (metis L continuous_map_eq_image_closure_subset image_subset_iff_funcset)
     then show ?thesis
-      by (metis (no_types) closure_of_subset_subtopology closure_of_subtopology_subset closure_of_topspace continuous_map_eq_image_closure_subset order.trans)
+      by (metis closure_of_subset_subtopology closure_of_subtopology_subset
+          closure_of_topspace continuous_map_eq_image_closure_subset
+          image_subset_iff_funcset subset_trans)
   qed
 next
   assume R: ?rhs
@@ -3963,7 +3965,7 @@
 proof
   show "?lhs \<Longrightarrow> ?rhs"
     unfolding embedding_map_def
-    by (metis continuous_map_in_subtopology homeomorphic_imp_continuous_map inf_absorb2 subtopology_subtopology)
+    by (metis Int_subset_iff homeomorphic_imp_surjective_map inf_le1 subtopology_restrict subtopology_subtopology topspace_subtopology)
 qed (simp add: embedding_map_def inf.absorb_iff2 subtopology_subtopology)
 
 lemma injective_open_imp_embedding_map:
@@ -4118,13 +4120,13 @@
   using assms continuous_on_closed by blast
 
 lemma continuous_map_subtopology_eu [simp]:
-  "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h ` S \<subseteq> T"
+  "continuous_map (top_of_set S) (subtopology euclidean T) h \<longleftrightarrow> continuous_on S h \<and> h \<in> S \<rightarrow> T"
   by (simp add: continuous_map_in_subtopology)
 
 lemma continuous_map_euclidean_top_of_set:
   assumes eq: "f -` S = UNIV" and cont: "continuous_on UNIV f"
   shows "continuous_map euclidean (top_of_set S) f"
-  by (simp add: cont continuous_map_in_subtopology eq image_subset_iff_subset_vimage)
+  using cont continuous_map_iff_continuous2 continuous_map_into_subtopology eq by blast
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Half-global and completely global cases\<close>
@@ -4166,25 +4168,14 @@
   by (metis Int_commute closedin_closed continuous_on_closed_invariant)
 
 lemma continuous_open_preimage:
-  assumes contf: "continuous_on S f" and "open S" "open T"
+  assumes "continuous_on S f" and "open S" "open T"
   shows "open (S \<inter> f -` T)"
-proof-
-  obtain U where "open U" "(S \<inter> f -` T) = S \<inter> U"
-    using continuous_openin_preimage_gen[OF contf \<open>open T\<close>]
-    unfolding openin_open by auto
-  then show ?thesis
-    using open_Int[of S U, OF \<open>open S\<close>] by auto
-qed
+  by (metis Int_commute assms continuous_on_open_vimage)
 
 lemma continuous_closed_preimage:
-  assumes contf: "continuous_on S f" and "closed S" "closed T"
+  assumes "continuous_on S f" and "closed S" "closed T"
   shows "closed (S \<inter> f -` T)"
-proof-
-  obtain U where "closed U" "(S \<inter> f -` T) = S \<inter> U"
-    using continuous_closedin_preimage[OF contf \<open>closed T\<close>]
-    unfolding closedin_closed by auto
-  then show ?thesis using closed_Int[of S U, OF \<open>closed S\<close>] by auto
-qed
+  by (metis assms closed_vimage_Int inf_commute)
 
 lemma continuous_open_vimage: "open S \<Longrightarrow> (\<And>x. continuous (at x) f) \<Longrightarrow> open (f -` S)"
   by (metis continuous_on_eq_continuous_within open_vimage)