English
Let f be a function from α to a linearly ordered β, and l a list of α. If m is in the argmax of f on l, then for every a in l, if f m ≤ f a then the index of m in l is not greater than the index of a in l. In words, the leftmost (first) maximal element occurs no later than any other element with a value at least as large.
Русский
Пусть f: α → β, β линейно упорядочена, l — список элементов α. Если m принадлежит argmax f l, то для любого a ∈ l, если f m ≤ f a, то индекс m в l не больше индекса a в l. Иначе говоря, первый максимальный элемент не позже любого элемента с не меньшим значением.
LaTeX
$$$\forall l.\; \forall m.\; m \in \operatorname{argmax} f\; l \rightarrow \forall a.\; a \in l \rightarrow f m \le f a \rightarrow l.idxOf m \; l \le l.idxOf a \; l\;\text{один}}$$
Lean4
theorem index_of_argmax : ∀ {l : List α} {m : α}, m ∈ argmax f l → ∀ {a}, a ∈ l → f m ≤ f a → l.idxOf m ≤ l.idxOf a
| [], m, _, _, _, _ => by simp
| hd :: tl, m, hm, a, ha, ham =>
by
simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢
cases h : argmax f tl
· rw [h] at hm
simp_all
rw [h] at hm
dsimp only at hm
simp only [cond_eq_if, beq_iff_eq]
obtain ha | ha := ha <;> split_ifs at hm <;> injection hm with hm <;> subst hm
· cases not_le_of_gt ‹_› ‹_›
· rw [if_pos rfl]
· rw [if_neg, if_neg]
· exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
· exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne
· exact ne_of_apply_ne _ ‹f hd < f _›.ne
· rw [if_pos rfl]
exact Nat.zero_le _
