Nuprl Definition : max-metric
max-metric(n) == λp,q. primrec(n;r0;λi,r. rmax(r;|(p i) - q i|))
Definitions occuring in Statement :
rabs: |x|,
rmax: rmax(x;y),
rsub: x - y,
int-to-real: r(n),
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
int-to-real: r(n),
natural_number: $n,
lambda: λx.A[x],
rmax: rmax(x;y),
rabs: |x|,
rsub: x - y,
apply: f a
FDL editor aliases :
max-metric
Latex:
max-metric(n) == \mlambda{}p,q. primrec(n;r0;\mlambda{}i,r. rmax(r;|(p i) - q i|))
Date html generated:
2019_10_30-AM-08_34_58
Last ObjectModification:
2019_10_02-AM-11_01_24
Theory : reals
Home
Index