English
Let f be a function α → β with β a preorder. Then the minimum over l ++ [a] is either a or the previous minimum, depending on f-values reversed.
Русский
Пусть f : α → β, β — частичный порядок. Тогда минимум по списку l ∪ {a} равен либо a, либо прежнему минимуму в l, в зависимости от значений f.
LaTeX
$$$\operatorname{argmin} f (l \cup \{a\}) = \begin{cases} \operatorname{Some} a & \text{если } \operatorname{argmin} f l = \mathrm{None},\\[2pt] \text{иначе } \text{если } f a < f c \text{ для соответствующего } c, \text{ то } \operatorname{Some} a, \text{иначе } \operatorname{Some} c. \end{cases}$$$
Lean4
/-- `argmin f l` returns `some a`, where `f a` is minimal among the elements of `l`, in the sense
that there is no `b ∈ l` with `f b < f a`. If `a`, `b` are such that `f a = f b`, it returns
whichever of `a` or `b` comes first in the list. `argmin f [] = none`. -/
def argmin (f : α → β) (l : List α) :=
l.foldl (argAux fun b c => f b < f c) none
