# HG changeset patch # User desharna # Date 1665479227 -7200 # Node ID 61a5b5ad3a6e3ef33dbe9c04aa416431b765afe9 # Parent 207b6fcfc47df9b0b74a76016783df414542fd33 added lemmas reflp_ge[simp] and reflp_le[simp] diff -r 207b6fcfc47d -r 61a5b5ad3a6e NEWS --- a/NEWS Mon Oct 10 19:07:54 2022 +0200 +++ b/NEWS Tue Oct 11 11:07:07 2022 +0200 @@ -16,6 +16,8 @@ antisymp_if_asymp irreflD irreflpD + reflp_ge[simp] + reflp_le[simp] totalp_on_singleton[simp] diff -r 207b6fcfc47d -r 61a5b5ad3a6e src/HOL/Relation.thy --- a/src/HOL/Relation.thy Mon Oct 10 19:07:54 2022 +0200 +++ b/src/HOL/Relation.thy Tue Oct 11 11:07:07 2022 +0200 @@ -256,6 +256,12 @@ lemma reflp_mono: "reflp R \ (\x y. R x y \ Q x y) \ reflp Q" by (rule reflp_on_mono[of UNIV R Q]) simp_all +lemma (in preorder) reflp_le[simp]: "reflp (\)" + by (simp add: reflpI) + +lemma (in preorder) reflp_ge[simp]: "reflp (\)" + by (simp add: reflpI) + subsubsection \Irreflexivity\