l_csSup — Mathlib

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

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