Theorems · Inductive type · general topology

TopologicalSpace.MetrizableSpace

(X : Type u_5) → [t : TopologicalSpace X] → Prop

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

Cited by

39 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace