Nuprl Definition : rational-upper-approx
above 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,
add: 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,
add: n + m,
callbyvalue: callbyvalue
FDL editor aliases :
rational-upper-approx
Latex:
above x within 1/n == eval m = 2 * n in eval a = (x m) + 2 in (r(a))/2 * m
Date html generated:
2017_01_09-AM-08_55_37
Last ObjectModification:
2016_11_26-PM-01_32_42
Theory : reals
Home
Index