English
If s is closed, then the set of closed subsets of α contained in s is closed.
Русский
Если s замкнуто, то множество замкнутых подмножеств α, содержащихся в s, замкнуто.
LaTeX
$$$\\text{IsClosed}(s) \\Rightarrow \\text{IsClosed}\\big\\{t \\in \\text{Closeds }\\alpha \\mid (t: \\text{Set}\\,\\alpha) \\subseteq s\\big\\}.$$$
Lean4
/-- Subsets of a given closed subset form a closed set -/
theorem isClosed_subsets_of_isClosed (hs : IsClosed s) : IsClosed {t : Closeds α | (t : Set α) ⊆ s} :=
by
refine
isClosed_of_closure_subset
fun (t : Closeds α) (ht : t ∈ closure {t : Closeds α | (t : Set α) ⊆ s}) (x : α) (hx : x ∈ t) => ?_
have : x ∈ closure s := by
refine mem_closure_iff.2 fun ε εpos => ?_
obtain ⟨u : Closeds α, hu : u ∈ {t : Closeds α | (t : Set α) ⊆ s}, Dtu : edist t u < ε⟩ :=
mem_closure_iff.1 ht ε εpos
obtain ⟨y : α, hy : y ∈ u, Dxy : edist x y < ε⟩ := exists_edist_lt_of_hausdorffEdist_lt hx Dtu
exact ⟨y, hu hy, Dxy⟩
rwa [hs.closure_eq] at this
