Library schutte.Lub
Set Implicit Arguments.
Require Import Relations.
Require Import Classical_sets.
Definition upper_bound (M:Type)
(D: Ensemble M)
(R:M->M->Prop)
(X:Ensemble M)
(a:M) :=
forall x, D x -> In _ X x -> x=a \/ R x a.
Definition is_lub (M:Type)
(D : Ensemble M)
(R:M->M->Prop)
(X:Ensemble M)
(a:M) :=
D a /\ upper_bound D R X a /\
(forall y, D y -> upper_bound D R X y -> y = a \/ R a y).