le_maximum_of_mem'

Mathlib.Data.List.MinMax

URI: https://scilib.ai/kg/mathlib#List.le_maximum_of_mem'

English

For any a ∈ l, a ≤ maximum l.

Русский

Для любого a ∈ l выполняется a ≤ максимума l.

LaTeX

$$$\forall a.\; a \in l \rightarrow (a : \mathrm{WithBot}\; \alpha) \le \operatorname{maximum} l$$$

Lean4

theorem le_maximum_of_mem' (ha : a ∈ l) : (a : WithBot α) ≤ maximum l :=
  le_of_not_gt <| not_maximum_lt_of_mem' ha

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

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

Разделы

Аффилиация

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