Nuprl Definition : mcompact
mcompact(X;d) == mcomplete(X with d) × m-TB(X;d)
Definitions occuring in Statement :
m-TB: m-TB(X;d),
mcomplete: mcomplete(M),
mk-metric-space: X with d,
product: x:A × B[x]
Definitions occuring in definition :
m-TB: m-TB(X;d),
mk-metric-space: X with d,
mcomplete: mcomplete(M),
product: x:A × B[x]
FDL editor aliases :
mcompact
Latex:
mcompact(X;d) == mcomplete(X with d) \mtimes{} m-TB(X;d)
Date html generated:
2019_10_30-AM-07_06_00
Last ObjectModification:
2019_10_25-PM-01_12_07
Theory : reals
Home
Index