Theorems · Definition · general topology
TopologicalSpace.pseudoMetrizableSpacePseudoMetric
(X : Type u_2) → [inst : TopologicalSpace X] → [TopologicalSpace.PseudoMetrizableSpace X] → PseudoMetricSpace X
Construct on a pseudometrizable space a pseudometric compatible with the topology.
- Defined in
- Mathlib.Topology.Metrizable.Uniformity
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- PseudoMetricSpacestatement · cited by 1,550
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- UniformSpace.pseudoMetricSpaceproof · cited by 0
Cited by14
Results whose statement or proof uses this declaration.
- Measurable.stronglyMeasurableproof · cited by 47
- measurable_of_tendsto_metrizable'proof · cited by 7
- Topology.IsEmbedding.aestronglyMeasurable_comp_iffproof · cited by 6
- MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpaceproof · cited by 2
- Continuous.stronglyMeasurable_of_support_subset_isCompactproof · cited by 2
- HasCompactSupport.measurable_of_prodproof · cited by 1
- ContinuousOn.aestronglyMeasurable_of_isSeparableproof · cited by 1
- Continuous.stronglyMeasurable_of_mulSupport_subset_isCompactproof · cited by 1
- HasCompactSupport.stronglyMeasurable_of_prodproof · cited by 1
- MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measureproof · cited by 1
- MeasureTheory.measurableSet_tendsto_funproof · cited by 0
- MeasureTheory.ProbabilityMeasure.continuous_piproof · cited by 0