Nuprl Definition : WFO
A WFO (well founded order) is a type together with a relation on the type
that satisfies the DCC (descending chain condition).⋅
WFO{i:l}() == A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<)
Definitions occuring in Statement :
DCC: DCC(T;<),
prop: ℙ,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
universe: Type,
product: x:A × B[x],
function: x:A ⟶ B[x],
prop: ℙ,
DCC: DCC(T;<)
FDL editor aliases :
WFO
Latex:
WFO\{i:l\}() == A:Type \mtimes{} <:A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{} \mtimes{} DCC(A;<)
Date html generated:
2016_07_08-PM-05_02_22
Last ObjectModification:
2015_09_23-AM-07_47_01
Theory : general
Home
Index