English
The aforementioned lattice structure is constructed via a Galois coinsertion with the interior operator; join/meet correspond to union/intersection.
Русский
Указанная выше структура решетки строится через галуа-коинсерцию с помощью оператора interior; объединение/пересечение соответствуют объединению/пересечению.
LaTeX
$$$\text{CompleteLattice}(\mathrm{Opens}(\alpha)) \text{ with } \vee = \cup, \wedge = \cap,$ defined via $\text{gi}$ and $\operatorname{interior}$.$$
Lean4
instance : CompleteLattice (Opens α) :=
CompleteLattice.copy
(GaloisCoinsertion.liftCompleteLattice gi)
-- le
(fun U V => (U : Set α) ⊆ V) rfl ⟨univ, isOpen_univ⟩
(ext interior_univ.symm)
-- bot
⟨∅, isOpen_empty⟩ rfl (fun U V => ⟨↑U ∪ ↑V, U.2.union V.2⟩) rfl (fun U V => ⟨↑U ∩ ↑V, U.2.inter V.2⟩)
(funext₂ fun U V => ext (U.2.inter V.2).interior_eq.symm)
-- sSup
(fun S => ⟨⋃ s ∈ S, ↑s, isOpen_biUnion fun s _ => s.2⟩)
(funext fun _ => ext sSup_image.symm)
-- sInf
_ rfl
