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