English
The complement map gives a bijection between closed sets and open sets: Closeds α ↔ Opens α, with inverse given by taking complements. In particular, every closed set is uniquely the complement of some open set and vice versa.
Русский
Отображение комплемента задаёт биекцию между замкнутыми и открытыми множествами: Closeds α и Opens α эквивалентны через замену на комплемент; каждому замкнутому соответствует единственный открытый комплемент, и наоборот.
LaTeX
$$$ \\text{Closeds}(\\alpha) \\xrightarrow{\\ ;\\ }\n\\text{Opens}(\\alpha) \\quad \\text{is bijective with inverse } \\text{Opens}(\\alpha) \\xrightarrow{\\ ;\\ } \\text{Closeds}(\\alpha).$$$
Lean4
theorem compl_bijective : Function.Bijective (@Closeds.compl α _) :=
Function.bijective_iff_has_inverse.mpr ⟨Opens.compl, Closeds.compl_compl, Opens.compl_compl⟩
