not_lt_of_mem_argmin

Mathlib.Data.List.MinMax

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

← MathLib Explorer

English

If a ∈ l and m ∈ argmin f l, then not f a < f m.

Русский

Если a ∈ l и m ∈ argmin f l, то не f a < f m.

LaTeX

$$$ a \in l \to m \in \operatorname{argmin} f l \to \neg (f a < f m)$$$

Lean4

theorem not_lt_of_mem_argmin : a ∈ l → m ∈ argmin f l → ¬f a < f m :=
  not_of_mem_foldl_argAux _ (fun x h => lt_irrefl (f x) h) (fun x _ _ hxy hyz => lt_trans (a := f x) hxy hyz)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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