Nuprl Definition : WtoSet
WtoSet(a.B[a];x) == let a,f = x in λb.WtoSet(a.B[a];f b)"(B[a])
Definitions occuring in Statement :
mk-set: f"(T),
apply: f a,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
apply: f a,
lambda: λx.A[x],
mk-set: f"(T),
spread: spread def
FDL editor aliases :
WtoSet
Latex:
WtoSet(a.B[a];x) == let a,f = x in \mlambda{}b.WtoSet(a.B[a];f b)"(B[a])
Date html generated:
2018_05_22-PM-09_51_55
Last ObjectModification:
2018_05_16-PM-01_31_44
Theory : constructive!set!theory
Home
Index