isLUB_sup_id — Mathlib

English

For any finite set s, IsLUB s (s.sup id) holds; i.e., the supremum of s under the identity function is the lub of s.

Русский

Для любого конечного множества s верно IsLUB s (s.sup id); т.е. верхняя грань над s по идентичности является наибольшей верхней гранью множества.

LaTeX

$$$ IsLUB s \\toSet (s.sup id) $$$

Lean4

theorem isLUB_sup_id {s : Finset α} : IsLUB s (s.sup id) := by simpa using isLUB_sup (f := id)

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