Nuprl Definition : real-subset-metric
real-subset-metric() == induced-rmetric(λp.(fst(p)))
Definitions occuring in Statement :
induced-rmetric: induced-rmetric(f),
pi1: fst(t),
lambda: λx.A[x]
Definitions occuring in definition :
induced-rmetric: induced-rmetric(f),
lambda: λx.A[x],
pi1: fst(t)
FDL editor aliases :
real-subset-metric
Latex:
real-subset-metric() == induced-rmetric(\mlambda{}p.(fst(p)))
Date html generated:
2019_10_29-AM-11_05_14
Last ObjectModification:
2019_10_02-AM-09_46_54
Theory : reals
Home
Index