Nuprl Definition : mul-initial-seg
mul-initial-seg(f) == λn.reduce(λx,y. (x * y);1;map(f;upto(n)))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
reduce: reduce(f;k;as),
lambda: λx.A[x],
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
multiply: n * m,
natural_number: $n,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
mul-initial-seg
Latex:
mul-initial-seg(f) == \mlambda{}n.reduce(\mlambda{}x,y. (x * y);1;map(f;upto(n)))
Date html generated:
2016_05_15-PM-06_36_44
Last ObjectModification:
2015_09_23-AM-08_04_29
Theory : general
Home
Index