Nuprl Definition : image-metric
image-metric(d) == λp,q. (d (fst(p)) (fst(q)))
Definitions occuring in Statement :
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
image-metric
Latex:
image-metric(d) == \mlambda{}p,q. (d (fst(p)) (fst(q)))
Date html generated:
2019_10_30-AM-06_35_08
Last ObjectModification:
2019_10_25-AM-11_05_48
Theory : reals
Home
Index