Nuprl Definition : least-upper-bound

least-upper-bound(T;x,y.R[x; y];a;b;c) ==  R[a; c] ∧ R[b; c] ∧ (∀x:T. (R[a; x] ⇒ R[b; x] ⇒ R[c; x]))


Definitions occuring in Statement :  all: ∀x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q
Definitions occuring in definition :  and: P ∧ Q,  all: ∀x:A. B[x],  implies: P ⇒ Q
FDL editor aliases :  least-upper-bound
Latex:
least-upper-bound(T;x,y.R[x;  y];a;b;c)  ==
    R[a;  c]  \mwedge{}  R[b;  c]  \mwedge{}  (\mforall{}x:T.  (R[a;  x]  {}\mRightarrow{}  R[b;  x]  {}\mRightarrow{}  R[c;  x]))


Date html generated: 2016_05_13-PM-04_18_08
Last ObjectModification: 2015_10_01-AM-10_53_46

Theory : rel_1


Home Index