Nuprl Definition : max-WO
This is a member of WFO{i':l} in which all members of WFO{i:l}() will embed.
(If ⌜Type ∈ Type⌝ this would lead to a contradiction.)⋅
max-WO{i:l}() == <WFO{i:l}(), order-type-less(), DCC-order-type()>
Definitions occuring in Statement :
DCC-order-type: DCC-order-type(),
WFO: WFO{i:l}(),
order-type-less: order-type-less(),
pair: <a, b>
Definitions occuring in definition :
WFO: WFO{i:l}(),
pair: <a, b>,
order-type-less: order-type-less(),
DCC-order-type: DCC-order-type()
FDL editor aliases :
max-WO
Latex:
max-WO\{i:l\}() == <WFO\{i:l\}(), order-type-less(), DCC-order-type()>
Date html generated:
2016_07_08-PM-05_03_09
Last ObjectModification:
2015_09_23-AM-07_47_24
Theory : general
Home
Index