English
Let f be a function from α to a linearly ordered β, and let a be an element of α and l a list of elements of α. Then the minimum of the list a :: l with respect to f is determined by the tail: if the tail has a minimum (argmin f l = some c), compare f c with f a; if f c < f a then the minimum is c, otherwise it is a. If the tail is empty (argmin f l = none), then the minimum is a.
Русский
Пусть f: α → β, β упорядованная линейно, l — список элементов α, и a ∈ α. Тогда минимум списка a :: l по отношению к f определяется так: если у хвоста есть минимум (argmin f l = some c), то сравниваем f c и f a; если f c < f a, минимум равен c, иначе минимум равен a. Если хвост пуст, то минимум равен a.
LaTeX
$$$\operatorname{argmin} f (a \,\mathbin{::} l) = \operatorname{Option.casesOn}(\operatorname{argmin} f l) (\operatorname{some} a) (\lambda c.\; \text{if } f c < f a \text{ then } \operatorname{some} c \text{ else } \operatorname{some} a)$$$
Lean4
theorem argmin_cons (f : α → β) (a : α) (l : List α) :
argmin f (a :: l) = Option.casesOn (argmin f l) (some a) fun c => if f c < f a then some c else some a :=
@argmax_cons α βᵒᵈ _ _ _ _
