English
For any α that is a complete semilattice with supremum, the maps sSup : Set α → α and Iic : α → Set α form a Galois connection. Equivalently, for all s ⊆ α and a ∈ α, sSup s ≤ a iff s ⊆ Iic a.
Русский
Для полной полусвязи с верхами (semilattice) отображения sSup и Iic образуют связь Галуа. Эквивалентно: для любых s ⊆ α и a ∈ α верно sSup s ≤ a эквивалентно s ⊆ Iic a.
LaTeX
$$$$ \\forall s \\subseteq \\alpha,\\; s\\!\\!\\!Sup(s) \\le a \\iff s \\subseteq \\mathrm{Iic}(a). $$$$
Lean4
/-- `sSup` and `Iic` form a Galois connection. -/
theorem gc_sSup_Iic [CompleteSemilatticeSup α] : GaloisConnection (sSup : Set α → α) (Iic : α → Set α) := fun _ _ ↦
sSup_le_iff
