sSup_eq_iSup — Mathlib

English

For a complete lattice α and a set s ⊆ α, sSup s equals the supremum over all a in s of a (i.e., sSup s = ⨆ a ∈ s, a).

Русский

Для полной решетки α множество s ⊆ α, верхняя грань sSup s равна наибольшему элементу множества s, т.е. sSup s = ⨆ a ∈ s, a.

LaTeX

$$$\\\\text{(sSup eq iSup)} \\\\text{for } s:\\\\ Set α,\ \ sSup s = \\\\bigsup_{a \\in s} a$$$

Lean4

theorem sSup_eq_iSup {s : Set α} : sSup s = ⨆ a ∈ s, a :=
  le_antisymm (sSup_le le_iSup₂) (iSup₂_le fun _ => le_sSup)

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