English
The collection of closed subsets of a topological space α, ordered by inclusion, forms a complete lattice. The top element is α itself, the bottom element is ∅, and the lattice operations correspond to set-theoretic union and intersection, with arbitrary unions of closed sets closed by taking closures and finite unions being closed as well; in particular, sup of a family is the closure of the union, and inf is the intersection.
Русский
Множество замкнутых подмножеств пространства α, упорядоченное включением, образует полную решетку. Наивысшее элемент — всё пространство α, наименьшее — пустое множество, операции объединения и пересечения соответствуют объединению и пересечению множеств (произвольные объединения замкнутых множеств замыкаются), а именно: сумма (верх) множества — замыкание объединения, произведение (нижняя граница) — пересечение.
LaTeX
$$$\text{For a topological space } \alpha,\ (\mathrm{Closeds}(\alpha), \subseteq) \text{ is a complete lattice with } \top = \alpha, \bot = \emptyset, \\ C \vee D = C \cup D, \ C \wedge D = C \cap D, \ \bigvee_{i} C_i = \overline{\bigcup_i C_i}, \ \bigwedge_i C_i = \bigcap_i C_i.$$$
Lean4
instance instCompleteLattice : CompleteLattice (Closeds α) :=
CompleteLattice.copy
(GaloisInsertion.liftCompleteLattice gi)
-- le
_ rfl ⟨univ, isClosed_univ⟩ rfl ⟨∅, isClosed_empty⟩
(SetLike.coe_injective closure_empty.symm)
-- sup
(fun s t => ⟨s ∪ t, s.2.union t.2⟩)
(funext fun s => funext fun t => SetLike.coe_injective (s.2.union t.2).closure_eq.symm)
-- inf
(fun s t => ⟨s ∩ t, s.2.inter t.2⟩) rfl _ rfl (fun S => ⟨⋂ s ∈ S, ↑s, isClosed_biInter fun s _ => s.2⟩)
(funext fun _ => SetLike.coe_injective sInf_image.symm)
