instTopOfCompactSpace — Mathlib

English

If α is compact, then the space of compact subsets of α has a canonical topological structure with univ as a top element.

Русский

Если α компактно, то множество компактов α (как топологическое пространство) имеет естественную топологическую структуру, верхняя грань равна всегому пространству.

LaTeX

$$$[CompactSpace\,\alpha] \Rightarrow Top (Compacts \alpha)$ with univ as the carrier and isCompact_univ.$$

Lean4

instance [CompactSpace α] : Top (Compacts α) :=
  ⟨⟨univ, isCompact_univ⟩⟩

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