not_lt_minimum_of_mem

Mathlib.Data.List.MinMax

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

English

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

Русский

Если a ∈ l и минимум списка равен m, то a не меньше m.

LaTeX

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

Lean4

theorem not_lt_minimum_of_mem : a ∈ l → (minimum l : WithTop α) = m → ¬a < m :=
  not_lt_of_mem_argmin

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

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

Разделы

Аффилиация

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