argmax_mem

Mathlib.Data.List.MinMax

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

← MathLib Explorer

English

If m ∈ argmax f l, then m ∈ l (repeated form).

Русский

Если m ∈ argmax f l, то m ∈ l (повторяющаяся формулировка).

LaTeX

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

Lean4

theorem argmax_mem : ∀ {l : List α} {m : α}, m ∈ argmax f l → m ∈ l
  | [], m => by simp
  | hd :: tl, m => by simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m

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

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

Разделы

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

Аффилиация

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