metrizableSpaceMetric — Mathlib

English

Construct on a metrizable space a metric compatible with the topology.

Русский

Построить на метризуемом пространстве метрику, совместимую с данной топологией.

LaTeX

$$$\text{There exists a metric } d\text{ on } X\text{ such that } \tau(d)=\tau$$$

Lean4

/-- Construct on a metrizable space a metric compatible with the topology. -/
noncomputable def metrizableSpaceMetric (X : Type*) [TopologicalSpace X] [h : MetrizableSpace X] : MetricSpace X :=
  h.exists_metric.choose.replaceTopology h.exists_metric.choose_spec.symm

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