Nuprl Definition : reg_seq_mul
reg_seq_mul(x;y) == λn.[(x n) * (y n) ÷ 2 * n]
Definitions occuring in Statement :
rounding-div: [b ÷ m],
apply: f a,
lambda: λx.A[x],
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
rounding-div: [b ÷ m],
apply: f a,
multiply: n * m,
natural_number: $n
FDL editor aliases :
reg_seq_mul
Latex:
reg\_seq\_mul(x;y) == \mlambda{}n.[(x n) * (y n) \mdiv{} 2 * n]
Date html generated:
2019_10_16-PM-03_06_00
Last ObjectModification:
2019_02_15-AM-10_14_02
Theory : reals
Home
Index