l_csSup' — Mathlib

English

For a Galois connection, the equality l(sSup s) = sSup(l''s) holds under nonempty and bounded conditions, equivalently the same statement with a subtype of s.

Русский

Для сопряженного отображения выполняется равенство l( sSup s ) = sSup( l''s ) при не пустоте и ограниченности, эквивалентно той же формулировке через подмножество.

LaTeX

$$$ l(\mathrm{sSup} s) = \mathrm{sSup}(l''s) $$$

Lean4

theorem l_csSup' (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) :
    l (sSup s) = sSup (l '' s) := by rw [gc.l_csSup hne hbdd, sSup_image']

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