Structures · Topology
TopologicalSpace.IsCompletelyPseudoMetrizableSpace
A topological space is completely pseudometrizable if there exists a pseudometric space
structure compatible with the topology which makes the space complete.
To endow such a space with a compatible distance, use
letI := upgradeIsCompletelyPseudoMetrizable X.
- Shape
- One type argument · adds complete
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Prod
- Sum
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- Measurable.tsum
- TopologicalSpace.upgradeIsCompletelyPseudoMetrizable
- MeasureTheory.measurableSet_exists_tendsto
- MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto
- MeasureTheory.innerRegularWRT_isCompact_closure
- MeasureTheory.isTightMeasureSet_singleton
- AEMeasurable.tsum
- TopologicalSpace.IsCompletelyPseudoMetrizableSpace.complete
- MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen
- MeasureTheory.StronglyMeasurable.tsum
- MeasureTheory.StronglyMeasurable.tprod
- TopologicalSpace.completelyPseudoMetrizableMetric
- MeasureTheory.innerRegularWRT_isCompact
- MeasureTheory.exists_isCompact_closure_measure_compl_lt
- MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite
- IsClosed.isCompletelyPseudoMetrizableSpace
- MeasureTheory.innerRegularWRT_isCompact_isClosed
- MeasureTheory.AEStronglyMeasurable.tsum
- Topology.IsClosedEmbedding.IsCompletelyPseudoMetrizableSpace
- Measurable.tprod
- MeasureTheory.instInnerRegularOfIsCompletelyPseudoMetrizableSpace
- TopologicalSpace.IsCompletelyPseudoMetrizableSpace.sum
- TopologicalSpace.IsCompletelyMetrizableSpace_of_isCompletelyPseudoMetrizableSpace
- TopologicalSpace.complete_completelyPseudoMetrizableMetric
- MeasureTheory.innerRegularWRT_isCompact_isOpen
- TopologicalSpace.IsCompletelyPseudoMetrizableSpace.prod
- BaireSpace.of_completelyPseudoMetrizable
- TopologicalSpace.IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace
- MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace
- TopologicalSpace.IsCompletelyPseudoMetrizableSpace.pi_countable
- MeasureTheory.AEStronglyMeasurable.tprod
- AEMeasurable.tprod
Ancestors0
No ancestors.