Nuprl Definition : qround
qround(r;k) == mk-rational(rounded-numerator(r;2 * k);2 * k)
Definitions occuring in Statement :
mk-rational: mk-rational(a;b),
rounded-numerator: rounded-numerator(r;k),
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
mk-rational: mk-rational(a;b),
rounded-numerator: rounded-numerator(r;k),
multiply: n * m,
natural_number: $n
FDL editor aliases :
qround
Latex:
qround(r;k) == mk-rational(rounded-numerator(r;2 * k);2 * k)
Date html generated:
2016_05_15-PM-10_37_58
Last ObjectModification:
2015_09_23-AM-08_26_56
Theory : rationals
Home
Index