compactSpace — Mathlib

English

If α is a CompactSpace, then NonemptyCompacts α is a CompactSpace.

Русский

Если α компактно, то NonemptyCompacts α компактно.

LaTeX

$$$[\\text{CompactSpace }\\alpha] \\Rightarrow \\text{CompactSpace}(\\text{NonemptyCompacts }\\alpha).$$$

Lean4

/-- In a compact space, the type of nonempty compact subsets is compact. This follows from
the same statement for closed subsets -/
instance compactSpace [CompactSpace α] : CompactSpace (NonemptyCompacts α) :=
  ⟨by
    rw [isometry_toCloseds.isEmbedding.isCompact_iff, image_univ]
    exact isClosed_in_closeds.isCompact⟩

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