toIsCompletelyMetrizableSpace — Mathlib

English

If a metric space is complete, then it is completely metrizable.

Русский

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

LaTeX

$$$[\text{MetricSpace } X] \land [\text{CompleteSpace } X] \Rightarrow [\text{IsCompletelyMetrizableSpace } X]$$$

Lean4

instance (priority := 100) _root_.MetricSpace.toIsCompletelyMetrizableSpace [MetricSpace X] [CompleteSpace X] :
    IsCompletelyMetrizableSpace X :=
  ⟨⟨‹_›, rfl, ‹_›⟩⟩

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