# HG changeset patch
# User nipkow
# Date 1739956355 -3600
# Node ID 52290d6ab92d628c7d8a07638b21125e23733e1d
# Parent  0b090cfce4e8d1d0d2bcccafaf19bdac2c7b057f
added lemma

diff -r 0b090cfce4e8 -r 52290d6ab92d src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 19 09:26:48 2025 +0100
+++ b/src/HOL/List.thy	Wed Feb 19 10:12:35 2025 +0100
@@ -6596,6 +6596,12 @@
   shows   "sorted_wrt R' (map f xs)"
   using assms by (induction rule: sorted_wrt_induct) auto
 
+lemma sorted_map_mono:
+  assumes "sorted xs" and "mono_on (set xs) f"
+  shows   "sorted (map f xs)"
+  using assms(1)
+  by (rule sorted_wrt_map_mono) (use assms in \<open>auto simp: mono_on_def\<close>)
+
 
 subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>