le_sup — Mathlib

English

Let α be a type with a semilattice structure and a bottom element. For any multiset s of α and any a ∈ s, we have a ≤ s.sup.

Русский

Пусть α — множество с полусположением и нижней границей. Для любого мультимножества s ⊆ α и любого a ∈ s верно a ≤ sup s.

LaTeX

$$$$ \\forall s:\\mathrm{Multiset}(\\alpha), \\forall a \\in s,\\ a \\le \\sup s $$$$

Lean4

theorem le_sup {s : Multiset α} {a : α} (h : a ∈ s) : a ≤ s.sup :=
  sup_le.1 le_rfl _ h

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