English
Let l be a list, f a function to a linearly ordered type, and m an element. Then m belongs to argmax f l if and only if m belongs to l and, for all a ∈ l, f a ≤ f m, and for all a ∈ l, if f m ≤ f a then l.idxOf m l ≤ l.idxOf a l.
Русский
Пусть список l, функция f, и элемент m. Тогда m принадлежит argmax f l тогда и только тогда, когда m принадлежит l и для всех a ∈ l выполняется f a ≤ f m, а для всех a ∈ l выполнено f m ≤ f a → idxOf m l ≤ idxOf a l.
LaTeX
$$$\ operatorname{mem_argmax} f l \\Leftrightarrow \ m \in l \land (\forall a \in l, f a \le f m) \land (\forall a \in l, f m \le f a \rightarrow l.idxOf m l \le l.idxOf a l) $$$
Lean4
theorem mem_argmax_iff : m ∈ argmax f l ↔ m ∈ l ∧ (∀ a ∈ l, f a ≤ f m) ∧ ∀ a ∈ l, f m ≤ f a → l.idxOf m ≤ l.idxOf a :=
⟨fun hm => ⟨argmax_mem hm, fun _ ha => le_of_mem_argmax ha hm, fun _ => index_of_argmax hm⟩,
by
rintro ⟨hml, ham, hma⟩
rcases harg : argmax f l with - | n
· simp_all
· have :=
_root_.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
(index_of_argmax harg hml (ham _ (argmax_mem harg)))
rw [(idxOf_inj hml (argmax_mem harg)).1 this, Option.mem_def]⟩
