Structures · Topology

TopologicalSpace.PseudoMetrizableSpace

A topological space is pseudometrizable if there exists a pseudometric space structure compatible with the topology. To minimize imports, we implement this class in terms of the existence of a countably generated uniformity inducing the topology, which is mathematically equivalent. To endow such a space with a compatible uniformity, use letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X. To endow such a space with a compatible distance, use letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X.

Defined in

Mathlib.Topology.Metrizable.Basic

Shape

One type argument · adds exists_countably_generated