le_max

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.le_max

English

For any element a in the finite set s, a is at most the maximum of s.

Русский

Для любого элемента a в множестве s выполняется a ≤ max s.

LaTeX

$$$a \in s \Rightarrow a \le s_{\max}$$$

Lean4

theorem le_max {a : α} {s : Finset α} (as : a ∈ s) : ↑a ≤ s.max :=
  le_sup as

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru