Nuprl Definition : max-WFTO
This is the same maximal WFO as max-WO{i:l}() together with the
witness that its ordering is transitive.⋅
max-WFTO{i:l}() == <WFO{i:l}(), order-type-less(), DCC-order-type(), ot-less-trans()>
Definitions occuring in Statement :
DCC-order-type: DCC-order-type(),
ot-less-trans: ot-less-trans(),
WFO: WFO{i:l}(),
order-type-less: order-type-less(),
pair: <a, b>
Definitions occuring in definition :
WFO: WFO{i:l}(),
order-type-less: order-type-less(),
pair: <a, b>,
DCC-order-type: DCC-order-type(),
ot-less-trans: ot-less-trans()
FDL editor aliases :
max-WFTO
Latex:
max-WFTO\{i:l\}() == <WFO\{i:l\}(), order-type-less(), DCC-order-type(), ot-less-trans()>
Date html generated:
2016_07_08-PM-05_03_19
Last ObjectModification:
2015_09_23-AM-07_47_29
Theory : general
Home
Index