gc_Ici_sInf — Mathlib

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

Похожие утверждения