# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1685617713 -3600
# Node ID 1cadc477f644c89c0fae513f51ff81f4af684c1d
# Parent  8234c42d20e64ee90644b7fec3e795d3611c912f
Even more material from the HOL Light metric space library

diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Analysis/Abstract_Metric_Spaces.thy
--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -542,6 +542,9 @@
 lemma mdist_euclidean_metric [simp]: "mdist euclidean_metric = dist"
   by (simp add: euclidean_metric_def)
 
+lemma mtopology_of_euclidean [simp]: "mtopology_of euclidean_metric = euclidean"
+  by (simp add: Met_TC.mtopology_def mtopology_of_def)
+
 text\<open> Subspace of a metric space\<close>
 
 definition submetric where
@@ -570,6 +573,16 @@
    "submetric m S = submetric m (mspace m \<inter> S)"
   by (metis submetric_mspace submetric_submetric)
 
+lemma mtopology_of_submetric: "mtopology_of (submetric m A) = subtopology (mtopology_of m) A"
+proof -
+  interpret Submetric "mspace m" "mdist m" "A \<inter> mspace m"
+    using Metric_space_mspace_mdist Submetric.intro Submetric_axioms.intro inf_le2 by blast
+  have "sub.mtopology = subtopology (mtopology_of m) A"
+    by (metis inf_commute mtopology_of_def mtopology_submetric subtopology_mspace subtopology_subtopology)
+  then show ?thesis
+    by (simp add: submetric_def)
+qed
+
 
 subsection\<open>The discrete metric\<close>
 
@@ -809,35 +822,6 @@
    "\<lbrakk>metrizable_space X; openin X S\<rbrakk> \<Longrightarrow> fsigma_in X S"
   by (meson closed_imp_gdelta_in fsigma_in_gdelta_in openin_closedin openin_subset)
 
