isClosed_subsets_of_isClosed — Mathlib

English

If hs is closed, then the set {A ∈ NonemptyCompacts α | A ⊆ s} is closed.

Русский

Если hs замкнуто, множество {A ∈ NonemptyCompacts α | A ⊆ s} замкнуто.

LaTeX

$$$\\forall hs:\\ IsClosed(s), \\ IsClosed\\{A : NonemptyCompacts α | (A: Set α) \\subseteq s\\}$.$$

Lean4

theorem isClosed_subsets_of_isClosed (hs : IsClosed s) : IsClosed {A : NonemptyCompacts α | (A : Set α) ⊆ s} :=
  (Closeds.isClosed_subsets_of_isClosed hs).preimage continuous_toCloseds

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