English
Let l,u form a Galois connection between α and β. For any nonempty and upper-bounded set s ⊆ α, l(sup s) = sup l(s).
Русский
Пусть l,u образуют сопряжение Гали между α и β. Для непустого верхнеограниченного множества s ⊆ α выполняется l( sup s ) = sup{ l(x) : x ∈ s }.
LaTeX
$$$ \text{gc} : \text{GaloisConnection } l u \Rightarrow l(\mathrm{sSup} s) = \bigvee_{x \in s} l(x) $$$
Lean4
theorem l_csSup (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
l (sSup s) = ⨆ x : s, l x :=
Eq.symm <| IsLUB.ciSup_set_eq (gc.isLUB_l_image <| isLUB_csSup hne hbdd) hne