complete_completelyMetrizableMetric

English

There is a complete metric on any completely metrizable space which is compatible with its topology.

Русский

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

LaTeX

$$$\\forall X,\\ [\\text{TopologicalSpace } X]\\ [IsCompletelyMetrizableSpace X]\\Rightarrow \\text{CompleteSpace }(X, \\text{metric from completelyMetrizableMetric }X)$$$

Lean4

theorem complete_completelyMetrizableMetric (X : Type*) [ht : TopologicalSpace X] [h : IsCompletelyMetrizableSpace X] :
    @CompleteSpace X (completelyMetrizableMetric X).toUniformSpace :=
  by
  convert h.complete.choose_spec.2
  exact MetricSpace.replaceTopology_eq _ _

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