English
For a preorder α with a bottom/top extension, the minimum of l is defined as the argmin of the identity function on l, yielding the smallest element of l in the preorder, with empty list giving the top element.
Русский
Для частично упорядоченного множества α с дополнением, минимум списка задаётся как аргмин идентичной функции на l, т.е. наименьший элемент списка; пустой список соответствует верхней границе.
LaTeX
$$$\operatorname{minimum} l := \operatorname{argmin} \mathrm{id} \, l$$
Lean4
/-- `minimum l` returns a `WithTop α`, the smallest element of `l` for nonempty lists, and `⊤` for
`[]` -/
def minimum (l : List α) : WithTop α :=
argmin id l
