Nuprl Definition : rational-lower-approx
(below x within 1/n) == eval m = 2 * n in eval a = (x m) - 2 in (r(a))/2 * m
Definitions occuring in Statement :
int-rdiv: (a)/k1,
int-to-real: r(n),
callbyvalue: callbyvalue,
apply: f a,
multiply: n * m,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
multiply: n * m,
int-to-real: r(n),
int-rdiv: (a)/k1,
apply: f a,
subtract: n - m,
callbyvalue: callbyvalue
FDL editor aliases :
rational-lower-approx
Latex:
(below x within 1/n) == eval m = 2 * n in eval a = (x m) - 2 in (r(a))/2 * m
Date html generated:
2016_10_26-AM-09_11_08
Last ObjectModification:
2016_10_14-PM-03_25_06
Theory : reals
Home
Index