English
Let f be a function from α to a linearly ordered β, and l a list of α. If m is in the argmin of f on l, then for every a in l, if f a ≤ f m then the index of m in l is not greater than the index of a in l.
Русский
Пусть f: α → β, β линейно упорядочена, l — список элементов α. Если m принадлежит argmin f l, то для любого a ∈ l, если f a ≤ f m, то индекс m в l не больше индекса a в l.
LaTeX
$$$\forall l.\; \forall m.\; m \in \operatorname{argmin} f\; l \rightarrow \forall a.\; a \in l \rightarrow f a \le f m \rightarrow l.idxOf m \; l \le l.idxOf a \; l\;$$
Lean4
theorem index_of_argmin : ∀ {l : List α} {m : α}, m ∈ argmin f l → ∀ {a}, a ∈ l → f a ≤ f m → l.idxOf m ≤ l.idxOf a :=
@index_of_argmax _ βᵒᵈ _ _ _
