# HG changeset patch
# User desharna
# Date 1742822838 -3600
# Node ID 1d0116b288e33ebafd2af0c38760a6bf7e034b69
# Parent  3bdfdadf3a5256060d0797db251763666709df4a
added lemmas asymp_on_mono_strong and asymp_on_mono[mono]

diff -r 3bdfdadf3a52 -r 1d0116b288e3 NEWS
--- a/NEWS	Mon Mar 24 14:21:36 2025 +0100
+++ b/NEWS	Mon Mar 24 14:27:18 2025 +0100
@@ -65,6 +65,8 @@
       antisymp_on_mono_stronger
       asym_on_bot[simp]
       asymp_on_bot[simp]
+      asymp_on_mono[mono]
+      asymp_on_mono_strong
       irrefl_on_bot[simp]
       irreflp_on_bot[simp]
       irreflp_on_mono[mono]
diff -r 3bdfdadf3a52 -r 1d0116b288e3 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 24 14:21:36 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 14:27:18 2025 +0100
@@ -410,11 +410,18 @@
 lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
   by (blast dest: asymD)
 
+lemma asymp_on_mono_strong:
+  "asymp_on B Q \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> asymp_on A R"
+  by (rule asymp_onI) (auto dest: asymp_onD)
+
+lemma asymp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> asymp_on B Q \<le> asymp_on A R"
+  by (simp add: asymp_on_mono_strong le_fun_def)
+
 lemma asym_on_subset: "asym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asym_on B r"
   by (auto simp: asym_on_def)
 
 lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
-  by (auto simp: asymp_on_def)
+  using asymp_on_mono_strong .
 
 lemma asymp_on_image: "asymp_on (f ` A) R \<longleftrightarrow> asymp_on A (\<lambda>a b. R (f a) (f b))"
   by (simp add: asymp_on_def)