English
If s is closed, then the set of nonempty compact subsets of α contained in s is closed.
Русский
Если s замкнуто, множество не пустых компактных подмножеств α, содержащихся в s, замкнуто.
LaTeX
$$$\\forall s\\, (\\text{IsClosed } s) \\Rightarrow \\text{IsClosed}\\big\\{A : \\text{NonemptyCompacts }\\alpha \\mid (A: Set \\alpha) \\subseteq s\\big\\}.$$$
Lean4
/-- In an emetric space, the type of non-empty compact subsets is an emetric space,
where the edistance is the Hausdorff edistance -/
instance emetricSpace : EMetricSpace (NonemptyCompacts α)
where
edist s t := hausdorffEdist (s : Set α) t
edist_self _ := hausdorffEdist_self
edist_comm _ _ := hausdorffEdist_comm
edist_triangle _ _ _ := hausdorffEdist_triangle
eq_of_edist_eq_zero {s t}
h :=
NonemptyCompacts.ext <|
by
have : closure (s : Set α) = closure t := hausdorffEdist_zero_iff_closure_eq_closure.1 h
rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this
