Nuprl Definition : regular-upto
regular-upto(k;n;f) ==
bdd-all(n;i.bdd-all(n;j.|((i + 1) * (f (j + 1))) - (j + 1) * (f (i + 1))| ≤z (2 * k) * ((i + 1) + j + 1)))
Definitions occuring in Statement :
bdd-all: bdd-all(n;i.P[i]),
le_int: i ≤z j,
absval: |i|,
apply: f a,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
add: n + m,
multiply: n * m,
apply: f a,
subtract: n - m,
absval: |i|,
le_int: i ≤z j,
bdd-all: bdd-all(n;i.P[i])
FDL editor aliases :
regular-upto
Latex:
regular-upto(k;n;f) ==
bdd-all(n;i.bdd-all(n;j.|((i + 1) * (f (j + 1))) - (j + 1) * (f (i + 1))| \mleq{}z (2 * k)
* ((i + 1) + j + 1)))
Date html generated:
2017_10_03-AM-08_42_20
Last ObjectModification:
2017_09_06-PM-04_00_49
Theory : reals
Home
Index