Nuprl Definition : up-set

up-set(T;eq;x,y.le[x; y];s) ==  ∀x,y:T.  (x ∈ s ⇒ le[x; y] ⇒ y ∈ s)


Definitions occuring in Statement :  fset-member: a ∈ s,  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q,  fset-member: a ∈ s
FDL editor aliases :  up-set
Latex:
up-set(T;eq;x,y.le[x;  y];s)  ==    \mforall{}x,y:T.    (x  \mmember{}  s  {}\mRightarrow{}  le[x;  y]  {}\mRightarrow{}  y  \mmember{}  s)


Date html generated: 2016_05_14-PM-03_47_20
Last ObjectModification: 2015_10_06-PM-01_33_43

Theory : finite!sets


Home Index