Nuprl Definition : metric-leq
d1 ≤ d2 == ∀x,y:X. (mdist(d1;x;y) ≤ mdist(d2;x;y))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rleq: x ≤ y,
all: ∀x:A. B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
rleq: x ≤ y,
mdist: mdist(d;x;y)
FDL editor aliases :
metric-leq
Latex:
d1 \mleq{} d2 == \mforall{}x,y:X. (mdist(d1;x;y) \mleq{} mdist(d2;x;y))
Date html generated:
2019_10_29-AM-11_06_31
Last ObjectModification:
2019_10_02-AM-09_48_03
Theory : reals
Home
Index