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