completelyMetrizableMetric — Mathlib

English

On a completely metrizable space, there exists a complete metric compatible with its topology.

Русский

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

LaTeX

$$$\\exists d\\text{ on } X:\\text{MetricSpace }(X,d)\\text{ with topology } \\mathcal T_X\\text{ and } \\text{CompleteSpace }(X,d)$$$

Lean4

/-- Construct on a completely metrizable space a metric (compatible with the topology)
which is complete. -/
noncomputable def completelyMetrizableMetric (X : Type*) [TopologicalSpace X] [h : IsCompletelyMetrizableSpace X] :
    MetricSpace X :=
  h.complete.choose.replaceTopology h.complete.choose_spec.1.symm

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