Nuprl Definition : WFTRO
WFTRO{i:l}() == A:Type × <:A ⟶ A ⟶ ℙ × DCC(A;<) × Trans(A;x,y.x < y)
Definitions occuring in Statement :
DCC: DCC(T;<),
trans: Trans(T;x,y.E[x; y]),
prop: ℙ,
infix_ap: x f y,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
universe: Type,
function: x:A ⟶ B[x],
prop: ℙ,
product: x:A × B[x],
DCC: DCC(T;<),
trans: Trans(T;x,y.E[x; y]),
infix_ap: x f y
FDL editor aliases :
WFTRO
Latex:
WFTRO\{i:l\}() == A:Type \mtimes{} <:A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{} \mtimes{} DCC(A;<) \mtimes{} Trans(A;x,y.x < y)
Date html generated:
2016_05_15-PM-04_15_02
Last ObjectModification:
2015_09_23-AM-07_47_20
Theory : general
Home
Index