Theorems · Inductive type · general topology

TopologicalSpace.PseudoMetrizableSpace

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

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

Cited by

245 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpace