# HG changeset patch
# User desharna
# Date 1671433291 -3600
# Node ID 3eda063a20a4242fb7c535ebacef95b2f838eed5
# Parent  cca28679bdbfe57a7978e8646a09a11ce5d54412
added lemmas asym_on_subset and asymp_on_subset

diff -r cca28679bdbf -r 3eda063a20a4 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:05:23 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:01:31 2022 +0100
@@ -379,6 +379,12 @@
 lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
   by (blast dest: asymD)
 
+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)
+
 lemma (in preorder) asymp_less[simp]: "asymp (<)"
   by (auto intro: asympI dual_order.asym)