argmax_concat

Mathlib.Data.List.MinMax

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

← MathLib Explorer

English

If m ∈ argmax f l, then m ∈ l.

Русский

Если m ∈ argmax f l, то m ∈ l.

LaTeX

$$$ m \in \operatorname{argmax} f l \Rightarrow m \in l $$$

Lean4

theorem argmax_concat (f : α → β) (a : α) (l : List α) :
    argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c => if f c < f a then some a else some c := by
  rw [argmax, argmax]; simp [argAux]

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

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

Разделы

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

Аффилиация

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