English
There is an order isomorphism between the lattice of closed sets and the order dual of the lattice of open sets, given by taking complements.
Русский
Существует отображение, являющееся порядковым изоморфизмом между решеткой замкнутых множеств и порядковым двойником решетки открытых множеств, заданное взятием комплемента.
LaTeX
$$$ \\operatorname{Closeds}(\\alpha) \\cong_o (\\operatorname{Opens}(\\alpha))^{\\mathrm{op}}. $$$
Lean4
/-- `TopologicalSpace.Closeds.compl` as an `OrderIso` to the order dual of
`TopologicalSpace.Opens α`. -/
@[simps]
def complOrderIso : Closeds α ≃o (Opens α)ᵒᵈ
where
toFun := OrderDual.toDual ∘ Closeds.compl
invFun := Opens.compl ∘ OrderDual.ofDual
left_inv s := by simp [Closeds.compl_compl]
right_inv s := by simp [Opens.compl_compl]
map_rel_iff' := (@OrderDual.toDual_le_toDual (Opens α)).trans compl_subset_compl