-(*NEEDS first_countable
-lemma first_countable_mtopology:
-   "first_countable mtopology"
-oops
-  GEN_TAC THEN REWRITE_TAC[first_countable; TOPSPACE_MTOPOLOGY] THEN
-  X_GEN_TAC `x::A` THEN DISCH_TAC THEN
-  EXISTS_TAC `{ mball m (x::A,r) | rational r \<and> 0 < r}` THEN
-  REWRITE_TAC[FORALL_IN_GSPEC; OPEN_IN_MBALL; EXISTS_IN_GSPEC] THEN
-  ONCE_REWRITE_TAC[SET_RULE
-   `{f x | S x \<and> Q x} = f ` {x \<in> S. Q x}`] THEN
-  SIMP_TAC[COUNTABLE_IMAGE; COUNTABLE_RATIONAL; COUNTABLE_RESTRICT] THEN
-  REWRITE_TAC[OPEN_IN_MTOPOLOGY] THEN
-  X_GEN_TAC `U::A=>bool` THEN STRIP_TAC THEN
-  FIRST_X_ASSUM(MP_TAC \<circ> SPEC `x::A`) THEN
-  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
-  X_GEN_TAC `r::real` THEN STRIP_TAC THEN FIRST_ASSUM
-   (MP_TAC \<circ> SPEC `r::real` \<circ> MATCH_MP RATIONAL_APPROXIMATION_BELOW) THEN
-  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `q::real` THEN
-  REWRITE_TAC[REAL_SUB_REFL] THEN STRIP_TAC THEN
-  ASM_SIMP_TAC[CENTRE_IN_MBALL] THEN
-  TRANS_TAC SUBSET_TRANS `mball m (x::A,r)` THEN
-  ASM_SIMP_TAC[MBALL_SUBSET_CONCENTRIC; REAL_LT_IMP_LE]);;
-
-lemma metrizable_imp_first_countable:
-   "metrizable_space X \<Longrightarrow> first_countable X"
-oops
-  REWRITE_TAC[FORALL_METRIZABLE_SPACE; FIRST_COUNTABLE_MTOPOLOGY]);;
-*)
-
 lemma mball_eq_ball [simp]: "Met_TC.mball = ball"
   by force
 
@@ -2950,7 +2934,14 @@
   "mdist (prod_metric m1 m2) = prod_dist (mdist m1) (mdist m2)"
   by (metis Metric_space.mdist_metric Metric_space12.prod_metric Metric_space12_mspace_mdist prod_metric_def)
 
-context Metric_space12 
+lemma prod_dist_dist [simp]: "prod_dist dist dist = dist"
+  by (simp add: prod_dist_def dist_prod_def fun_eq_iff)
+
+lemma prod_metric_euclidean [simp]:
+  "prod_metric euclidean_metric euclidean_metric = euclidean_metric"
+  by (simp add: prod_metric_def euclidean_metric_def)
+
+context Metric_space12
 begin
 
 lemma component_le_prod_metric:
@@ -3343,6 +3334,1232 @@
 qed (simp add: empty_completely_metrizable_space)
 
 
+subsection \<open>The "atin-within" filter for topologies\<close>
+
+(*FIXME: replace original definition of atin to be an abbreviation, like at / at_within
+    ("atin (_) (_)/ within (_)" [1000, 60] 60)*)
+definition atin_within :: "['a topology, 'a, 'a set] \<Rightarrow> 'a filter"
+  where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \<inter> S - {a}))"
+
+lemma atin_within_UNIV [simp]:
+  shows "atin_within X a UNIV = atin X a"
+  by (simp add: atin_def atin_within_def)
+
+lemma eventually_atin_subtopology:
+  assumes "a \<in> topspace X"
+  shows "eventually P (atin (subtopology X S) a) \<longleftrightarrow> 
+    (a \<in> S \<longrightarrow> (\<exists>U. openin (subtopology X S) U \<and> a \<in> U \<and> (\<forall>x\<in>U - {a}. P x)))"
+  using assms by (simp add: eventually_atin)
+
+lemma eventually_atin_within:
+  "eventually P (atin_within X a S) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+proof (cases "a \<in> topspace X")
+  case True
+  hence "eventually P (atin_within X a S) \<longleftrightarrow> 
+         (\<exists>T. openin X T \<and> a \<in> T \<and>
+          (\<forall>x\<in>T. x \<in> topspace X \<and> x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+    by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
+  also have "\<dots> \<longleftrightarrow> (\<exists>T. openin X T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
+    using openin_subset by (intro ex_cong) auto
+  finally show ?thesis by (simp add: True)
+qed (simp add: atin_within_def)
+
+lemma atin_subtopology_within:
+  assumes "a \<in> S"
+  shows "atin (subtopology X S) a = atin_within X a S"
+proof -
+  have "eventually P (atin (subtopology X S) a) \<longleftrightarrow> eventually P (atin_within X a S)" for P
+    unfolding eventually_atin eventually_atin_within openin_subtopology
+    using assms by auto
+  then show ?thesis
+    by (meson le_filter_def order.eq_iff)
+qed
+
+lemma limit_continuous_map_within:
+   "\<lbrakk>continuous_map (subtopology X S) Y f; a \<in> S; a \<in> topspace X\<rbrakk>
+    \<Longrightarrow> limitin Y f (f a) (atin_within X a S)"
+  by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)
+
+lemma atin_subtopology_within_if:
+  shows "atin (subtopology X S) a = (if a \<in> S then atin_within X a S else bot)"
+  by (simp add: atin_subtopology_within)
+
+lemma trivial_limit_atpointof_within:
+   "trivial_limit(atin_within X a S) \<longleftrightarrow>
+        (a \<notin> X derived_set_of S)"
+  by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)
+
+lemma derived_set_of_trivial_limit:
+   "a \<in> X derived_set_of S \<longleftrightarrow> \<not> trivial_limit(atin_within X a S)"
+  by (simp add: trivial_limit_atpointof_within)
+
+    
+subsection\<open>More sequential characterizations in a metric space\<close>
+
+context Metric_space
+begin
+  
+definition decreasing_dist :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
+    where "decreasing_dist \<sigma> x \<equiv> (\<forall>m n. m < n \<longrightarrow> d (\<sigma> n) x < d (\<sigma> m) x)"
+
+lemma decreasing_dist_imp_inj: "decreasing_dist \<sigma> a \<Longrightarrow> inj \<sigma>"
+  by (metis decreasing_dist_def dual_order.irrefl linorder_inj_onI')
+
+lemma eventually_atin_within_metric:
+   "eventually P (atin_within mtopology a S) \<longleftrightarrow>
+    (a \<in> M \<longrightarrow> (\<exists>\<delta>>0. \<forall>x. x \<in> M \<and> x \<in> S \<and> 0 < d x a \<and> d x a < \<delta> \<longrightarrow> P x))" (is "?lhs=?rhs")
+proof
+  assume ?lhs then show ?rhs
+unfolding eventually_atin_within openin_mtopology subset_iff
+  by (metis commute in_mball mdist_zero order_less_irrefl topspace_mtopology)
+next
+  assume R: ?rhs 
+  show ?lhs
+  proof (cases "a \<in> M")
+    case True
+    then obtain \<delta> where "\<delta> > 0" and \<delta>: "\<And>x. \<lbrakk>x \<in> M; x \<in> S; 0 < d x a; d x a < \<delta>\<rbrakk> \<Longrightarrow> P x"
+      using R by blast
+    then have "openin mtopology (mball a \<delta>) \<and> (\<forall>x \<in> mball a \<delta>. x \<in> S \<and> x \<noteq> a \<longrightarrow> P x)"
+      by (simp add: commute openin_mball)
+    then show ?thesis
+      by (metis True \<open>0 < \<delta>\<close> centre_in_mball_iff eventually_atin_within) 
+  next
+    case False
+    with R show ?thesis
+      by (simp add: eventually_atin_within)
+  qed
+qed
+
+
+lemma eventually_atin_within_A:
+  assumes 
+    "(\<And>\<sigma>. \<lbrakk>range \<sigma> \<subseteq> (S \<inter> M) - {a}; decreasing_dist \<sigma> a;
+          inj \<sigma>; limitin mtopology \<sigma> a sequentially\<rbrakk>
+      \<Longrightarrow> eventually (\<lambda>n. P (\<sigma> n)) sequentially)"
+  shows "eventually P (atin_within mtopology a S)"
+proof -
+  have False if SP: "\<And>\<delta>. \<delta>>0 \<Longrightarrow> \<exists>x \<in> M-{a}. d x a < \<delta> \<and> x \<in> S \<and> \<not> P x" and "a \<in> M"
+  proof -
+    define \<Phi> where "\<Phi> \<equiv> \<lambda>n x. x \<in> M-{a} \<and> d x a < inverse (Suc n) \<and> x \<in> S \<and> \<not> P x"
+    obtain \<sigma> where \<sigma>: "\<And>n. \<Phi> n (\<sigma> n)" and dless: "\<And>n. d (\<sigma>(Suc n)) a < d (\<sigma> n) a"
+    proof -
+      obtain x0 where x0: "\<Phi> 0 x0"
+        using SP [OF zero_less_one] by (force simp: \<Phi>_def)
+      have "\<exists>y. \<Phi> (Suc n) y \<and> d y a < d x a" if "\<Phi> n x" for n x
+        using SP [of "min (inverse (Suc (Suc n))) (d x a)"] \<open>a \<in> M\<close> that
+        by (auto simp: \<Phi>_def)
+      then obtain f where f: "\<And>n x. \<Phi> n x \<Longrightarrow> \<Phi> (Suc n) (f n x) \<and> d (f n x) a < d x a" 
+        by metis
+      show thesis
+        proof
+          show "\<Phi> n (rec_nat x0 f n)" for n
+            by (induction n) (auto simp: x0 dest: f)
+          with f show "d (rec_nat x0 f (Suc n)) a < d (rec_nat x0 f n) a" for n
+            by auto 
+        qed
+    qed
+    have 1: "range \<sigma> \<subseteq> (S \<inter> M) - {a}"
+      using \<sigma> by (auto simp: \<Phi>_def)
+    have "d (\<sigma>(Suc (m+n))) a < d (\<sigma> n) a" for m n
+      by (induction m) (auto intro: order_less_trans dless)
+    then have 2: "decreasing_dist \<sigma> a"
+      unfolding decreasing_dist_def by (metis add.commute less_imp_Suc_add)
+    have "\<forall>\<^sub>F xa in sequentially. d (\<sigma> xa) a < \<epsilon>" if "\<epsilon> > 0" for \<epsilon>
+    proof -
+      obtain N where "inverse (Suc N) < \<epsilon>"
+        using \<open>\<epsilon> > 0\<close> reals_Archimedean by blast
+      with \<sigma> 2 show ?thesis
+        unfolding decreasing_dist_def by (smt (verit, best) \<Phi>_def eventually_at_top_dense)
+    qed
+    then have 4: "limitin mtopology \<sigma> a sequentially"
+      using \<sigma> \<open>a \<in> M\<close> by (simp add: \<Phi>_def limitin_metric)
+    show False
+      using 2 assms [OF 1 _ decreasing_dist_imp_inj 4] \<sigma> by (force simp: \<Phi>_def)
+  qed
+  then show ?thesis
+    by (fastforce simp: eventually_atin_within_metric)
+qed
+
+
+lemma eventually_atin_within_B:
+  assumes ev: "eventually P (atin_within mtopology a S)" 
+    and ran: "range \<sigma> \<subseteq> (S \<inter> M) - {a}"
+    and lim: "limitin mtopology \<sigma> a sequentially"
+  shows "eventually (\<lambda>n. P (\<sigma> n)) sequentially"
+proof -
+  have "a \<in> M"
+    using lim limitin_mspace by auto
+  with ev obtain \<delta> where "0 < \<delta>" 
+    and \<delta>: "\<And>\<sigma>. \<lbrakk>\<sigma> \<in> M; \<sigma> \<in> S; 0 < d \<sigma> a; d \<sigma> a < \<delta>\<rbrakk> \<Longrightarrow> P \<sigma>"
+    by (auto simp: eventually_atin_within_metric)
+  then have *: "\<And>n. \<sigma> n \<in> M \<and> d (\<sigma> n) a < \<delta> \<Longrightarrow> P (\<sigma> n)"
+    using \<open>a \<in> M\<close> ran by auto
+  have "\<forall>\<^sub>F n in sequentially. \<sigma> n \<in> M \<and> d (\<sigma> n) a < \<delta>"
+    using lim \<open>0 < \<delta>\<close> by (auto simp: limitin_metric)
+  then show ?thesis
+    by (simp add: "*" eventually_mono)
+qed
+
+lemma eventually_atin_within_sequentially:
+     "eventually P (atin_within mtopology a S) \<longleftrightarrow>
+        (\<forall>\<sigma>. range \<sigma> \<subseteq> (S \<inter> M) - {a} \<and>
+            limitin mtopology \<sigma> a sequentially
+            \<longrightarrow> eventually (\<lambda>n. P(\<sigma> n)) sequentially)"
+  by (metis eventually_atin_within_A eventually_atin_within_B)
+
+lemma eventually_atin_within_sequentially_inj:
+     "eventually P (atin_within mtopology a S) \<longleftrightarrow>
+        (\<forall>\<sigma>. range \<sigma> \<subseteq> (S \<inter> M) - {a} \<and> inj \<sigma> \<and>
+            limitin mtopology \<sigma> a sequentially
+            \<longrightarrow> eventually (\<lambda>n. P(\<sigma> n)) sequentially)"
+  by (metis eventually_atin_within_A eventually_atin_within_B)
+
+lemma eventually_atin_within_sequentially_decreasing:
+     "eventually P (atin_within mtopology a S) \<longleftrightarrow>
+        (\<forall>\<sigma>. range \<sigma> \<subseteq> (S \<inter> M) - {a} \<and> decreasing_dist \<sigma> a \<and>
+            limitin mtopology \<sigma> a sequentially
+            \<longrightarrow> eventually (\<lambda>n. P(\<sigma> n)) sequentially)"
+  by (metis eventually_atin_within_A eventually_atin_within_B)
+
+
+lemma eventually_atin_sequentially:
+   "eventually P (atin mtopology a) \<longleftrightarrow>
+    (\<forall>\<sigma>. range \<sigma> \<subseteq> M - {a} \<and> limitin mtopology \<sigma> a sequentially
+         \<longrightarrow> eventually (\<lambda>n. P(\<sigma> n)) sequentially)"
+  using eventually_atin_within_sequentially [where S=UNIV] by simp
+
+lemma eventually_atin_sequentially_inj:
+   "eventually P (atin mtopology a) \<longleftrightarrow>
+    (\<forall>\<sigma>. range \<sigma> \<subseteq> M - {a} \<and> inj \<sigma> \<and>
+        limitin mtopology \<sigma> a sequentially
+        \<longrightarrow> eventually (\<lambda>n. P(\<sigma> n)) sequentially)"
+  using eventually_atin_within_sequentially_inj [where S=UNIV] by simp
+
+lemma eventually_atin_sequentially_decreasing:
+   "eventually P (atin mtopology a) \<longleftrightarrow>
+    (\<forall>\<sigma>. range \<sigma> \<subseteq> M - {a} \<and> decreasing_dist \<sigma> a \<and>
+         limitin mtopology \<sigma> a sequentially
+        \<longrightarrow> eventually (\<lambda>n. P(\<sigma> n)) sequentially)"
+  using eventually_atin_within_sequentially_decreasing [where S=UNIV] by simp
+
+end
+
+context Metric_space12
+begin
+
+lemma limit_atin_sequentially_within:
+  "limitin M2.mtopology f l (atin_within M1.mtopology a S) \<longleftrightarrow>
+     l \<in> M2 \<and>
+     (\<forall>\<sigma>. range \<sigma> \<subseteq> S \<inter> M1 - {a} \<and>
+          limitin M1.mtopology \<sigma> a sequentially
+          \<longrightarrow> limitin M2.mtopology (f \<circ> \<sigma>) l sequentially)"
+    by (auto simp: M1.eventually_atin_within_sequentially limitin_def)
+
+lemma limit_atin_sequentially_within_inj:
+  "limitin M2.mtopology f l (atin_within M1.mtopology a S) \<longleftrightarrow>
+     l \<in> M2 \<and>
+     (\<forall>\<sigma>. range \<sigma> \<subseteq> S \<inter> M1 - {a} \<and> inj \<sigma> \<and>
+          limitin M1.mtopology \<sigma> a sequentially
+          \<longrightarrow> limitin M2.mtopology (f \<circ> \<sigma>) l sequentially)"
+    by (auto simp: M1.eventually_atin_within_sequentially_inj limitin_def)
+
+lemma limit_atin_sequentially_within_decreasing:
+  "limitin M2.mtopology f l (atin_within M1.mtopology a S) \<longleftrightarrow>
+     l \<in> M2 \<and>
+     (\<forall>\<sigma>. range \<sigma> \<subseteq> S \<inter> M1 - {a} \<and> M1.decreasing_dist \<sigma> a \<and> 
+          limitin M1.mtopology \<sigma> a sequentially
+          \<longrightarrow> limitin M2.mtopology (f \<circ> \<sigma>) l sequentially)"
+    by (auto simp: M1.eventually_atin_within_sequentially_decreasing limitin_def)
+
+lemma limit_atin_sequentially:
+   "limitin M2.mtopology f l (atin M1.mtopology a) \<longleftrightarrow>
+        l \<in> M2 \<and>
+        (\<forall>\<sigma>. range \<sigma> \<subseteq> M1 - {a} \<and>
+            limitin M1.mtopology \<sigma> a sequentially
+            \<longrightarrow> limitin M2.mtopology (f \<circ> \<sigma>) l sequentially)"
+  using limit_atin_sequentially_within [where S=UNIV] by simp
+
+lemma limit_atin_sequentially_inj:
+   "limitin M2.mtopology f l (atin M1.mtopology a) \<longleftrightarrow>
+        l \<in> M2 \<and>
+        (\<forall>\<sigma>. range \<sigma> \<subseteq> M1 - {a} \<and> inj \<sigma> \<and>
+            limitin M1.mtopology \<sigma> a sequentially
+            \<longrightarrow> limitin M2.mtopology (f \<circ> \<sigma>) l sequentially)"
+  using limit_atin_sequentially_within_inj [where S=UNIV] by simp
+
+lemma limit_atin_sequentially_decreasing:
+  "limitin M2.mtopology f l (atin M1.mtopology a) \<longleftrightarrow>
+     l \<in> M2 \<and>
+     (\<forall>\<sigma>. range \<sigma> \<subseteq> M1 - {a} \<and> M1.decreasing_dist \<sigma> a \<and> 
+          limitin M1.mtopology \<sigma> a sequentially
+          \<longrightarrow> limitin M2.mtopology (f \<circ> \<sigma>) l sequentially)"
+  using limit_atin_sequentially_within_decreasing [where S=UNIV] by simp
 
 end
 
+text \<open>An experiment: same result as within the locale, but using metric space variables\<close>
+lemma limit_atin_sequentially_within:
+  "limitin (mtopology_of m2) f l (atin_within (mtopology_of m1) a S) \<longleftrightarrow>
+     l \<in> mspace m2 \<and>
+     (\<forall>\<sigma>. range \<sigma> \<subseteq> S \<inter> mspace m1 - {a} \<and>
+          limitin (mtopology_of m1) \<sigma> a sequentially
+          \<longrightarrow> limitin (mtopology_of m2) (f \<circ> \<sigma>) l sequentially)"
+  using Metric_space12.limit_atin_sequentially_within [OF Metric_space12_mspace_mdist]
+  by (metis mtopology_of_def)
+
+
+context Metric_space
+begin
+
+lemma atin_within_imp_M:
+   "atin_within mtopology x S \<noteq> bot \<Longrightarrow> x \<in> M"
+  by (metis derived_set_of_trivial_limit in_derived_set_of topspace_mtopology)
+
+lemma atin_within_sequentially_sequence:
+  assumes "atin_within mtopology x S \<noteq> bot"
+  obtains \<sigma> where "range \<sigma> \<subseteq> S \<inter> M - {x}" 
+          "decreasing_dist \<sigma> x" "inj \<sigma>" "limitin mtopology \<sigma> x sequentially"
+  by (metis eventually_atin_within_A eventually_False assms)
+
+lemma derived_set_of_sequentially:
+  "mtopology derived_set_of S =
+   {x \<in> M. \<exists>\<sigma>. range \<sigma> \<subseteq> S \<inter> M - {x} \<and> limitin mtopology \<sigma> x sequentially}"
+proof -
+  have False
+    if "range \<sigma> \<subseteq> S \<inter> M - {x}"
+      and "limitin mtopology \<sigma> x sequentially"
+      and "atin_within mtopology x S = bot"
+    for x \<sigma>
+  proof -
+    have "\<forall>\<^sub>F n in sequentially. P (\<sigma> n)" for P
+      using that by (metis eventually_atin_within_B eventually_bot)
+    then show False
+      by (meson eventually_False_sequentially eventually_mono)
+  qed
+  then show ?thesis
+    using derived_set_of_trivial_limit 
+    by (fastforce elim!: atin_within_sequentially_sequence intro: atin_within_imp_M)
+qed
+
+lemma derived_set_of_sequentially_alt:
+  "mtopology derived_set_of S =
+   {x. \<exists>\<sigma>. range \<sigma> \<subseteq> S - {x} \<and> limitin mtopology \<sigma> x sequentially}"
+proof -
+  have *: "\<exists>\<sigma>. range \<sigma> \<subseteq> S \<inter> M - {x} \<and> limitin mtopology \<sigma> x sequentially"
+    if \<sigma>: "range \<sigma> \<subseteq> S - {x}" and lim: "limitin mtopology \<sigma> x sequentially" for x \<sigma>
+  proof -
+    obtain N where "\<forall>n\<ge>N. \<sigma> n \<in> M \<and> d (\<sigma> n) x < 1"
+      using lim limit_metric_sequentially by fastforce
+    with \<sigma> obtain a where a:"a \<in> S \<inter> M - {x}" by auto
+    show ?thesis
+    proof (intro conjI exI)
+      show "range (\<lambda>n. if \<sigma> n \<in> M then \<sigma> n else a) \<subseteq> S \<inter> M - {x}"
+        using a \<sigma> by fastforce
+      show "limitin mtopology (\<lambda>n. if \<sigma> n \<in> M then \<sigma> n else a) x sequentially"
+        using lim limit_metric_sequentially by fastforce
+    qed
+  qed
+  show ?thesis
+    by (auto simp: limitin_mspace derived_set_of_sequentially intro!: *)
+qed
+
+lemma derived_set_of_sequentially_inj:
+   "mtopology derived_set_of S =
+    {x \<in> M. \<exists>\<sigma>. range \<sigma> \<subseteq> S \<inter> M - {x} \<and> inj \<sigma> \<and> limitin mtopology \<sigma> x sequentially}"
+proof -
+  have False
+    if "x \<in> M" and "range \<sigma> \<subseteq> S \<inter> M - {x}"
+      and "limitin mtopology \<sigma> x sequentially"
+      and "atin_within mtopology x S = bot"
+    for x \<sigma>
+  proof -
+    have "\<forall>\<^sub>F n in sequentially. P (\<sigma> n)" for P
+      using that derived_set_of_sequentially_alt derived_set_of_trivial_limit by fastforce
+    then show False
+      by (meson eventually_False_sequentially eventually_mono)
+  qed
+  then show ?thesis
+    using derived_set_of_trivial_limit 
+    by (fastforce elim!: atin_within_sequentially_sequence intro: atin_within_imp_M)
+qed
+
+
+lemma derived_set_of_sequentially_inj_alt:
+   "mtopology derived_set_of S =
+    {x. \<exists>\<sigma>. range \<sigma> \<subseteq> S - {x} \<and> inj \<sigma> \<and> limitin mtopology \<sigma> x sequentially}"
+proof -
+  have "\<exists>\<sigma>. range \<sigma> \<subseteq> S - {x} \<and> inj \<sigma> \<and> limitin mtopology \<sigma> x sequentially"
+    if "atin_within mtopology x S \<noteq> bot" for x
+    by (metis Diff_empty Int_subset_iff atin_within_sequentially_sequence subset_Diff_insert that)
+  moreover have False
+    if "range (\<lambda>x. \<sigma> (x::nat)) \<subseteq> S - {x}"
+      and "limitin mtopology \<sigma> x sequentially"
+      and "atin_within mtopology x S = bot"
+    for x \<sigma>
+  proof -
+    have "\<forall>\<^sub>F n in sequentially. P (\<sigma> n)" for P
+      using that derived_set_of_sequentially_alt derived_set_of_trivial_limit by fastforce
+    then show False
+      by (meson eventually_False_sequentially eventually_mono)
+  qed
+  ultimately show ?thesis
+    using derived_set_of_trivial_limit by (fastforce intro: atin_within_imp_M)
+qed
+
+lemma derived_set_of_sequentially_decreasing:
+   "mtopology derived_set_of S =
+    {x \<in> M. \<exists>\<sigma>. range \<sigma> \<subseteq> S - {x} \<and> decreasing_dist \<sigma> x \<and> limitin mtopology \<sigma> x sequentially}"
+proof -
+  have "\<exists>\<sigma>. range \<sigma> \<subseteq> S - {x} \<and> decreasing_dist \<sigma> x \<and> limitin mtopology \<sigma> x sequentially"
+    if "atin_within mtopology x S \<noteq> bot" for x
+    by (metis Diff_empty atin_within_sequentially_sequence le_infE subset_Diff_insert that)
+  moreover have False
+    if "x \<in> M" and "range \<sigma> \<subseteq> S - {x}"
+      and "limitin mtopology \<sigma> x sequentially"
+      and "atin_within mtopology x S = bot"
+    for x \<sigma>
+  proof -
+    have "\<forall>\<^sub>F n in sequentially. P (\<sigma> n)" for P
+      using that derived_set_of_sequentially_alt derived_set_of_trivial_limit by fastforce
+    then show False
+      by (meson eventually_False_sequentially eventually_mono)
+  qed
+  ultimately show ?thesis
+    using derived_set_of_trivial_limit by (fastforce intro: atin_within_imp_M)
+qed
+
+lemma derived_set_of_sequentially_decreasing_alt:
+   "mtopology derived_set_of S =
+    {x. \<exists>\<sigma>. range \<sigma> \<subseteq> S - {x} \<and> decreasing_dist \<sigma> x \<and> limitin mtopology \<sigma> x sequentially}"
+  using derived_set_of_sequentially_alt derived_set_of_sequentially_decreasing by auto
+
+lemma closure_of_sequentially:
+   "mtopology closure_of S = 
+    {x \<in> M. \<exists>\<sigma>. range \<sigma> \<subseteq> S \<inter> M \<and> limitin mtopology \<sigma> x sequentially}"
+  by (auto simp: closure_of derived_set_of_sequentially)
+
+end (*Metric_space*)
+    
+
+subsection \<open>Three strong notions of continuity for metric spaces\<close>
+
+subsubsection \<open>Lipschitz continuity\<close>
+
+definition Lipschitz_continuous_map 
+  where "Lipschitz_continuous_map \<equiv> 
+      \<lambda>m1 m2 f. f ` mspace m1 \<subseteq> mspace m2 \<and>
+        (\<exists>B. \<forall>x \<in> mspace m1. \<forall>y \<in> mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y)"
+
+lemma Lipschitz_continuous_map_image: 
+  "Lipschitz_continuous_map m1 m2 f \<Longrightarrow> f ` mspace m1 \<subseteq> mspace m2"
+  by (simp add: Lipschitz_continuous_map_def)
+
+lemma Lipschitz_continuous_map_pos:
+   "Lipschitz_continuous_map m1 m2 f \<longleftrightarrow>
+    f ` mspace m1 \<subseteq> mspace m2 \<and>
+        (\<exists>B>0. \<forall>x \<in> mspace m1. \<forall>y \<in> mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y)"
+proof -
+  have "B * mdist m1 x y \<le> (\<bar>B\<bar> + 1) * mdist m1 x y" "\<bar>B\<bar> + 1 > 0" for x y B
+    by (auto simp add: mult_right_mono)
+  then show ?thesis
+    unfolding Lipschitz_continuous_map_def by (meson dual_order.trans)
+qed
+
+
+lemma Lipschitz_continuous_map_eq:
+  assumes "Lipschitz_continuous_map m1 m2 f" "\<And>x. x \<in> mspace m1 \<Longrightarrow> f x = g x"
+  shows "Lipschitz_continuous_map m1 m2 g"
+  using Lipschitz_continuous_map_def assms
+  by (metis (no_types, opaque_lifting) image_subset_iff)
+
+lemma Lipschitz_continuous_map_from_submetric:
+  assumes "Lipschitz_continuous_map m1 m2 f"
+  shows "Lipschitz_continuous_map (submetric m1 S) m2 f"
+  unfolding Lipschitz_continuous_map_def 
+proof
+  show "f ` mspace (submetric m1 S) \<subseteq> mspace m2"
+    using Lipschitz_continuous_map_pos assms by fastforce
+qed (use assms in \<open>fastforce simp: Lipschitz_continuous_map_def\<close>)
+
+lemma Lipschitz_continuous_map_from_submetric_mono:
+   "\<lbrakk>Lipschitz_continuous_map (submetric m1 T) m2 f; S \<subseteq> T\<rbrakk>
+           \<Longrightarrow> Lipschitz_continuous_map (submetric m1 S) m2 f"
+  by (metis Lipschitz_continuous_map_from_submetric inf.absorb_iff2 submetric_submetric)
+
+lemma Lipschitz_continuous_map_into_submetric:
+   "Lipschitz_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
+        f ` mspace m1 \<subseteq> S \<and> Lipschitz_continuous_map m1 m2 f"
+  by (auto simp: Lipschitz_continuous_map_def)
+
+lemma Lipschitz_continuous_map_const:
+  "Lipschitz_continuous_map m1 m2 (\<lambda>x. c) \<longleftrightarrow>
+        mspace m1 = {} \<or> c \<in> mspace m2"
+  unfolding Lipschitz_continuous_map_def image_subset_iff
+  by (metis all_not_in_conv mdist_nonneg mdist_zero mult_1)
+
+lemma Lipschitz_continuous_map_id:
+   "Lipschitz_continuous_map m1 m1 (\<lambda>x. x)"
+  by (metis Lipschitz_continuous_map_def image_ident mult_1 order_refl)
+
+lemma Lipschitz_continuous_map_compose:
+  assumes f: "Lipschitz_continuous_map m1 m2 f" and g: "Lipschitz_continuous_map m2 m3 g"
+  shows "Lipschitz_continuous_map m1 m3 (g \<circ> f)"
+  unfolding Lipschitz_continuous_map_def image_subset_iff
+proof
+  show "\<forall>x\<in>mspace m1. (g \<circ> f) x \<in> mspace m3"
+    by (metis Lipschitz_continuous_map_def assms comp_apply image_subset_iff)
+  obtain B where B: "\<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
+    using assms unfolding Lipschitz_continuous_map_def by presburger
+  obtain C where "C>0" and C: "\<forall>x\<in>mspace m2. \<forall>y\<in>mspace m2. mdist m3 (g x) (g y) \<le> C * mdist m2 x y"
+    using assms unfolding Lipschitz_continuous_map_pos by metis
+  show "\<exists>B. \<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m3 ((g \<circ> f) x) ((g \<circ> f) y) \<le> B * mdist m1 x y"
+    apply (rule_tac x="C*B" in exI)
+  proof clarify
+    fix x y
+    assume \<section>: "x \<in> mspace m1" "y \<in> mspace m1"
+    then have "mdist m3 ((g \<circ> f) x) ((g \<circ> f) y) \<le> C * mdist m2 (f x) (f y)"
+      by (metis C Lipschitz_continuous_map_def f comp_apply image_subset_iff)
+    also have "\<dots> \<le> C * B * mdist m1 x y"
+      by (simp add: "\<section>" B \<open>0 < C\<close>)
+    finally show "mdist m3 ((g \<circ> f) x) ((g \<circ> f) y) \<le> C * B * mdist m1 x y" .
+  qed
+qed
+
+subsubsection \<open>Uniform continuity\<close>
+
+definition uniformly_continuous_map 
+  where "uniformly_continuous_map \<equiv> 
+      \<lambda>m1 m2 f. f ` mspace m1 \<subseteq> mspace m2 \<and>
+        (\<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>x \<in> mspace m1. \<forall>y \<in> mspace m1. 
+                           mdist m1 y x < \<delta> \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>)"
+
+lemma uniformly_continuous_map_image: 
+  "uniformly_continuous_map m1 m2 f \<Longrightarrow> f ` mspace m1 \<subseteq> mspace m2"
+  by (simp add: uniformly_continuous_map_def)
+
+lemma ucmap_A:
+  assumes "uniformly_continuous_map m1 m2 f"
+  and "(\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0"
+    and "range \<rho> \<subseteq> mspace m1" "range \<sigma> \<subseteq> mspace m1"
+  shows "(\<lambda>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n))) \<longlonglongrightarrow> 0"
+  using assms
+  unfolding uniformly_continuous_map_def image_subset_iff tendsto_iff
+  apply clarsimp
+  by (metis (mono_tags, lifting) eventually_sequentially)
+
+lemma ucmap_B:
+  assumes \<section>: "\<And>\<rho> \<sigma>. \<lbrakk>range \<rho> \<subseteq> mspace m1; range \<sigma> \<subseteq> mspace m1;
+              (\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0\<rbrakk>
+              \<Longrightarrow> (\<lambda>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n))) \<longlonglongrightarrow> 0"
+    and "0 < \<epsilon>"
+    and \<rho>: "range \<rho> \<subseteq> mspace m1"
+    and \<sigma>: "range \<sigma> \<subseteq> mspace m1"
+    and "(\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0"
+  shows "\<exists>n. mdist m2 (f (\<rho> (n::nat))) (f (\<sigma> n)) < \<epsilon>"
+  using \<section> [OF \<rho> \<sigma>] assms by (meson LIMSEQ_le_const linorder_not_less)
+
+lemma ucmap_C: 
+  assumes \<section>: "\<And>\<rho> \<sigma> \<epsilon>. \<lbrakk>\<epsilon> > 0; range \<rho> \<subseteq> mspace m1; range \<sigma> \<subseteq> mspace m1;
+                       ((\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0)\<rbrakk>
+                      \<Longrightarrow> \<exists>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n)) < \<epsilon>"
+    and fim: "f ` mspace m1 \<subseteq> mspace m2"
+  shows "uniformly_continuous_map m1 m2 f"
+proof -
+  {assume "\<not> (\<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m1 y x < \<delta> \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>)" 
+    then obtain \<epsilon> where "\<epsilon> > 0" 
+      and "\<And>n. \<exists>x\<in>mspace m1. \<exists>y\<in>mspace m1. mdist m1 y x < inverse(Suc n) \<and> mdist m2 (f y) (f x) \<ge> \<epsilon>"
+      by (meson inverse_Suc linorder_not_le)
+    then obtain \<rho> \<sigma> where space: "range \<rho> \<subseteq> mspace m1" "range \<sigma> \<subseteq> mspace m1"
+         and dist: "\<And>n. mdist m1 (\<sigma> n) (\<rho> n) < inverse(Suc n) \<and> mdist m2 (f(\<sigma> n)) (f(\<rho> n)) \<ge> \<epsilon>"
+      by (metis image_subset_iff)
+    have False 
+      using \<section> [OF \<open>\<epsilon> > 0\<close> space] dist Lim_null_comparison
+      by (smt (verit) LIMSEQ_norm_0 inverse_eq_divide mdist_commute mdist_nonneg real_norm_def)
+  }
+  moreover
+  have "t \<in> mspace m2" if "t \<in> f ` mspace m1" for t
+    using fim that by blast
+  ultimately show ?thesis
+    by (fastforce simp: uniformly_continuous_map_def)
+qed
+
+lemma uniformly_continuous_map_sequentially:
+  "uniformly_continuous_map m1 m2 f \<longleftrightarrow>
+    f ` mspace m1 \<subseteq> mspace m2 \<and>
+    (\<forall>\<rho> \<sigma>. range \<rho> \<subseteq> mspace m1 \<and> range \<sigma> \<subseteq> mspace m1 \<and> (\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0
+          \<longrightarrow> (\<lambda>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n))) \<longlonglongrightarrow> 0)"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (simp add: ucmap_A uniformly_continuous_map_image)
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (intro ucmap_B ucmap_C) auto
+qed
+
+
+lemma uniformly_continuous_map_sequentially_alt:
+    "uniformly_continuous_map m1 m2 f \<longleftrightarrow>
+      f ` mspace m1 \<subseteq> mspace m2 \<and>
+      (\<forall>\<epsilon>>0. \<forall>\<rho> \<sigma>. range \<rho> \<subseteq> mspace m1 \<and> range \<sigma> \<subseteq> mspace m1 \<and>
+            ((\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0)
+            \<longrightarrow> (\<exists>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n)) < \<epsilon>))"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    using uniformly_continuous_map_image by (intro conjI strip ucmap_B | force simp: ucmap_A)+
+  show "?rhs \<Longrightarrow> ?lhs"
+    by (intro ucmap_C) auto
+qed
+
+
+lemma uniformly_continuous_map_eq:
+   "\<lbrakk>\<And>x. x \<in> mspace m1 \<Longrightarrow> f x = g x; uniformly_continuous_map m1 m2 f\<rbrakk>
+      \<Longrightarrow> uniformly_continuous_map m1 m2 g"
+  by (simp add: uniformly_continuous_map_def)
+
+lemma uniformly_continuous_map_from_submetric:
+  assumes "uniformly_continuous_map m1 m2 f"
+  shows "uniformly_continuous_map (submetric m1 S) m2 f"
+  unfolding uniformly_continuous_map_def 
+proof
+  show "f ` mspace (submetric m1 S) \<subseteq> mspace m2"
+    using assms by (auto simp: uniformly_continuous_map_def)
+qed (use assms in \<open>force simp: uniformly_continuous_map_def\<close>)
+
+lemma uniformly_continuous_map_from_submetric_mono:
+   "\<lbrakk>uniformly_continuous_map (submetric m1 T) m2 f; S \<subseteq> T\<rbrakk>
+           \<Longrightarrow> uniformly_continuous_map (submetric m1 S) m2 f"
+  by (metis uniformly_continuous_map_from_submetric inf.absorb_iff2 submetric_submetric)
+
+lemma uniformly_continuous_map_into_submetric:
+   "uniformly_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
+        f ` mspace m1 \<subseteq> S \<and> uniformly_continuous_map m1 m2 f"
+  by (auto simp: uniformly_continuous_map_def)
+
+lemma uniformly_continuous_map_const:
+  "uniformly_continuous_map m1 m2 (\<lambda>x. c) \<longleftrightarrow>
+        mspace m1 = {} \<or> c \<in> mspace m2"
+  unfolding uniformly_continuous_map_def image_subset_iff
+  by (metis empty_iff equals0I mdist_zero)
+
+lemma uniformly_continuous_map_id [simp]:
+   "uniformly_continuous_map m1 m1 (\<lambda>x. x)"
+  by (metis image_ident order_refl uniformly_continuous_map_def)
+
+lemma uniformly_continuous_map_compose:
+  assumes f: "uniformly_continuous_map m1 m2 f" and g: "uniformly_continuous_map m2 m3 g"
+  shows "uniformly_continuous_map m1 m3 (g \<circ> f)"
+  by (smt (verit, ccfv_threshold) comp_apply f g image_subset_iff uniformly_continuous_map_def)
+
+lemma uniformly_continuous_map_real_const [simp]:
+   "uniformly_continuous_map m euclidean_metric (\<lambda>x. c)"
+  by (simp add: euclidean_metric_def uniformly_continuous_map_const)
+
+text \<open>Equivalence between "abstract" and "type class" notions\<close>
+lemma uniformly_continuous_map_euclidean [simp]:
+  "uniformly_continuous_map (submetric euclidean_metric S) euclidean_metric f
+     = uniformly_continuous_on S f"
+  by (auto simp add: uniformly_continuous_map_def uniformly_continuous_on_def)
+
+subsubsection \<open>Cauchy continuity\<close>
+
+definition Cauchy_continuous_map where
+ "Cauchy_continuous_map \<equiv>
+  \<lambda>m1 m2 f. \<forall>\<sigma>. Metric_space.MCauchy (mspace m1) (mdist m1) \<sigma> 
+            \<longrightarrow> Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> \<sigma>)"
+
+lemma Cauchy_continuous_map_euclidean [simp]:
+  "Cauchy_continuous_map (submetric euclidean_metric S) euclidean_metric f
+     = Cauchy_continuous_on S f"
+  by (auto simp add: Cauchy_continuous_map_def Cauchy_continuous_on_def Cauchy_def Met_TC.subspace Metric_space.MCauchy_def)
+
+lemma Cauchy_continuous_map_image:
+  assumes "Cauchy_continuous_map m1 m2 f"
+  shows "f ` mspace m1 \<subseteq> mspace m2"
+proof clarsimp
+  fix x
+  assume "x \<in> mspace m1"
+  then have "Metric_space.MCauchy (mspace m1) (mdist m1) (\<lambda>n. x)"
+    by (simp add: Metric_space.MCauchy_const Metric_space_mspace_mdist)
+  then have "Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> (\<lambda>n. x))"
+    by (meson Cauchy_continuous_map_def assms)
+  then show "f x \<in> mspace m2"
+    by (simp add: Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+qed
+
+
+lemma Cauchy_continuous_map_eq:
+   "\<lbrakk>\<And>x. x \<in> mspace m1 \<Longrightarrow> f x = g x; Cauchy_continuous_map m1 m2 f\<rbrakk>
+      \<Longrightarrow> Cauchy_continuous_map m1 m2 g"
+  by (simp add: image_subset_iff Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+
+lemma Cauchy_continuous_map_from_submetric:
+  assumes "Cauchy_continuous_map m1 m2 f"
+  shows "Cauchy_continuous_map (submetric m1 S) m2 f"
+  using assms
+  by (simp add: image_subset_iff Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+
+lemma Cauchy_continuous_map_from_submetric_mono:
+   "\<lbrakk>Cauchy_continuous_map (submetric m1 T) m2 f; S \<subseteq> T\<rbrakk>
+           \<Longrightarrow> Cauchy_continuous_map (submetric m1 S) m2 f"
+  by (metis Cauchy_continuous_map_from_submetric inf.absorb_iff2 submetric_submetric)
+
+lemma Cauchy_continuous_map_into_submetric:
+   "Cauchy_continuous_map m1 (submetric m2 S) f \<longleftrightarrow>
+   f ` mspace m1 \<subseteq> S \<and> Cauchy_continuous_map m1 m2 f"  (is "?lhs \<longleftrightarrow> ?rhs")
+proof -
+  have "?lhs \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
+    by (simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+  moreover have "?rhs \<Longrightarrow> ?lhs"
+    by (bestsimp simp add: Cauchy_continuous_map_def  Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+  ultimately show ?thesis
+    by (metis Cauchy_continuous_map_image le_inf_iff mspace_submetric)
+qed
+
+lemma Cauchy_continuous_map_const [simp]:
+  "Cauchy_continuous_map m1 m2 (\<lambda>x. c) \<longleftrightarrow> mspace m1 = {} \<or> c \<in> mspace m2"
+proof -
+   have "mspace m1 = {} \<Longrightarrow> Cauchy_continuous_map m1 m2 (\<lambda>x. c)"
+    by (simp add: Cauchy_continuous_map_def Metric_space.MCauchy_def Metric_space_mspace_mdist)
+  moreover have "c \<in> mspace m2 \<Longrightarrow> Cauchy_continuous_map m1 m2 (\<lambda>x. c)"
+    by (simp add: Cauchy_continuous_map_def o_def Metric_space.MCauchy_const [OF Metric_space_mspace_mdist])
+  ultimately show ?thesis
+    using Cauchy_continuous_map_image by blast
+qed
+
+lemma Cauchy_continuous_map_id [simp]:
+   "Cauchy_continuous_map m1 m1 (\<lambda>x. x)"
+  by (simp add: Cauchy_continuous_map_def o_def)
+
+lemma Cauchy_continuous_map_compose:
+  assumes f: "Cauchy_continuous_map m1 m2 f" and g: "Cauchy_continuous_map m2 m3 g"
+  shows "Cauchy_continuous_map m1 m3 (g \<circ> f)"
+  by (metis (no_types, lifting) Cauchy_continuous_map_def f fun.map_comp g)
+
+lemma Lipschitz_imp_uniformly_continuous_map:
+  assumes "Lipschitz_continuous_map m1 m2 f"
+  shows "uniformly_continuous_map m1 m2 f"
+  proof -
+  have "f ` mspace m1 \<subseteq> mspace m2"
+    by (simp add: Lipschitz_continuous_map_image assms)
+  moreover have "\<exists>\<delta>>0. \<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m1 y x < \<delta> \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>"
+    if "\<epsilon> > 0" for \<epsilon>
+  proof -
+    obtain B where "\<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
+             and "B>0"
+      using that assms by (force simp add: Lipschitz_continuous_map_pos)
+    then have "\<forall>x\<in>mspace m1. \<forall>y\<in>mspace m1. mdist m1 y x < \<epsilon>/B \<longrightarrow> mdist m2 (f y) (f x) < \<epsilon>"
+      by (smt (verit, ccfv_SIG) less_divide_eq mdist_nonneg mult.commute that zero_less_divide_iff)
+    with \<open>B>0\<close> show ?thesis
+      by (metis divide_pos_pos that)
+  qed
+  ultimately show ?thesis
+    by (auto simp: uniformly_continuous_map_def)
+qed
+
+lemma uniformly_imp_Cauchy_continuous_map:
+   "uniformly_continuous_map m1 m2 f \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
+  unfolding uniformly_continuous_map_def Cauchy_continuous_map_def
+  apply (simp add: image_subset_iff o_def Metric_space.MCauchy_def [OF Metric_space_mspace_mdist])
+  by meson
+
+lemma locally_Cauchy_continuous_map:
+  assumes "\<epsilon> > 0"
+    and \<section>: "\<And>x. x \<in> mspace m1 \<Longrightarrow> Cauchy_continuous_map (submetric m1 (mball_of m1 x \<epsilon>)) m2 f"
+  shows "Cauchy_continuous_map m1 m2 f"
+  unfolding Cauchy_continuous_map_def
+proof (intro strip)
+  interpret M1: Metric_space "mspace m1" "mdist m1"
+    by (simp add: Metric_space_mspace_mdist)
+  interpret M2: Metric_space "mspace m2" "mdist m2"
+    by (simp add: Metric_space_mspace_mdist)
+  fix \<sigma>
+  assume \<sigma>: "M1.MCauchy \<sigma>"
+  with \<open>\<epsilon> > 0\<close> obtain N where N: "\<And>n n'. \<lbrakk>n\<ge>N; n'\<ge>N\<rbrakk> \<Longrightarrow> mdist m1 (\<sigma> n) (\<sigma> n') < \<epsilon>"
+    using M1.MCauchy_def by fastforce
+  then have "M1.mball (\<sigma> N) \<epsilon> \<subseteq> mspace m1"
+    by (auto simp: image_subset_iff M1.mball_def)
+  then interpret MS1: Metric_space "mball_of m1 (\<sigma> N) \<epsilon> \<inter> mspace m1" "mdist m1"
+    by (simp add: M1.subspace)
+  show "M2.MCauchy (f \<circ> \<sigma>)"
+  proof (rule M2.MCauchy_offset)
+    have "M1.MCauchy (\<sigma> \<circ> (+) N)"
+      by (simp add: M1.MCauchy_imp_MCauchy_suffix \<sigma>)
+    moreover have "range (\<sigma> \<circ> (+) N) \<subseteq> M1.mball (\<sigma> N) \<epsilon>"
+      using N [OF order_refl] M1.MCauchy_def \<sigma> by fastforce
+    ultimately have "MS1.MCauchy (\<sigma> \<circ> (+) N)"
+      unfolding M1.MCauchy_def MS1.MCauchy_def by (simp add: mball_of_def)
+    moreover have "\<sigma> N \<in> mspace m1"
+      using M1.MCauchy_def \<sigma> by auto
+    ultimately show "M2.MCauchy (f \<circ> \<sigma> \<circ> (+) N)"
+      unfolding comp_assoc
+      by (metis "\<section>" Cauchy_continuous_map_def mdist_submetric mspace_submetric)
+  next
+    fix n
+    have "\<sigma> n \<in> mspace m1"
+      by (meson Metric_space.MCauchy_def Metric_space_mspace_mdist \<sigma> range_subsetD)
+    then have "\<sigma> n \<in> mball_of m1 (\<sigma> n) \<epsilon>"
+      by (simp add: Metric_space.centre_in_mball_iff Metric_space_mspace_mdist assms(1) mball_of_def)
+    then show "(f \<circ> \<sigma>) n \<in> mspace m2"
+      using Cauchy_continuous_map_image [OF \<section> [of "\<sigma> n"]] \<open>\<sigma> n \<in> mspace m1\<close> by auto
+  qed
+qed
+
+context Metric_space12
+begin
+
+lemma Cauchy_continuous_imp_continuous_map:
+  assumes "Cauchy_continuous_map (metric (M1,d1)) (metric (M2,d2)) f"
+  shows "continuous_map M1.mtopology M2.mtopology f"
+proof (clarsimp simp: continuous_map_atin)
+  fix x
+  assume "x \<in> M1"
+  show "limitin M2.mtopology f (f x) (atin M1.mtopology x)"
+    unfolding limit_atin_sequentially
+  proof (intro conjI strip)
+    show "f x \<in> M2"
+      using Cauchy_continuous_map_image \<open>x \<in> M1\<close> assms by fastforce
+    fix \<sigma>
+    assume "range \<sigma> \<subseteq> M1 - {x} \<and> limitin M1.mtopology \<sigma> x sequentially"
+    then have "M1.MCauchy (\<lambda>n. if even n then \<sigma> (n div 2) else x)"
+      by (force simp add: M1.MCauchy_interleaving)
+    then have "M2.MCauchy (f \<circ> (\<lambda>n. if even n then \<sigma> (n div 2) else x))"
+      using assms by (simp add: Cauchy_continuous_map_def)
+    then show "limitin M2.mtopology (f \<circ> \<sigma>) (f x) sequentially"
+      using M2.MCauchy_interleaving [of "f \<circ> \<sigma>" "f x"]
+      by (simp add: o_def if_distrib cong: if_cong)
+  qed
+qed
+
+lemma continuous_imp_Cauchy_continuous_map:
+  assumes "M1.mcomplete"
+    and f: "continuous_map M1.mtopology M2.mtopology f"
+  shows "Cauchy_continuous_map (metric (M1,d1)) (metric (M2,d2)) f"
+  unfolding Cauchy_continuous_map_def
+proof clarsimp
+  fix \<sigma>
+  assume \<sigma>: "M1.MCauchy \<sigma>"
+  then obtain y where y: "limitin M1.mtopology \<sigma> y sequentially"
+    using M1.mcomplete_def assms by blast
+  have "range (f \<circ> \<sigma>) \<subseteq> M2"
+    using \<sigma> f by (simp add: M2.subspace M1.MCauchy_def M1.metric_continuous_map image_subset_iff)
+  then show "M2.MCauchy (f \<circ> \<sigma>)"
+    using continuous_map_limit [OF f y] M2.convergent_imp_MCauchy
+    by blast
+qed
+
+end
+
+text \<open>The same outside the locale\<close>
+lemma Cauchy_continuous_imp_continuous_map:
+  assumes "Cauchy_continuous_map m1 m2 f"
+  shows "continuous_map (mtopology_of m1) (mtopology_of m2) f"
+  using assms Metric_space12.Cauchy_continuous_imp_continuous_map [OF Metric_space12_mspace_mdist]
+  by (auto simp add: mtopology_of_def)
+
+lemma continuous_imp_Cauchy_continuous_map:
+  assumes "Metric_space.mcomplete (mspace m1) (mdist m1)"
+    and "continuous_map (mtopology_of m1) (mtopology_of m2) f"
+  shows "Cauchy_continuous_map m1 m2 f"
+  using assms Metric_space12.continuous_imp_Cauchy_continuous_map [OF Metric_space12_mspace_mdist]
+  by (auto simp add: mtopology_of_def)
+
+lemma uniformly_continuous_imp_continuous_map:
+   "uniformly_continuous_map m1 m2 f
+        \<Longrightarrow> continuous_map (mtopology_of m1) (mtopology_of m2) f"
+  by (simp add: Cauchy_continuous_imp_continuous_map uniformly_imp_Cauchy_continuous_map)
+
+lemma Lipschitz_continuous_imp_continuous_map:
+   "Lipschitz_continuous_map m1 m2 f
+     \<Longrightarrow> continuous_map (mtopology_of m1) (mtopology_of m2) f"
+  by (simp add: Lipschitz_imp_uniformly_continuous_map uniformly_continuous_imp_continuous_map)
+
+lemma Lipschitz_imp_Cauchy_continuous_map:
+   "Lipschitz_continuous_map m1 m2 f
+        \<Longrightarrow> Cauchy_continuous_map m1 m2 f"
+  by (simp add: Lipschitz_imp_uniformly_continuous_map uniformly_imp_Cauchy_continuous_map)
+
+lemma Cauchy_imp_uniformly_continuous_map:
+  assumes f: "Cauchy_continuous_map m1 m2 f"
+    and tbo: "Metric_space.mtotally_bounded (mspace m1) (mdist m1) (mspace m1)"
+  shows "uniformly_continuous_map m1 m2 f"
+  unfolding uniformly_continuous_map_sequentially_alt imp_conjL
+proof (intro conjI strip)
+  show "f ` mspace m1 \<subseteq> mspace m2"
+    by (simp add: Cauchy_continuous_map_image f)
+  interpret M1: Metric_space "mspace m1" "mdist m1"
+    by (simp add: Metric_space_mspace_mdist)
+  interpret M2: Metric_space "mspace m2" "mdist m2"
+    by (simp add: Metric_space_mspace_mdist)
+  fix \<epsilon> :: real and \<rho> \<sigma> 
+  assume "\<epsilon> > 0"
+    and \<rho>: "range \<rho> \<subseteq> mspace m1"
+    and \<sigma>: "range \<sigma> \<subseteq> mspace m1"
+    and 0: "(\<lambda>n. mdist m1 (\<rho> n) (\<sigma> n)) \<longlonglongrightarrow> 0"
+  then obtain r1 where "strict_mono r1" and r1: "M1.MCauchy (\<rho> \<circ> r1)"
+    using M1.mtotally_bounded_sequentially tbo by meson
+  then obtain r2 where "strict_mono r2" and r2: "M1.MCauchy (\<sigma> \<circ> r1 \<circ> r2)"
+    by (metis M1.mtotally_bounded_sequentially tbo \<sigma> image_comp image_subset_iff range_subsetD)
+  define r where "r \<equiv> r1 \<circ> r2"
+  have r: "strict_mono r"
+    by (simp add: r_def \<open>strict_mono r1\<close> \<open>strict_mono r2\<close> strict_mono_o)
+  define \<eta> where "\<eta> \<equiv> \<lambda>n. if even n then (\<rho> \<circ> r) (n div 2) else (\<sigma> \<circ> r) (n div 2)"
+  have "M1.MCauchy \<eta>"
+    unfolding \<eta>_def M1.MCauchy_interleaving_gen
+  proof (intro conjI)
+    show "M1.MCauchy (\<rho> \<circ> r)"
+      by (simp add: M1.MCauchy_subsequence \<open>strict_mono r2\<close> fun.map_comp r1 r_def)
+    show "M1.MCauchy (\<sigma> \<circ> r)"
+      by (simp add: fun.map_comp r2 r_def)
+    show "(\<lambda>n. mdist m1 ((\<rho> \<circ> r) n) ((\<sigma> \<circ> r) n)) \<longlonglongrightarrow> 0"
+      using LIMSEQ_subseq_LIMSEQ [OF 0 r] by (simp add: o_def)
+  qed
+  then have "Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> \<eta>)"
+    by (meson Cauchy_continuous_map_def f)
+  then have "(\<lambda>n. mdist m2 (f (\<rho> (r n))) (f (\<sigma> (r n)))) \<longlonglongrightarrow> 0"
+    using M2.MCauchy_interleaving_gen [of "f \<circ> \<rho> \<circ> r" "f \<circ> \<sigma> \<circ> r"]
+    by (simp add: \<eta>_def o_def if_distrib cong: if_cong)
+  then show "\<exists>n. mdist m2 (f (\<rho> n)) (f (\<sigma> n)) < \<epsilon>"
+    by (meson LIMSEQ_le_const \<open>0 < \<epsilon>\<close> linorder_not_le)
+qed
+
+lemma continuous_imp_uniformly_continuous_map:
+   "compact_space (mtopology_of m1) \<and>
+        continuous_map (mtopology_of m1) (mtopology_of m2) f
+        \<Longrightarrow> uniformly_continuous_map m1 m2 f"
+  by (simp add: Cauchy_imp_uniformly_continuous_map continuous_imp_Cauchy_continuous_map
+                Metric_space.compact_space_eq_mcomplete_mtotally_bounded
+                Metric_space_mspace_mdist mtopology_of_def)
+
+lemma continuous_eq_Cauchy_continuous_map:
+   "Metric_space.mcomplete (mspace m1) (mdist m1) \<Longrightarrow> 
+    continuous_map (mtopology_of m1) (mtopology_of m2) f \<longleftrightarrow> Cauchy_continuous_map m1 m2 f"
+  using Cauchy_continuous_imp_continuous_map continuous_imp_Cauchy_continuous_map by blast
+
+lemma continuous_eq_uniformly_continuous_map:
+   "compact_space (mtopology_of m1) 
+    \<Longrightarrow> continuous_map (mtopology_of m1) (mtopology_of m2) f \<longleftrightarrow>
+        uniformly_continuous_map m1 m2 f"
+  using continuous_imp_uniformly_continuous_map uniformly_continuous_imp_continuous_map by blast
+
+lemma Cauchy_eq_uniformly_continuous_map:
+   "Metric_space.mtotally_bounded (mspace m1) (mdist m1) (mspace m1)
+    \<Longrightarrow> Cauchy_continuous_map m1 m2 f \<longleftrightarrow> uniformly_continuous_map m1 m2 f"
+  using Cauchy_imp_uniformly_continuous_map uniformly_imp_Cauchy_continuous_map by blast
+
+lemma Lipschitz_continuous_map_projections:
+  "Lipschitz_continuous_map (prod_metric m1 m2) m1 fst"
+  "Lipschitz_continuous_map (prod_metric m1 m2) m2 snd"
+  by (simp add: Lipschitz_continuous_map_def prod_dist_def; 
+      metis mult_numeral_1 real_sqrt_sum_squares_ge1 real_sqrt_sum_squares_ge2)+
+
+lemma Lipschitz_continuous_map_pairwise:
+   "Lipschitz_continuous_map m (prod_metric m1 m2) f \<longleftrightarrow>
+    Lipschitz_continuous_map m m1 (fst \<circ> f) \<and> Lipschitz_continuous_map m m2 (snd \<circ> f)"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (simp add: Lipschitz_continuous_map_compose Lipschitz_continuous_map_projections)
+  have "Lipschitz_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f1 x, f2 x))"
+    if f1: "Lipschitz_continuous_map m m1 f1" and f2: "Lipschitz_continuous_map m m2 f2" for f1 f2
+  proof -
+    obtain B1 where "B1 > 0" 
+      and B1: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m\<rbrakk> \<Longrightarrow> mdist m1 (f1 x) (f1 y) \<le> B1 * mdist m x y"
+      by (meson Lipschitz_continuous_map_pos f1)
+    obtain B2 where "B2 > 0" 
+      and B2: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m\<rbrakk> \<Longrightarrow> mdist m2 (f2 x) (f2 y) \<le> B2 * mdist m x y"
+      by (meson Lipschitz_continuous_map_pos f2)
+    show ?thesis
+      unfolding Lipschitz_continuous_map_pos
+    proof (intro exI conjI strip)
+      have f1im: "f1 ` mspace m \<subseteq> mspace m1"
+        by (simp add: Lipschitz_continuous_map_image f1)
+      moreover have f2im: "f2 ` mspace m \<subseteq> mspace m2"
+        by (simp add: Lipschitz_continuous_map_image f2)
+      ultimately show "(\<lambda>x. (f1 x, f2 x)) ` mspace m \<subseteq> mspace (prod_metric m1 m2)"
+        by auto
+      show "B1+B2 > 0"
+        using \<open>0 < B1\<close> \<open>0 < B2\<close> by linarith
+      fix x y
+      assume xy: "x \<in> mspace m" "y \<in> mspace m"
+      with f1im f2im have "mdist (prod_metric m1 m2) (f1 x, f2 x) (f1 y, f2 y) \<le> mdist m1 (f1 x) (f1 y) + mdist m2 (f2 x) (f2 y)"
+        unfolding mdist_prod_metric
+        by (intro Metric_space12.prod_metric_le_components [OF Metric_space12_mspace_mdist]) auto
+      also have "... \<le> (B1+B2) * mdist m x y"
+        using B1 [OF xy] B2 [OF xy] by (simp add: vector_space_over_itself.scale_left_distrib) 
+      finally show "mdist (prod_metric m1 m2) (f1 x, f2 x) (f1 y, f2 y) \<le> (B1+B2) * mdist m x y" .
+    qed
+  qed
+  then show "?rhs \<Longrightarrow> ?lhs"
+    by force
+qed
+
+lemma uniformly_continuous_map_pairwise:
+   "uniformly_continuous_map m (prod_metric m1 m2) f \<longleftrightarrow> 
+    uniformly_continuous_map m m1 (fst \<circ> f) \<and> uniformly_continuous_map m m2 (snd \<circ> f)"
+   (is "?lhs \<longleftrightarrow> ?rhs")
+proof 
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (simp add: Lipschitz_continuous_map_projections Lipschitz_imp_uniformly_continuous_map uniformly_continuous_map_compose)
+  have "uniformly_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f1 x, f2 x))"
+    if f1: "uniformly_continuous_map m m1 f1" and f2: "uniformly_continuous_map m m2 f2" for f1 f2
+  proof -
+    show ?thesis
+      unfolding uniformly_continuous_map_def
+    proof (intro conjI strip)
+      have f1im: "f1 ` mspace m \<subseteq> mspace m1"
+        by (simp add: uniformly_continuous_map_image f1)
+      moreover have f2im: "f2 ` mspace m \<subseteq> mspace m2"
+        by (simp add: uniformly_continuous_map_image f2)
+      ultimately show "(\<lambda>x. (f1 x, f2 x)) ` mspace m \<subseteq> mspace (prod_metric m1 m2)"
+        by auto
+      fix \<epsilon>:: real
+      assume "\<epsilon> > 0"
+      obtain \<delta>1 where "\<delta>1>0" 
+        and \<delta>1: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m; mdist m y x < \<delta>1\<rbrakk> \<Longrightarrow> mdist m1 (f1 y) (f1 x) < \<epsilon>/2"
+        by (metis \<open>0 < \<epsilon>\<close> f1 half_gt_zero uniformly_continuous_map_def)
+      obtain \<delta>2 where "\<delta>2>0" 
+        and \<delta>2: "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m; mdist m y x < \<delta>2\<rbrakk> \<Longrightarrow> mdist m2 (f2 y) (f2 x) < \<epsilon>/2"
+        by (metis \<open>0 < \<epsilon>\<close> f2 half_gt_zero uniformly_continuous_map_def)
+      show "\<exists>\<delta>>0. \<forall>x\<in>mspace m. \<forall>y\<in>mspace m. mdist m y x < \<delta> \<longrightarrow> mdist (prod_metric m1 m2) (f1 y, f2 y) (f1 x, f2 x) < \<epsilon>"
+      proof (intro exI conjI strip)
+        show "min \<delta>1 \<delta>2>0"
+          using \<open>0 < \<delta>1\<close> \<open>0 < \<delta>2\<close> by auto
+        fix x y
+        assume xy: "x \<in> mspace m" "y \<in> mspace m" and d: "mdist m y x < min \<delta>1 \<delta>2"
+        have *: "mdist m1 (f1 y) (f1 x) < \<epsilon>/2" "mdist m2 (f2 y) (f2 x) < \<epsilon>/2"
+          using \<delta>1 \<delta>2 d xy by auto
+        have "mdist (prod_metric m1 m2) (f1 y, f2 y) (f1 x, f2 x) \<le> mdist m1 (f1 y) (f1 x) + mdist m2 (f2 y) (f2 x)"
+          unfolding mdist_prod_metric using f1im f2im xy
+          by (intro Metric_space12.prod_metric_le_components [OF Metric_space12_mspace_mdist]) auto
+        also have "... < \<epsilon>/2 + \<epsilon>/2"
+          using * by simp
+        finally show "mdist (prod_metric m1 m2) (f1 y, f2 y) (f1 x, f2 x) < \<epsilon>"
+          by simp
+      qed
+    qed
+  qed
+  then show "?rhs \<Longrightarrow> ?lhs"
+    by force
+qed
+
+lemma Cauchy_continuous_map_pairwise:
+   "Cauchy_continuous_map m (prod_metric m1 m2) f \<longleftrightarrow> Cauchy_continuous_map m m1 (fst \<circ> f) \<and> Cauchy_continuous_map m m2 (snd \<circ> f)"
+  by (auto simp: Cauchy_continuous_map_def Metric_space12.MCauchy_prod_metric[OF Metric_space12_mspace_mdist] comp_assoc)
+
+lemma Lipschitz_continuous_map_paired:
+   "Lipschitz_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f x, g x)) \<longleftrightarrow>
+        Lipschitz_continuous_map m m1 f \<and> Lipschitz_continuous_map m m2 g"
+  by (simp add: Lipschitz_continuous_map_pairwise o_def)
+
+lemma uniformly_continuous_map_paired:
+   "uniformly_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f x, g x)) \<longleftrightarrow>
+        uniformly_continuous_map m m1 f \<and> uniformly_continuous_map m m2 g"
+  by (simp add: uniformly_continuous_map_pairwise o_def)
+
+lemma Cauchy_continuous_map_paired:
+   "Cauchy_continuous_map m (prod_metric m1 m2) (\<lambda>x. (f x, g x)) \<longleftrightarrow>
+        Cauchy_continuous_map m m1 f \<and> Cauchy_continuous_map m m2 g"
+  by (simp add: Cauchy_continuous_map_pairwise o_def)
+
+lemma mbounded_Lipschitz_continuous_image:
+  assumes f: "Lipschitz_continuous_map m1 m2 f" and S: "Metric_space.mbounded (mspace m1) (mdist m1) S"
+  shows "Metric_space.mbounded (mspace m2) (mdist m2) (f`S)"
+proof -
+  obtain B where fim: "f ` mspace m1 \<subseteq> mspace m2"
+    and "B>0" and B: "\<And>x y. \<lbrakk>x \<in> mspace m1; y \<in> mspace m1\<rbrakk> \<Longrightarrow> mdist m2 (f x) (f y) \<le> B * mdist m1 x y"
+    by (meson Lipschitz_continuous_map_pos f)
+  show ?thesis
+    unfolding Metric_space.mbounded_alt_pos [OF Metric_space_mspace_mdist]
+  proof
+    obtain C where "S \<subseteq> mspace m1" and "C>0" and C: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> mdist m1 x y \<le> C"
+      using S by (auto simp: Metric_space.mbounded_alt_pos [OF Metric_space_mspace_mdist])
+    show "f ` S \<subseteq> mspace m2"
+      using fim \<open>S \<subseteq> mspace m1\<close> by blast
+    have "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> mdist m2 (f x) (f y) \<le> B * C"
+      by (smt (verit) B C \<open>0 < B\<close> \<open>S \<subseteq> mspace m1\<close> mdist_nonneg mult_mono subsetD)
+    moreover have "B*C > 0"
+      by (simp add: \<open>0 < B\<close> \<open>0 < C\<close>)
+    ultimately show "\<exists>B>0. \<forall>x\<in>f ` S. \<forall>y\<in>f ` S. mdist m2 x y \<le> B"
+      by auto
+  qed
+qed
+
+lemma mtotally_bounded_Cauchy_continuous_image:
+  assumes f: "Cauchy_continuous_map m1 m2 f" and S: "Metric_space.mtotally_bounded (mspace m1) (mdist m1) S"
+  shows "Metric_space.mtotally_bounded (mspace m2) (mdist m2) (f ` S)"
+  unfolding Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist]
+proof (intro conjI strip)
+  have "S \<subseteq> mspace m1"
+    using S by (simp add: Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist])
+  then show "f ` S \<subseteq> mspace m2"
+    using Cauchy_continuous_map_image f by blast
+  fix \<sigma> :: "nat \<Rightarrow> 'b"
+  assume "range \<sigma> \<subseteq> f ` S"
+  then have "\<forall>n. \<exists>x. \<sigma> n = f x \<and> x \<in> S"
+    by (meson imageE range_subsetD)
+  then obtain \<rho> where \<rho>: "\<And>n. \<sigma> n = f (\<rho> n)" "range \<rho> \<subseteq> S"
+    by (metis image_subset_iff)
+  then have "\<sigma> = f \<circ> \<rho>"
+    by fastforce
+  obtain r where "strict_mono r" "Metric_space.MCauchy (mspace m1) (mdist m1) (\<rho> \<circ> r)"
+    by (meson \<rho> S Metric_space.mtotally_bounded_sequentially[OF Metric_space_mspace_mdist])
+  then have "Metric_space.MCauchy (mspace m2) (mdist m2) (f \<circ> \<rho> \<circ> r)"
+    using f unfolding Cauchy_continuous_map_def by (metis fun.map_comp)
+  then show "\<exists>r. strict_mono r \<and> Metric_space.MCauchy (mspace m2) (mdist m2) (\<sigma> \<circ> r)"
+    using \<open>\<sigma> = f \<circ> \<rho>\<close> \<open>strict_mono r\<close> by blast
+qed
+
+lemma Lipschitz_coefficient_pos:
+  assumes "x \<in> mspace m" "y \<in> mspace m" "f x \<noteq> f y" 
+    and "f ` mspace m \<subseteq> mspace m2" 
+    and "\<And>x y. \<lbrakk>x \<in> mspace m; y \<in> mspace m\<rbrakk>
+            \<Longrightarrow> mdist m2 (f x) (f y) \<le> k * mdist m x y"
+  shows  "0 < k"
+  using assms by (smt (verit, best) image_subset_iff mdist_nonneg mdist_zero mult_nonpos_nonneg)
+
+lemma Lipschitz_continuous_map_metric:
+   "Lipschitz_continuous_map (prod_metric m m) euclidean_metric (\<lambda>(x,y). mdist m x y)"
+proof -
+  have "\<And>x y x' y'. \<lbrakk>x \<in> mspace m; y \<in> mspace m; x' \<in> mspace m; y' \<in> mspace m\<rbrakk>
+       \<Longrightarrow> \<bar>mdist m x y - mdist m x' y'\<bar> \<le> 2 * sqrt ((mdist m x x')\<^sup>2 + (mdist m y y')\<^sup>2)"
+    by (smt (verit, del_insts) mdist_commute mdist_triangle real_sqrt_sum_squares_ge2)
+  then show ?thesis
+    by (fastforce simp add: Lipschitz_continuous_map_def prod_dist_def dist_real_def)
+qed
+
+lemma Lipschitz_continuous_map_mdist:
+  assumes f: "Lipschitz_continuous_map m m' f" 
+    and g: "Lipschitz_continuous_map m m' g"
+  shows "Lipschitz_continuous_map m euclidean_metric (\<lambda>x. mdist m' (f x) (g x))"
+    (is "Lipschitz_continuous_map m _ ?h")
+proof -
+  have eq: "?h = ((\<lambda>(x,y). mdist m' x y) \<circ> (\<lambda>x. (f x,g x)))"
+    by force
+  show ?thesis
+    unfolding eq
+  proof (rule Lipschitz_continuous_map_compose)
+    show "Lipschitz_continuous_map m (prod_metric m' m') (\<lambda>x. (f x, g x))"
+      by (simp add: Lipschitz_continuous_map_paired f g)
+    show "Lipschitz_continuous_map (prod_metric m' m') euclidean_metric (\<lambda>(x,y). mdist m' x y)"
+      by (simp add: Lipschitz_continuous_map_metric)
+  qed
+qed
+
+lemma uniformly_continuous_map_mdist:
+  assumes f: "uniformly_continuous_map m m' f" 
+    and g: "uniformly_continuous_map m m' g"
+  shows "uniformly_continuous_map m euclidean_metric (\<lambda>x. mdist m' (f x) (g x))"
+    (is "uniformly_continuous_map m _ ?h")
+proof -
+  have eq: "?h = ((\<lambda>(x,y). mdist m' x y) \<circ> (\<lambda>x. (f x,g x)))"
+    by force
+  show ?thesis
+    unfolding eq
+  proof (rule uniformly_continuous_map_compose)
+    show "uniformly_continuous_map m (prod_metric m' m') (\<lambda>x. (f x, g x))"
+      by (simp add: uniformly_continuous_map_paired f g)
+    show "uniformly_continuous_map (prod_metric m' m') euclidean_metric (\<lambda>(x,y). mdist m' x y)"
+      by (simp add: Lipschitz_continuous_map_metric Lipschitz_imp_uniformly_continuous_map)
+  qed
+qed
+
+lemma Cauchy_continuous_map_mdist:
+  assumes f: "Cauchy_continuous_map m m' f" 
+    and g: "Cauchy_continuous_map m m' g"
+  shows "Cauchy_continuous_map m euclidean_metric (\<lambda>x. mdist m' (f x) (g x))"
+    (is "Cauchy_continuous_map m _ ?h")
+proof -
+  have eq: "?h = ((\<lambda>(x,y). mdist m' x y) \<circ> (\<lambda>x. (f x,g x)))"
+    by force
+  show ?thesis
+    unfolding eq
+  proof (rule Cauchy_continuous_map_compose)
+    show "Cauchy_continuous_map m (prod_metric m' m') (\<lambda>x. (f x, g x))"
+      by (simp add: Cauchy_continuous_map_paired f g)
+    show "Cauchy_continuous_map (prod_metric m' m') euclidean_metric (\<lambda>(x,y). mdist m' x y)"
+      by (simp add: Lipschitz_continuous_map_metric Lipschitz_imp_Cauchy_continuous_map)
+  qed
+qed
+
+lemma mtopology_of_prod_metric [simp]:
+    "mtopology_of (prod_metric m1 m2) = prod_topology (mtopology_of m1) (mtopology_of m2)"
+  by (simp add: mtopology_of_def Metric_space12.mtopology_prod_metric[OF Metric_space12_mspace_mdist])
+
+lemma continuous_map_metric:
+   "continuous_map (prod_topology (mtopology_of m) (mtopology_of m)) euclidean
+      (\<lambda>(x,y). mdist m x y)"
+  using Lipschitz_continuous_imp_continuous_map [OF Lipschitz_continuous_map_metric]
+  by auto
+
+lemma continuous_map_mdist_alt:
+  assumes "continuous_map X (prod_topology (mtopology_of m) (mtopology_of m)) f"
+  shows "continuous_map X euclidean (\<lambda>x. case_prod (mdist m) (f x))"
+    (is "continuous_map _ _ ?h")
+proof -
+  have eq: "?h = case_prod (mdist m) \<circ> f"
+    by force
+  show ?thesis
+    unfolding eq
+    using assms continuous_map_compose continuous_map_metric by blast
+qed
+
+lemma continuous_map_mdist:
+  assumes f: "continuous_map X (mtopology_of m) f" 
+      and g: "continuous_map X (mtopology_of m) g"
+  shows "continuous_map X euclidean (\<lambda>x. mdist m (f x) (g x))"
+    (is "continuous_map X _ ?h")
+proof -
+  have eq: "?h = ((\<lambda>(x,y). mdist m x y) \<circ> (\<lambda>x. (f x,g x)))"
+    by force
+  show ?thesis
+    unfolding eq
+  proof (rule continuous_map_compose)
+    show "continuous_map X (prod_topology (mtopology_of m) (mtopology_of m)) (\<lambda>x. (f x, g x))"
+      by (simp add: continuous_map_paired f g)
+  qed (simp add: continuous_map_metric)
+qed
+
+lemma continuous_on_mdist:
+   "a \<in> mspace m \<Longrightarrow> continuous_map (mtopology_of m) euclidean (mdist m a)"
+  by (simp add: continuous_map_mdist)
+
+subsection \<open>Isometries\<close>
+
+lemma (in Metric_space12) isometry_imp_embedding_map:
+  assumes fim: "f ` M1 \<subseteq> M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
+  shows "embedding_map M1.mtopology M2.mtopology f"
+proof -
+  have "inj_on f M1"
+    by (metis M1.zero d inj_onI)
+  then obtain g where g: "\<And>x. x \<in> M1 \<Longrightarrow> g (f x) = x"
+    by (metis inv_into_f_f)
+  have "homeomorphic_maps M1.mtopology (subtopology M2.mtopology (f ` topspace M1.mtopology)) f g"
+    unfolding homeomorphic_maps_def
+  proof (intro conjI; clarsimp)
+    show "continuous_map M1.mtopology (subtopology M2.mtopology (f ` M1)) f"
+      by (metis M1.metric_continuous_map M1.topspace_mtopology M2.Metric_space_axioms continuous_map_into_subtopology d fim order_refl)
+    have "Lipschitz_continuous_map (submetric (metric(M2,d2)) (f ` M1)) (metric(M1,d1)) g"
+      unfolding Lipschitz_continuous_map_def
+    proof (intro conjI exI strip; simp)
+      show "d1 (g x) (g y) \<le> 1 * d2 x y" if "x \<in> f ` M1 \<and> x \<in> M2" and "y \<in> f ` M1 \<and> y \<in> M2" for x y
+        using that d g by force
+    qed (use g in auto)
+    then have "continuous_map (mtopology_of (submetric (metric(M2,d2)) (f ` M1))) M1.mtopology g"
+      using Lipschitz_continuous_imp_continuous_map by force
+    moreover have "mtopology_of (submetric (metric(M2,d2)) (f ` M1)) = subtopology M2.mtopology (f ` M1)"
+      by (simp add: mtopology_of_submetric)
+    ultimately show "continuous_map (subtopology M2.mtopology (f ` M1)) M1.mtopology g"
+       by simp
+  qed (use g in auto)
+  then show ?thesis
+    by (auto simp: embedding_map_def homeomorphic_map_maps)
+qed
+
+lemma (in Metric_space12) isometry_imp_homeomorphic_map:
+  assumes fim: "f ` M1 = M2" and d: "\<And>x y. \<lbrakk>x \<in> M1; y \<in> M1\<rbrakk> \<Longrightarrow> d2 (f x) (f y) = d1 x y"
+  shows "homeomorphic_map M1.mtopology M2.mtopology f"
+  by (metis M1.topspace_mtopology M2.subtopology_mspace d embedding_map_def fim isometry_imp_embedding_map subsetI)
+
+end
+
diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -999,9 +999,6 @@
 
 subsubsection\<open>Totally bounded\<close>
 
-lemma cauchy_def: "Cauchy S \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (S m) (S n) < e)"
-  unfolding Cauchy_def by metis
-
 proposition seq_compact_imp_totally_bounded:
   assumes "seq_compact S"
   shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> S \<and> S \<subseteq> (\<Union>x\<in>k. ball x e)"
@@ -1025,7 +1022,7 @@
     then have "Cauchy (x \<circ> r)"
       using LIMSEQ_imp_Cauchy by auto
     then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
-      unfolding cauchy_def using \<open>e > 0\<close> by blast
+      unfolding Cauchy_def using \<open>e > 0\<close> by blast
     then have False
       using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
   then show ?thesis
@@ -1204,7 +1201,7 @@
     then show ?thesis by auto
   qed
   then have "Cauchy z"
-    by (simp add: cauchy_def)
+    by (metis metric_CauchyI)
   then obtain x where "x\<in>s" and x:"(z \<longlongrightarrow> x) sequentially"
     using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
 
@@ -1678,7 +1675,7 @@
       fix e :: real
       assume "e > 0"
       from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2"
-        unfolding cauchy_def using \<open>e > 0\<close> by (meson half_gt_zero)
+        unfolding Cauchy_def using \<open>e > 0\<close> by (meson half_gt_zero)
       then obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
         by (metis dist_self lim_sequentially lr(3))
       {
@@ -1793,7 +1790,7 @@
   shows "bounded (range s)"
 proof -
   from assms obtain N :: nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1"
-    unfolding cauchy_def by force
+    by (meson Cauchy_def zero_less_one)
   then have N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
   moreover
   have "bounded (s ` {0..N})"
@@ -1867,11 +1864,6 @@
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
-lemma continuous_closed_imp_Cauchy_continuous:
-  fixes S :: "('a::complete_space) set"
-  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
-  by (meson LIMSEQ_imp_Cauchy completeE complete_eq_closed continuous_on_sequentially)
-
 lemma banach_fix_type:
   fixes f::"'a::complete_space\<Rightarrow>'a"
   assumes c:"0 \<le> c" "c < 1"
@@ -1880,6 +1872,73 @@
   using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
   by auto
 
+subsection \<open>Cauchy continuity\<close>
+
+definition Cauchy_continuous_on where
+  "Cauchy_continuous_on \<equiv> \<lambda>S f. \<forall>\<sigma>. Cauchy \<sigma> \<longrightarrow> range \<sigma> \<subseteq> S \<longrightarrow> Cauchy (f \<circ> \<sigma>)"
+
+lemma continuous_closed_imp_Cauchy_continuous:
+  fixes S :: "('a::complete_space) set"
+  shows "\<lbrakk>continuous_on S f; closed S\<rbrakk> \<Longrightarrow> Cauchy_continuous_on S f"
+  unfolding Cauchy_continuous_on_def
+  by (metis LIMSEQ_imp_Cauchy completeE complete_eq_closed continuous_on_sequentially range_subsetD)
+
+lemma uniformly_continuous_imp_Cauchy_continuous:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "uniformly_continuous_on S f \<Longrightarrow> Cauchy_continuous_on S f"
+  by (simp add: uniformly_continuous_on_def Cauchy_continuous_on_def Cauchy_def image_subset_iff) metis
+
+lemma Cauchy_continuous_on_imp_continuous:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  assumes "Cauchy_continuous_on S f"
+  shows "continuous_on S f"
+proof -
+  have False if x: "\<forall>n. \<exists>x'\<in>S. dist x' x < inverse(Suc n) \<and> \<not> dist (f x') (f x) < \<epsilon>" "\<epsilon>>0" "x \<in> S" for x and \<epsilon>::real
+  proof -
+    obtain \<rho> where \<rho>: "\<forall>n. \<rho> n \<in> S" and dx: "\<forall>n. dist (\<rho> n) x < inverse(Suc n)" and dfx: "\<forall>n. \<not> dist (f (\<rho> n)) (f x) < \<epsilon>"
+      using x by metis
+    define \<sigma> where "\<sigma> \<equiv> \<lambda>n. if even n then \<rho> n else x"
+    with \<rho> \<open>x \<in> S\<close> have "range \<sigma> \<subseteq> S"
+      by auto
+    have "\<sigma> \<longlonglongrightarrow> x"
+      unfolding tendsto_iff
+    proof (intro strip)
+      fix e :: real
+      assume "e>0"
+      then obtain N where "inverse (Suc N) < e"
+        using reals_Archimedean by blast
+      then have "\<forall>n. N \<le> n \<longrightarrow> dist (\<rho> n) x < e"
+        by (smt (verit, ccfv_SIG) dx inverse_Suc inverse_less_iff_less inverse_positive_iff_positive of_nat_Suc of_nat_mono)
+      with \<open>e>0\<close> show "\<forall>\<^sub>F n in sequentially. dist (\<sigma> n) x < e"
+        by (auto simp add: eventually_sequentially \<sigma>_def)
+    qed
+    then have "Cauchy \<sigma>"
+      by (intro LIMSEQ_imp_Cauchy)
+    then have Cf: "Cauchy (f \<circ> \<sigma>)"
+      by (meson Cauchy_continuous_on_def \<open>range \<sigma> \<subseteq> S\<close> assms)
+    have "(f \<circ> \<sigma>) \<longlonglongrightarrow> f x"
+      unfolding tendsto_iff 
+    proof (intro strip)
+      fix e :: real
+      assume "e>0"
+      then obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist ((f \<circ> \<sigma>) m) ((f \<circ> \<sigma>) n) < e"
+        using Cf unfolding Cauchy_def by presburger
+      moreover have "(f \<circ> \<sigma>) (Suc(N+N)) = f x"
+        by (simp add: \<sigma>_def)
+      ultimately have "\<forall>n\<ge>N. dist ((f \<circ> \<sigma>) n) (f x) < e"
+        by (metis add_Suc le_add2)
+      then show "\<forall>\<^sub>F n in sequentially. dist ((f \<circ> \<sigma>) n) (f x) < e"
+        using eventually_sequentially by blast
+    qed
+    moreover have "\<And>n. \<not> dist (f (\<sigma> (2*n))) (f x) < \<epsilon>"
+      using dfx by (simp add: \<sigma>_def)
+    ultimately show False
+      using \<open>\<epsilon>>0\<close> by (fastforce simp: mult_2 nat_le_iff_add tendsto_iff eventually_sequentially)
+  qed
+  then show ?thesis
+    unfolding continuous_on_iff by (meson inverse_Suc)
+qed
+
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open> Finite intersection property\<close>
 
@@ -2805,7 +2864,7 @@
       by auto
   }
   then have "Cauchy t"
-    unfolding cauchy_def by auto
+    by (metis metric_CauchyI)
   then obtain l where l:"(t \<longlongrightarrow> l) sequentially"
     using complete_UNIV unfolding complete_def by auto
   { fix n :: nat
diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Analysis/Function_Metric.thy
--- a/src/HOL/Analysis/Function_Metric.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Analysis/Function_Metric.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -308,13 +308,14 @@
 proof
   fix u::"nat \<Rightarrow> ('a \<Rightarrow> 'b)" assume "Cauchy u"
   have "Cauchy (\<lambda>n. u n i)" for i
-  unfolding cauchy_def proof (intro impI allI)
-    fix e assume "e>(0::real)"
+    unfolding Cauchy_def 
+  proof (intro strip)
+    fix e::real assume "e>0"
     obtain k where "i = from_nat k"
       using from_nat_to_nat[of i] by metis
     have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
     then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
-      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
+      using \<open>Cauchy u\<close> by (meson Cauchy_def)
     then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
       by blast
     have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
@@ -334,7 +335,7 @@
         by (auto simp add: field_split_simps)
       then show "dist (u m i) (u n i) < e" by auto
     qed
-    then show "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
+    then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (u m i) (u n i) < e"
       by blast
   qed
   then have "\<exists>x. (\<lambda>n. u n i) \<longlonglongrightarrow> x" for i
diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -2684,7 +2684,8 @@
     fix \<sigma>
     assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>"
     have "Cauchy (f o \<sigma>)"
-      using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast
+      using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf
+      unfolding Cauchy_continuous_on_def by blast
     then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l"
       by (auto simp: convergent_eq_Cauchy [symmetric])
     show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l"
diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -6,7 +6,7 @@
 
 theory Lipschitz
   imports
-    Derivative
+    Derivative Abstract_Metric_Spaces
 begin
 
 definition\<^marker>\<open>tag important\<close> lipschitz_on
@@ -117,6 +117,17 @@
   from lipschitz_on_concat[OF this fg] show ?thesis .
 qed
 
+text \<open>Equivalence between "abstract" and "type class" Lipschitz notions, 
+for all types in the metric space class\<close>
+lemma Lipschitz_map_euclidean [simp]:
+  "Lipschitz_continuous_map euclidean_metric euclidean_metric f
+     \<longleftrightarrow> (\<exists>B. lipschitz_on B UNIV f)"  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show "?lhs \<Longrightarrow> ?rhs"
+    by (force simp add: Lipschitz_continuous_map_pos lipschitz_on_def less_le_not_le)
+  show "?rhs \<Longrightarrow> ?lhs"
+  by (metis Lipschitz_continuous_map_def lipschitz_onD mdist_euclidean_metric mspace_euclidean_metric top_greatest)
+qed
 
 subsubsection \<open>Continuity\<close>
 
diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Homology/Invariance_of_Domain.thy
--- a/src/HOL/Homology/Invariance_of_Domain.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Homology/Invariance_of_Domain.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -2799,7 +2799,8 @@
     fix \<sigma>
     assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>"
     have "Cauchy (f o \<sigma>)"
-      using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast
+      using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf 
+      unfolding Cauchy_continuous_on_def by blast
     then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l"
       by (auto simp: convergent_eq_Cauchy [symmetric])
     show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l"
diff -r 8234c42d20e6 -r 1cadc477f644 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed May 31 11:28:31 2023 +0100
+++ b/src/HOL/Limits.thy	Thu Jun 01 12:08:33 2023 +0100
@@ -2949,11 +2949,6 @@
 lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
 
-lemma uniformly_continuous_imp_Cauchy_continuous:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
-  shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
-  by (simp add: uniformly_continuous_on_def Cauchy_def) meson
-
 lemma (in bounded_linear) isUCont: "isUCont f"
   unfolding isUCont_def dist_norm
 proof (intro allI impI)