English
For α a complete semilattice with Inf, the pair of maps toDual ∘ Ici and sInf ∘ ofDual form a Galois coinsertion between (α, Set α) considered with the dual order.
Русский
Для α, обладающего полной полупоследовательностью Inf, пары отображений toDual ∘ Ici и sInf ∘ ofDual образуют коинсерцию Галуа между α и множеством α, рассматриваемым в двойственном порядке.
LaTeX
$$$\mathrm{GaloisCoinsertion}(\mathrm{toDual} \circ \mathrm{Ici}, \mathrm{sInf} \circ \mathrm{ofDual})$$$
Lean4
/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois coinsertion. -/
def gci_Ici_sInf [CompleteSemilatticeInf α] :
GaloisCoinsertion (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α) :=
gc_Ici_sInf.toGaloisCoinsertion fun _ ↦ sInf_le le_rfl
