Nuprl Definition : countable-p-union
countable-p-union(i.A[i]) == λp.if (fst(p) =z 0) then 0 else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi
Definitions occuring in Statement :
upto: upto(n),
imax-list: imax-list(L),
map: map(f;as),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pi1: fst(t),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
imax-list: imax-list(L),
map: map(f;as),
lambda: λx.A[x],
apply: f a,
upto: upto(n),
pi1: fst(t)
FDL editor aliases :
countable-p-union
countable-p-union(i.A[i]) ==
\mlambda{}p.if (fst(p) =\msubz{} 0) then 0 else imax-list(map(\mlambda{}i.(A[i] p);upto(fst(p)))) fi
Date html generated:
2015_07_17-AM-08_00_30
Last ObjectModification:
2008_02_27-PM-05_49_39
Home
Index