of_isClosed — Mathlib

English

A closed subspace of a proper space is proper.

Русский

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

LaTeX

$$$IsClosed(s) \\Rightarrow\\text{ProperSpace}(s)$$$

Lean4

/-- A closed subspace of a proper space is proper.
This is true for any proper lipschitz map. See `LipschitzWith.properSpace`. -/
theorem of_isClosed {X : Type*} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : IsClosed s) : ProperSpace s :=
  ⟨fun x r ↦
    Topology.IsEmbedding.subtypeVal.isCompact_iff.mpr
      ((isCompact_closedBall x.1 r).of_isClosed_subset (hs.isClosedMap_subtype_val _ isClosed_closedBall)
        (Set.image_subset_iff.mpr subset_rfl))⟩

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