Nuprl Definition : msep
x # y == r0 < mdist(d;x;y)
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rless: x < y,
int-to-real: r(n),
natural_number: $n
Definitions occuring in definition :
rless: x < y,
int-to-real: r(n),
natural_number: $n,
mdist: mdist(d;x;y)
FDL editor aliases :
msep
Latex:
x \# y == r0 < mdist(d;x;y)
Date html generated:
2019_10_29-AM-11_00_03
Last ObjectModification:
2019_10_02-AM-09_41_27
Theory : reals
Home
Index