Nuprl Definition : unit-interval-ms
I == interval-metric-space([r0, r1])
Definitions occuring in Statement :
interval-metric-space: interval-metric-space(I),
rccint: [l, u],
int-to-real: r(n),
natural_number: $n
Definitions occuring in definition :
interval-metric-space: interval-metric-space(I),
rccint: [l, u],
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
unit-interval-ms
Latex:
I == interval-metric-space([r0, r1])
Date html generated:
2019_10_29-AM-11_13_15
Last ObjectModification:
2019_10_02-AM-09_53_37
Theory : reals
Home
Index