Nuprl Definition : positive-lower-bound
positive-lower-bound(x) == rlessw(r0;x) + 1
Definitions occuring in Statement :
rlessw: rlessw(x;y),
int-to-real: r(n),
add: n + m,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
int-to-real: r(n),
rlessw: rlessw(x;y),
add: n + m
FDL editor aliases :
positive-lower-bound
Latex:
positive-lower-bound(x) == rlessw(r0;x) + 1
Date html generated:
2016_10_26-AM-09_14_50
Last ObjectModification:
2016_10_12-PM-03_16_11
Theory : reals
Home
Index