Nuprl Definition : l-ordered
l-ordered(T;x,y.R[x; y];L) == ∀x,y:T. (x before y ∈ L ⇒ R[x; y])
Definitions occuring in Statement :
l_before: x before y ∈ l,
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
l_before: x before y ∈ l
FDL editor aliases :
l-ordered
Latex:
l-ordered(T;x,y.R[x; y];L) == \mforall{}x,y:T. (x before y \mmember{} L {}\mRightarrow{} R[x; y])
Date html generated:
2016_05_15-PM-04_35_51
Last ObjectModification:
2015_09_23-AM-07_49_26
Theory : general
Home
Index