Theorems · Theorem · order theory

List.argmax_concat

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableLT β] (f : α → β) (a : α) (l : List α),
  List.argmax f (l ++ [a]) = Option.casesOn (List.argmax f l) (some a) fun c => if f c < f a then some a else some c

Defined in

Mathlib.Data.List.MinMax

Cited by

2 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

PreorderDecidableLT