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
FDL editor aliases : 
countable-p-union
Latex:
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:
2016_05_15-PM-11_49_33
Last ObjectModification:
2008_02_27-PM-05_49_39
Theory : randomness
Home
Index