English
For a complete semilattice Inf α, the pair (toDual ∘ Ici, sInf ∘ ofDual) forms a Galois connection between α and its dual order.
Русский
Для полной части Inf α пара (toDual ∘ Ici, sInf ∘ ofDual) образует связь Галуа между α и его двойственным порядком.
LaTeX
$$$$ GaloisConnection (toDual \\circ Ici : α \\to (Set α)^{\\mathrm{op}}) (sInf \\circ ofDual : (Set α)^{\\mathrm{op}} \\to α). $$$$
Lean4
/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois connection. -/
theorem gc_Ici_sInf [CompleteSemilatticeInf α] :
GaloisConnection (toDual ∘ Ici : α → (Set α)ᵒᵈ) (sInf ∘ ofDual : (Set α)ᵒᵈ → α) := fun _ _ ↦ le_sInf_iff.symm