isCompletelyMetrizableSpace — Mathlib

English

A closed subset of a completely metrizable space is completely metrizable.

Русский

Замкнутое подмножество полностью метризуемого пространства является полностью метризуемым.

LaTeX

$$$\\forall X, [TopologicalSpace X] [IsCompletelyMetrizableSpace X]\\forall s: Set X\\IsClosed s\\Rightarrow IsCompletelyMetrizableSpace s$$$

Lean4

/-- A closed subset of a completely metrizable space is also completely metrizable. -/
theorem _root_.IsClosed.isCompletelyMetrizableSpace [TopologicalSpace X] [IsCompletelyMetrizableSpace X] {s : Set X}
    (hs : IsClosed s) : IsCompletelyMetrizableSpace s :=
  hs.isClosedEmbedding_subtypeVal.IsCompletelyMetrizableSpace

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