Theorems · Definition · order theory

List.argmax

{α : Type u_1} → {β : Type u_2} → [inst : Preorder β] → [DecidableLT β] → (α → β) → List α → Option α

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.

Defined in

Mathlib.Data.List.MinMax

Cited by

15 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PreorderDecidableLT