# HG changeset patch
# User desharna
# Date 1654358288 -7200
# Node ID f0dfcd8329d042793526122dbdf3e2286012fdd6
# Parent  4e3e55aedd7f37151bdad64ed72b39b98b5318b2
added lemmas reflp_on_Inf and reflp_on_Sup

diff -r 4e3e55aedd7f -r f0dfcd8329d0 NEWS
--- a/NEWS	Sat Jun 04 17:48:58 2022 +0200
+++ b/NEWS	Sat Jun 04 17:58:08 2022 +0200
@@ -52,6 +52,8 @@
       preorder.asymp_less
       reflp_onD
       reflp_onI
+      reflp_on_Inf
+      reflp_on_Sup
       reflp_on_inf
       reflp_on_mono
       reflp_on_subset
diff -r 4e3e55aedd7f -r f0dfcd8329d0 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Jun 04 17:48:58 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 17:58:08 2022 +0200
@@ -224,9 +224,15 @@
 lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Inter>(A ` S)) (\<Inter>(r ` S))"
   unfolding refl_on_def by fast
 
+lemma reflp_on_Inf: "\<forall>x\<in>S. reflp_on (A x) (R x) \<Longrightarrow> reflp_on (\<Inter>(A ` S)) (\<Sqinter>(R ` S))"
+  by (auto intro: reflp_onI dest: reflp_onD)
+
 lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Union>(A ` S)) (\<Union>(r ` S))"
   unfolding refl_on_def by blast
 
+lemma reflp_on_Sup: "\<forall>x\<in>S. reflp_on (A x) (R x) \<Longrightarrow> reflp_on (\<Union>(A ` S)) (\<Squnion>(R ` S))"
+  by (auto intro: reflp_onI dest: reflp_onD)
+
 lemma refl_on_empty [simp]: "refl_on {} {}"
   by (simp add: refl_on_def)