src/HOL/Analysis/Urysohn.thy

   have "T \<subseteq> mspace m1"
     using Tsub by (auto simp: mtopology_of_def closure_of_def)
   show ?thesis
     unfolding Lipschitz_continuous_map_pos
   proof
-    show "f ` mspace (submetric m1 T) \<subseteq> mspace m2"
-      by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist  mtopology_of_def mtopology_of_submetric)
+    show "f \<in> mspace (submetric m1 T) \<rightarrow> mspace m2"
+      by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist  mtopology_of_def 
+          mtopology_of_submetric image_subset_iff_funcset)
     define X where "X \<equiv> prod_topology (subtopology L.M1.mtopology T) (subtopology L.M1.mtopology T)"
     obtain B::real where "B > 0" and B: "\<forall>(x,y) \<in> S\<times>S. mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
       using lcf \<open>S \<subseteq> mspace m1\<close>  by (force simp: Lipschitz_continuous_map_pos)
     have eq: "{z \<in> A. case z of (x,y) \<Rightarrow> p x y \<le> B * q x y} = {z \<in> A. ((\<lambda>(x,y). B * q x y - p x y)z) \<in> {0..}}" 
         for p q and A::"('a*'a)set"

   have "T \<subseteq> mspace m1"
     using Tsub by (auto simp: mtopology_of_def closure_of_def)
   show ?thesis
     unfolding uniformly_continuous_map_def
     proof (intro conjI strip)
-    show "f ` mspace (submetric m1 T) \<subseteq> mspace m2"
-      by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist  mtopology_of_def mtopology_of_submetric)
+    show "f \<in> mspace (submetric m1 T) \<rightarrow> mspace m2"
+      by (metis cmf Metric_space.metric_continuous_map Metric_space_mspace_mdist  
+          mtopology_of_def mtopology_of_submetric image_subset_iff_funcset)
     fix \<epsilon>::real
     assume "\<epsilon> > 0"
     then obtain \<delta> where "\<delta>>0" and \<delta>: "\<forall>(x,y) \<in> S\<times>S. mdist m1 x y < \<delta> \<longrightarrow> mdist m2 (f x) (f y) \<le> \<epsilon>/2"
       using ucf \<open>S \<subseteq> mspace m1\<close> unfolding uniformly_continuous_map_def mspace_submetric
       apply (simp add: Ball_def del: divide_const_simps)

 definition cfunspace where
   "cfunspace X m \<equiv> submetric (funspace (topspace X) m) {f. continuous_map X (mtopology_of m) f}"
 
 lemma mspace_cfunspace [simp]:
   "mspace (cfunspace X m) = 
-     {f. f ` topspace X \<subseteq> mspace m \<and> f \<in> extensional (topspace X) \<and>
+     {f. f \<in> topspace X \<rightarrow> mspace m \<and> f \<in> extensional (topspace X) \<and>
          Metric_space.mbounded (mspace m) (mdist m) (f ` (topspace X)) \<and>
          continuous_map X (mtopology_of m) f}"
   by (auto simp: cfunspace_def Metric_space.fspace_def)
 
 lemma mdist_cfunspace_eq_mdist_funspace:

         by (metis assms mcomplete_funspace mcomplete_of_def mdist_Self mdist_funspace mspace_Self mspace_funspace)
       fix \<sigma> g
       assume g: "range \<sigma> \<subseteq> mspace (cfunspace X Self) \<and> limitin F.mtopology \<sigma> g sequentially"
       show "g \<in> mspace (cfunspace X Self)"
       proof (simp add: mtopology_of_def, intro conjI)
-        show "g ` topspace X \<subseteq> M" "g \<in> extensional (topspace X)" "mbounded (g ` topspace X)"
+        show "g \<in> topspace X \<rightarrow> M" "g \<in> extensional (topspace X)" "mbounded (g ` topspace X)"
           using g F.limitin_mspace by (force simp: fspace_def)+
         show "continuous_map X mtopology g"
           using * g by blast
       qed
     qed

 
 lemma (in Metric_space) metric_completion_explicit:
   obtains f :: "['a,'a] \<Rightarrow> real" and S where
       "S \<subseteq> mspace(funspace M euclidean_metric)"
       "mcomplete_of (submetric (funspace M euclidean_metric) S)"
-      "f ` M \<subseteq> S"
+      "f \<in> M \<rightarrow> S"
       "mtopology_of(funspace M euclidean_metric) closure_of f ` M = S"
       "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk>
             \<Longrightarrow> mdist (funspace M euclidean_metric) (f x) (f y) = d x y"
 proof -
   define m':: "('a\<Rightarrow>real) metric" where "m' \<equiv> funspace M euclidean_metric"

         by (simp add: S_def closedin_Int funspace_def)
       moreover have "S.mcomplete"
         using Metric_space.mcomplete_funspace Met_TC.Metric_space_axioms by (fastforce simp: mcomplete_of_def)
       ultimately show "mcomplete_of (submetric (funspace M euclidean_metric) S)"
         by (simp add: S.closedin_eq_mcomplete mcomplete_of_def)
