the above with
x and y to be those two elements and have the assumption reduce to F.)
Michael
From: Waqar Ahmad via hol-info
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Saturday, 1 September 2018 at 09:31
To: hol-info
Subject: [Hol-info] Partial Order for Set Supremum
Hi,
Latel
Hi,
Lately, I proved the equivalence of two supremum functions as:
|- !P.
(!x y. P x /\ P y ==> x <= y) /\ P <> {} ==>
(BIGSUP $<= P P = SOME (sup P)): thm
where BIGSUP is defined in [1] and "sup" can be found in HOL realTheory.
I'm not sure why the premise (!x y. P x /\ P y
