English
Let α be a topological space and assume α is compact. Then the family of compact subsets of α, denoted Compacts α, forms a bounded lattice under inclusion, with bottom ∅ and top α (the top exists when α is compact). The join of two compact subsets corresponds to their union, and the meet corresponds to their intersection (the latter under a Hausdorff condition).
Русский
Пусть α — топологическое пространство и α компактно. Тогда множество компактных подмножеств α образует ограниченную решётку по включению, с наименьшим элементом ∅ и наибольшим элементом α (верхний элемент существует, если α компактно). Объединение двух компактных подмножеств соответствует их объединению, а их пересечение — их пересечению (пересечение — подмножество компактно в условиях Хаусдорфа).
LaTeX
$$$\\forall \\alpha [\\text{TopologicalSpace }\\alpha], [\\text{CompactSpace }\\alpha] \\,\\Rightarrow \\\\ (\\mathrm{Compacts}(\\alpha), \\le) \text{ is a bounded lattice with } \\\\ \\top = \\text{univ}, \\ \\bot = \\varnothing, \\\\ s \\lor t = s \\cup t, \\\\ s \\land t = s \\cap t \ (\\text{the latter for } T_2).$$
Lean4
instance [CompactSpace α] : BoundedOrder (Compacts α) :=
BoundedOrder.lift ((↑) : _ → Set α) (fun _ _ => id) rfl rfl
