l_sSup_u_image — Mathlib

English

If a Galois insertion l ⊣ u relates complete lattices α and β, and s is a subset of β, then the image under l of the supremum of u(s) equals the supremum of s: l(sSup(u''s)) = sSup s.

Русский

Если существует Галуа-вставка l ⊣ u между полными решетками α и β, и s ⊆ β, то образ под l от супремума u(s) равен супремуму самой множества: l(sSup(u''s)) = sSup s.

LaTeX

$$$$ l\left( \operatorname{sSup}(u''s) \right) = \operatorname{sSup}(s). $$$$

Lean4

theorem l_sSup_u_image [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) (s : Set β) :
    l (sSup (u '' s)) = sSup s := by rw [sSup_image, gi.l_biSup_u, sSup_eq_iSup]

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