metricSpace — Mathlib

English

There is a MetricSpace structure on X that is compatible with the UniformSpace structure, making the topologies agree.

Русский

Существует структура метрического пространства на X, совместимая с равномерной структурой так, что топологии совпадают.

LaTeX

$$$\\text{UniformSpace.pseudoMetricSpace}$ yields a compatible $MetricSpace$ on X via $MetricSpace.ofT0PseudoMetricSpace$$$

Lean4

/-- A `MetricSpace` instance compatible with a given `UniformSpace` structure. -/
protected noncomputable def metricSpace (X : Type*) [UniformSpace X] [IsCountablyGenerated (𝓤 X)] [T0Space X] :
    MetricSpace X :=
  @MetricSpace.ofT0PseudoMetricSpace X (UniformSpace.pseudoMetricSpace X) _

Похожие утверждения