Nuprl Definition : strong-regular-upto

strong-regular-upto(a;b;n;f) ==
  bdd-all(n;i.bdd-all(n;j.a * |((i + 1) * (f (j + 1))) - (j + 1) * (f (i + 1))| ≤z b * ((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 :  strong-regular-upto
Latex:
strong-regular-upto(a;b;n;f)  ==
    bdd-all(n;i.bdd-all(n;j.a  *  |((i  +  1)  *  (f  (j  +  1)))  -  (j  +  1)  *  (f  (i  +  1))|  \mleq{}z  b
    *  ((i  +  1)  +  j  +  1)))


Date html generated: 2017_10_03-AM-08_42_47
Last ObjectModification: 2017_09_20-PM-05_11_29

Theory : reals


Home Index