Structures · Topology
TopologicalSpace.IsCompletelyMetrizableSpace
A topological space is completely metrizable if there exists a metric space structure
compatible with the topology which makes the space complete.
To endow such a space with a compatible distance, use
letI := upgradeIsCompletelyMetrizable X.
- Shape
- One type argument · adds complete
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- Prod
- Set.Elem
- Sum
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- TopologicalSpace.upgradeIsCompletelyMetrizable
- Topology.IsClosedEmbedding.IsCompletelyMetrizableSpace
- MeasureTheory.StronglyMeasurable.limUnder
- TopologicalSpace.completelyMetrizableMetric
- MeasureTheory.StronglyMeasurable.exists_eq_measurable_comp
- TopologicalSpace.IsCompletelyMetrizableSpace.complete
- TopologicalSpace.IsCompletelyMetrizableSpace.prod
- TopologicalSpace.IsCompletelyMetrizableSpace.univ
- IsClosed.isCompletelyMetrizableSpace
- TopologicalSpace.IsCompletelyMetrizableSpace.sum
- TopologicalSpace.IsCompletelyMetrizableSpace.pi_countable
- TopologicalSpace.IsCompletelyMetrizableSpace.sigma
- instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace
- TopologicalSpace.complete_completelyMetrizableMetric
- TopologicalSpace.IsCompletelyMetrizableSpace.toIsCompletelyPseudoMetrizableSpace
- TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace
Ancestors0
No ancestors.