Nuprl Definition : order
(compound):: Order(T;x,y.R[x; y]) == Refl(T;x,y.R[x; y]) ∧ Trans(T;x,y.R[x; y]) ∧ AntiSym(T;x,y.R[x; y])
Definitions occuring in Statement :
anti_sym: AntiSym(T;x,y.R[x; y])
,
trans: Trans(T;x,y.E[x; y])
,
refl: Refl(T;x,y.E[x; y])
,
and: P ∧ Q
Definitions occuring in definition :
refl: Refl(T;x,y.E[x; y])
,
and: P ∧ Q
,
trans: Trans(T;x,y.E[x; y])
,
anti_sym: AntiSym(T;x,y.R[x; y])
FDL editor aliases :
order
Latex:
(compound)::
Order(T;x,y.R[x; y]) ==
Refl(T;x,y.R[x; y]) \mwedge{} Trans(T;x,y.R[x; y]) \mwedge{} AntiSym(T;x,y.R[x; y])
Date html generated:
2016_05_13-PM-04_16_28
Last ObjectModification:
2015_09_22-PM-05_46_08
Theory : rel_1
Home
Index