le_of_mem_argmax

Mathlib.Data.List.MinMax

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

English

If a ∈ l and m ∈ argmax f l, then f a ≤ f m.

Русский

Если a ∈ l и m ∈ argmax f l, то f(a) ≤ f(m).

LaTeX

$$$ a \in l \to m \in \operatorname{argmax} f l \to f a \le f m $$$

Lean4

theorem le_of_mem_argmax : a ∈ l → m ∈ argmax f l → f a ≤ f m := fun ha hm => le_of_not_gt <| not_lt_of_mem_argmax ha hm

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

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

Разделы

Аффилиация

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