l_sSup — Mathlib

English

Let α and β be complete lattices and l,u form a Galois connection. For any subset s ⊆ α, l(sup s) = sup { l(a) : a ∈ s }. In words, l preserves suprema over sets.

Русский

Пусть α и β — полные решетки и связь Галуа между ними. Для любого подмножества s ⊆ α выполняется: l( sup s ) = sup { l(a) : a ∈ s }. То есть l сохраняет верхние границы.

LaTeX

$$$${l(\\sup s) = \\sup\\{\,l(a) : a \\in s\\,\\}}.$$$$

Lean4

theorem l_sSup {s : Set α} : l (sSup s) = ⨆ a ∈ s, l a := by simp only [sSup_eq_iSup, gc.l_iSup]

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