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