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