-      show "f ` M \<subseteq> S"
+      show "f \<in> M \<rightarrow> S"
         using S_def fim in_closure_of m'_def by fastforce
       show "mtopology_of (funspace M euclidean_metric) closure_of f ` M = S"
         by (auto simp: f_def S_def mtopology_of_def)
       show "mdist (funspace M euclidean_metric) (f x) (f y) = d x y"
         if "x \<in> M" "y \<in> M" for x y

 
 
 lemma (in Metric_space) metric_completion:
   obtains f :: "['a,'a] \<Rightarrow> real" and m' where
     "mcomplete_of m'"
-    "f ` M \<subseteq> mspace m' "
+    "f \<in> M \<rightarrow> mspace m' "
     "mtopology_of m' closure_of f ` M = mspace m'"
     "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist m' (f x) (f y) = d x y"
 proof -
   obtain f :: "['a,'a] \<Rightarrow> real" and S where
     Ssub: "S \<subseteq> mspace(funspace M euclidean_metric)"
     and mcom: "mcomplete_of (submetric (funspace M euclidean_metric) S)"
-    and fim: "f ` M \<subseteq> S"
+    and fim: "f \<in> M \<rightarrow> S"
     and eqS: "mtopology_of(funspace M euclidean_metric) closure_of f ` M = S"
     and eqd: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist (funspace M euclidean_metric) (f x) (f y) = d x y"
     using metric_completion_explicit by metis
   define m' where "m' \<equiv> submetric (funspace M euclidean_metric) S"
   show thesis
   proof
     show "mcomplete_of m'"
       by (simp add: mcom m'_def)
-    show "f ` M \<subseteq> mspace m'"
+    show "f \<in> M \<rightarrow> mspace m'"
       using Ssub fim m'_def by auto
     show "mtopology_of m' closure_of f ` M = mspace m'"
       using eqS fim Ssub
-      by (force simp: m'_def mtopology_of_submetric closure_of_subtopology Int_absorb1)
+      by (force simp: m'_def mtopology_of_submetric closure_of_subtopology Int_absorb1 image_subset_iff_funcset)
     show "mdist m' (f x) (f y) = d x y" if "x \<in> M" and "y \<in> M" for x y
       using that eqd m'_def by force 
   qed 
 qed
 

   obtain M d where "Metric_space M d" and Xeq: "X = Metric_space.mtopology M d"
     using assms metrizable_space_def by blast
   then interpret Metric_space M d by simp
   obtain f :: "['a,'a] \<Rightarrow> real" and m' where
     "mcomplete_of m'"
-    and fim: "f ` M \<subseteq> mspace m' "
+    and fim: "f \<in> M \<rightarrow> mspace m' "
     and m': "mtopology_of m' closure_of f ` M = mspace m'"
     and eqd: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> mdist m' (f x) (f y) = d x y"
-    by (meson metric_completion)
+    by (metis metric_completion)
   show thesis
   proof
     show "completely_metrizable_space (mtopology_of m')"
       using \<open>mcomplete_of m'\<close>
       unfolding completely_metrizable_space_def mcomplete_of_def mtopology_of_def
       by (metis Metric_space_mspace_mdist)
     show "embedding_map X (mtopology_of m') f"
       using Metric_space12.isometry_imp_embedding_map
-      by (metis Metric_space12_def Metric_space_axioms Metric_space_mspace_mdist Xeq eqd fim mtopology_of_def)
+      by (metis Metric_space12_def Metric_space_axioms Metric_space_mspace_mdist Xeq eqd fim 
+             mtopology_of_def)
     show "(mtopology_of m') closure_of f ` topspace X = topspace (mtopology_of m')"
       by (simp add: Xeq m')
   qed
 qed
 

 
 subsection\<open>Contractions\<close>
 
 lemma (in Metric_space) contraction_imp_unique_fixpoint:
   assumes "f x = x" "f y = y"
-    and "f ` M \<subseteq> M"
+    and "f \<in> M \<rightarrow> M"
     and "k < 1"
     and "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> d (f x) (f y) \<le> k * d x y"
     and "x \<in> M" "y \<in> M"
   shows "x = y"
   by (smt (verit, ccfv_SIG) Metric_space.mdist_pos_less Metric_space_axioms assms mult_le_cancel_right1)
 
 text \<open>Banach Fixed-Point Theorem (aka, Contraction Mapping Principle)\<close>
 lemma (in Metric_space) Banach_fixedpoint_thm:
-  assumes mcomplete and "M \<noteq> {}" and fim: "f ` M \<subseteq> M"    
+  assumes mcomplete and "M \<noteq> {}" and fim: "f \<in> M \<rightarrow> M"    
     and "k < 1"
     and con: "\<And>x y. \<lbrakk>x \<in> M; y \<in> M\<rbrakk> \<Longrightarrow> d (f x) (f y) \<le> k * d x y"
   obtains x where "x \<in> M" "f x = x"
 proof -
   obtain a where "a \<in> M"
     using \<open>M \<noteq> {}\<close> by blast
   show thesis
   proof (cases "\<forall>x \<in> M. f x = f a")
     case True
     then show ?thesis
-      by (metis \<open>a \<in> M\<close> fim image_subset_iff that)
+      by (metis \<open>a \<in> M\<close> fim image_subset_iff image_subset_iff_funcset that)
   next
     case False
     then obtain b where "b \<in> M" and b: "f b \<noteq> f a"
       by blast
     have "k>0"

           show "range \<sigma> \<subseteq> M"
             using f_iter by blast
           fix \<epsilon>::real
           assume "\<epsilon>>0"
           with \<open>k < 1\<close> \<open>f a \<noteq> a\<close> \<open>a \<in> M\<close> fim have gt0: "((1 - k) * \<epsilon>) / d a (f a) > 0"
-            by (fastforce simp: divide_simps)
+            by (fastforce simp: divide_simps Pi_iff)
           obtain N where "k^N < ((1-k) * \<epsilon>) / d a (f a)"
             using real_arch_pow_inv [OF gt0 \<open>k < 1\<close>] by blast
           then have N: "\<And>n. n \<ge> N \<Longrightarrow> k^n < ((1-k) * \<epsilon>) / d a (f a)"
             by (smt (verit) \<open>0 < k\<close> assms(4) power_decreasing)
           have "\<forall>n n'. n<n' \<longrightarrow> N \<le> n \<longrightarrow> N \<le> n' \<longrightarrow> d (\<sigma> n) (\<sigma> n') < \<epsilon>"

 lemma completely_regular_space_cube_embedding_explicit:
   assumes "completely_regular_space X" "Hausdorff_space X"
   shows "embedding_map X
              (product_topology (\<lambda>f. top_of_set {0..1::real})
                 (mspace (submetric (cfunspace X euclidean_metric)
-                  {f. f ` topspace X \<subseteq> {0..1}})) )
-             (\<lambda>x. \<lambda>f \<in> mspace (submetric (cfunspace X euclidean_metric) {f. f ` topspace X \<subseteq> {0..1}}).
+                  {f. f \<in> topspace X \<rightarrow> {0..1}})) )
+             (\<lambda>x. \<lambda>f \<in> mspace (submetric (cfunspace X euclidean_metric) {f. f \<in> topspace X \<rightarrow> {0..1}}).
               f x)"
 proof -
-  define K where "K \<equiv> mspace(submetric (cfunspace X euclidean_metric) {f. f ` topspace X \<subseteq> {0..1::real}})"
+  define K where "K \<equiv> mspace(submetric (cfunspace X euclidean_metric) {f. f \<in> topspace X \<rightarrow> {0..1::real}})"
   define e where "e \<equiv> \<lambda>x. \<lambda>f\<in>K. f x"
   have "e x \<noteq> e y" if xy: "x \<noteq> y" "x \<in> topspace X" "y \<in> topspace X" for x y
   proof -
     have "closedin X {x}"
       by (simp add: \<open>Hausdorff_space X\<close> closedin_Hausdorff_singleton \<open>x \<in> topspace X\<close>)

   proof (clarsimp simp add: continuous_map_atin limitin_atin openin_subtopology_alt e')
     fix x U
     assume "e x \<in> K \<rightarrow>\<^sub>E {0..1}" and "x \<in> topspace X" and "openin X U" and "x \<in> U"
     then obtain g where contg: "continuous_map X (top_of_set {0..1}) g" and "g x = 0" 
           and gim: "g ` (topspace X - U) \<subseteq> {1::real}"
-      using \<open>completely_regular_space X\<close> unfolding completely_regular_space_def
+      using \<open>completely_regular_space X\<close> unfolding completely_regular_space_def 
       by (metis Diff_iff openin_closedin_eq)
     then have "bounded (g ` topspace X)"
       by (meson bounded_closed_interval bounded_subset continuous_map_in_subtopology)
-    moreover have "g ` topspace X \<subseteq> {0..1}"
-      using contg by (simp add: continuous_map_in_subtopology)
+    moreover have "g \<in> topspace X \<rightarrow> {0..1}"
+      using contg by (simp add: continuous_map_def)
     ultimately have g_in_K: "restrict g (topspace X) \<in> K"
-      using contg by (simp add: K_def continuous_map_in_subtopology)
+      using contg by (force simp add: K_def continuous_map_in_subtopology)
     have "openin (top_of_set {0..1}) {0..<1::real}"
       using open_real_greaterThanLessThan[of "-1" 1] by (force simp: openin_open)
     moreover have "e x \<in> (\<Pi>\<^sub>E f\<in>K. if f = restrict g (topspace X) then {0..<1} else {0..1})"
       using \<open>e x \<in> K \<rightarrow>\<^sub>E {0..1}\<close> by (simp add: e_def \<open>g x = 0\<close> \<open>x \<in> topspace X\<close> PiE_iff)
     moreover have "e y = e x"