Nuprl Definition : power-set
P(T) == I:Type × (I ⟶ T)
Definitions occuring in Statement :
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x]
FDL editor aliases :
power-set
Latex:
P(T) == I:Type \mtimes{} (I {}\mrightarrow{} T)
Date html generated:
2016_05_13-PM-03_51_32
Last ObjectModification:
2015_09_22-PM-05_45_23
Theory : bar-induction
Home
Index