Structures · Topology

TopologicalSpace.MetrizableSpace

A topological space is metrizable if there exists a metric 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 : MetricSpace X := TopologicalSpace.metrizableSpaceMetric X.

Defined in

Mathlib.Topology.Metrizable.Basic

Shape

One type argument