not_maximum_lt_of_mem

Mathlib.Data.List.MinMax

URI: https://scilib.ai/kg/mathlib#List.not_maximum_lt_of_mem

English

If a ∈ l and maximum l = m, then m is not less than a.

Русский

Если a ∈ l и максимум списка равен m, то m не меньше a; эквивалентно ¬(m < a).

LaTeX

$$$\forall \{l\: \alpha\: \}, \; a \in l \rightarrow (\operatorname{maximum} l : \mathrm{WithBot}\; \alpha) = m \rightarrow \neg m < a$$$

Lean4

theorem not_maximum_lt_of_mem : a ∈ l → (maximum l : WithBot α) = m → ¬m < a :=
  not_lt_of_mem_argmax

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

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

Разделы

Аффилиация

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