Nuprl Definition : prod2-metric
prod2-metric(dX;dY) == λv,w. let x1,y1 = v in let x2,y2 = w in mdist(dX;x1;x2) + mdist(dY;y1;y2)
Definitions occuring in Statement :
mdist: mdist(d;x;y),
radd: a + b,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
lambda: λx.A[x],
spread: spread def,
radd: a + b,
mdist: mdist(d;x;y)
FDL editor aliases :
prod2-metric
Latex:
prod2-metric(dX;dY) == \mlambda{}v,w. let x1,y1 = v in let x2,y2 = w in mdist(dX;x1;x2) + mdist(dY;y1;y2)
Date html generated:
2019_10_29-AM-11_10_14
Last ObjectModification:
2019_10_02-AM-09_50_57
Theory : reals
Home
Index