Nuprl Definition : ulinorder
(compound)::
UniformLinorder(T;x,y.R[x; y]) ==
UniformOrder(T;x,y.R[x; y]) ∧ Connex(T;x,y.R[x; y]) ∧ (∀[x,y:T]. R[x; y] supposing R[x; y])
Definitions occuring in Statement :
uorder: UniformOrder(T;x,y.R[x; y]),
connex: Connex(T;x,y.R[x; y]),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
and: P ∧ Q
Definitions occuring in definition :
uorder: UniformOrder(T;x,y.R[x; y]),
and: P ∧ Q,
connex: Connex(T;x,y.R[x; y]),
uall: ∀[x:A]. B[x],
uimplies: b supposing a
FDL editor aliases :
ulinorder
Latex:
(compound)::
UniformLinorder(T;x,y.R[x; y]) ==
UniformOrder(T;x,y.R[x; y]) \mwedge{} Connex(T;x,y.R[x; y]) \mwedge{} (\mforall{}[x,y:T]. R[x; y] supposing R[x; y])
Date html generated:
2016_05_13-PM-04_16_42
Last ObjectModification:
2015_09_22-PM-05_46_10
Theory : rel_1
Home
Index