Nuprl Definition : rleq

x ≤ y ==  rnonneg(y - x)


Definitions occuring in Statement :  rnonneg: rnonneg(x),  rsub: x - y
Definitions occuring in definition :  rnonneg: rnonneg(x),  rsub: x - y
FDL editor aliases :  rleq
Latex:
x  \mleq{}  y  ==    rnonneg(y  -  x)


Date html generated: 2016_05_18-AM-07_04_32
Last ObjectModification: 2015_09_23-AM-09_01_19

Theory : reals


Home Index