Nuprl Definition : metric-space
MetricSpace == X:Type × metric(X)
Definitions occuring in Statement :
metric: metric(X),
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
product: x:A × B[x],
universe: Type,
metric: metric(X)
FDL editor aliases :
metric-space
Latex:
MetricSpace == X:Type \mtimes{} metric(X)
Date html generated:
2019_10_29-AM-11_07_52
Last ObjectModification:
2019_10_02-AM-09_49_13
Theory : reals
Home
Index