Nuprl Definition : greatest-lower-bound

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


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 :  greatest-lower-bound
Latex:
greatest-lower-bound(T;x,y.R[x;  y];a;b;c)  ==
    R[c;  a]  \mwedge{}  R[c;  b]  \mwedge{}  (\mforall{}x:T.  (R[x;  a]  {}\mRightarrow{}  R[x;  b]  {}\mRightarrow{}  R[x;  c]))


Date html generated: 2016_05_13-PM-04_18_23
Last ObjectModification: 2015_10_01-AM-10_53_57

Theory : rel_1


Home Index