Nuprl Definition : prod-metric
prod-metric(k;d) == λv,w. Σ{mdist(d i;v i;w i) | 0≤i≤k - 1}
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rsum: Σ{x[k] | n≤k≤m},
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
rsum: Σ{x[k] | n≤k≤m},
subtract: n - m,
natural_number: $n,
mdist: mdist(d;x;y),
apply: f a
FDL editor aliases :
prod-metric
Latex:
prod-metric(k;d) == \mlambda{}v,w. \mSigma{}\{mdist(d i;v i;w i) | 0\mleq{}i\mleq{}k - 1\}
Date html generated:
2019_10_29-AM-11_09_14
Last ObjectModification:
2019_10_02-AM-09_50_22
Theory : reals
Home
Index