--- 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>