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).