Nuprl Definition : ireal-approx
j-approx(x;M;z) == |x - (r(z)/r(2 * M))| ≤ (r(j)/r(M))
Definitions occuring in Statement :
rdiv: (x/y),
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
multiply: n * m,
natural_number: $n,
rdiv: (x/y),
int-to-real: r(n)
FDL editor aliases :
ireal-approx
Latex:
j-approx(x;M;z) == |x - (r(z)/r(2 * M))| \mleq{} (r(j)/r(M))
Date html generated:
2018_05_22-PM-01_58_34
Last ObjectModification:
2017_10_25-AM-10_18_09
Theory : reals
Home
Index