# Documentation

Mathlib.Data.List.MinMax

# Minimum and maximum of lists #

## Main definitions #

The main definitions are argmax, argmin, minimum and maximum for lists.

argmax f l returns some a, where a of l that maximises f a. If there are a b such that f a = f b, it returns whichever of a or b comes first in the list. argmax f [] = none

minimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for []

def List.argAux {α : Type u_1} (r : ααProp) [] (a : ) (b : α) :

Auxiliary definition for argmax and argmin.

Instances For
@[simp]
theorem List.foldl_argAux_eq_none {α : Type u_1} (r : ααProp) [] {l : List α} {o : } :
List.foldl () o l = none l = [] o = none
@[simp]
theorem List.argAux_self {α : Type u_1} (r : ααProp) [] (hr₀ : ) (a : α) :
theorem List.not_of_mem_foldl_argAux {α : Type u_1} (r : ααProp) [] {l : List α} (hr₀ : ) (hr₁ : ) {a : α} {m : α} {o : } :
a lm List.foldl () o l¬r a m
def List.argmax {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] (f : αβ) (l : List α) :

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.

Instances For
def List.argmin {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] (f : αβ) (l : List α) :

argmin f l returns some a, where f a is minimal among the elements of l, in the sense that there is no b ∈ l with f b < f a. If a, b are such that f a = f b, it returns whichever of a or b comes first in the list. argmin f [] = none.

Instances For
@[simp]
theorem List.argmax_nil {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] (f : αβ) :
List.argmax f [] = none
@[simp]
theorem List.argmin_nil {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] (f : αβ) :
List.argmin f [] = none
@[simp]
theorem List.argmax_singleton {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {a : α} :
@[simp]
theorem List.argmin_singleton {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {a : α} :
theorem List.not_lt_of_mem_argmax {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {l : List α} {a : α} {m : α} :
a lm ¬f m < f a
theorem List.not_lt_of_mem_argmin {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {l : List α} {a : α} {m : α} :
a lm ¬f a < f m
theorem List.argmax_concat {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] (f : αβ) (a : α) (l : List α) :
List.argmax f (l ++ [a]) = Option.casesOn () (some a) fun c => if f c < f a then some a else some c
theorem List.argmin_concat {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] (f : αβ) (a : α) (l : List α) :
List.argmin f (l ++ [a]) = Option.casesOn () (some a) fun c => if f a < f c then some a else some c
theorem List.argmax_mem {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {l : List α} {m : α} :
m m l
theorem List.argmin_mem {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {l : List α} {m : α} :
m m l
@[simp]
theorem List.argmax_eq_none {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {l : List α} :
= none l = []
@[simp]
theorem List.argmin_eq_none {α : Type u_1} {β : Type u_2} [] [DecidableRel fun x x_1 => x < x_1] {f : αβ} {l : List α} :
= none l = []
theorem List.le_of_mem_argmax {α : Type u_1} {β : Type u_2} [] {f : αβ} {l : List α} {a : α} {m : α} :
a lm f a f m
theorem List.le_of_mem_argmin {α : Type u_1} {β : Type u_2} [] {f : αβ} {l : List α} {a : α} {m : α} :
a lm f m f a
theorem List.argmax_cons {α : Type u_1} {β : Type u_2} [] (f : αβ) (a : α) (l : List α) :
List.argmax f (a :: l) = Option.casesOn () (some a) fun c => if f a < f c then some c else some a
theorem List.argmin_cons {α : Type u_1} {β : Type u_2} [] (f : αβ) (a : α) (l : List α) :
List.argmin f (a :: l) = Option.casesOn () (some a) fun c => if f c < f a then some c else some a
theorem List.index_of_argmax {α : Type u_1} {β : Type u_2} [] {f : αβ} [] {l : List α} {m : α} :
m ∀ {a : α}, a lf m f a
theorem List.index_of_argmin {α : Type u_1} {β : Type u_2} [] {f : αβ} [] {l : List α} {m : α} :
m ∀ {a : α}, a lf a f m
theorem List.mem_argmax_iff {α : Type u_1} {β : Type u_2} [] {f : αβ} {l : List α} {m : α} [] :
m m l (∀ (a : α), a lf a f m) ∀ (a : α), a lf m f a
theorem List.argmax_eq_some_iff {α : Type u_1} {β : Type u_2} [] {f : αβ} {l : List α} {m : α} [] :
= some m m l (∀ (a : α), a lf a f m) ∀ (a : α), a lf m f a
theorem List.mem_argmin_iff {α : Type u_1} {β : Type u_2} [] {f : αβ} {l : List α} {m : α} [] :
m m l (∀ (a : α), a lf m f a) ∀ (a : α), a lf a f m
theorem List.argmin_eq_some_iff {α : Type u_1} {β : Type u_2} [] {f : αβ} {l : List α} {m : α} [] :
= some m m l (∀ (a : α), a lf m f a) ∀ (a : α), a lf a f m
def List.maximum {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] (l : List α) :

maximum l returns a WithBot α, the largest element of l for nonempty lists, and ⊥ for []

Instances For
def List.minimum {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] (l : List α) :

minimum l returns a WithTop α, the smallest element of l for nonempty lists, and ⊤ for []

Instances For
@[simp]
theorem List.maximum_nil {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] :
@[simp]
theorem List.minimum_nil {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] :
@[simp]
theorem List.maximum_singleton {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] (a : α) :
List.maximum [a] = a
@[simp]
theorem List.minimum_singleton {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] (a : α) :
List.minimum [a] = a
theorem List.maximum_mem {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} {m : α} :
= mm l
theorem List.minimum_mem {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} {m : α} :
= mm l
@[simp]
theorem List.maximum_eq_none {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} :
= none l = []
@[simp]
theorem List.minimum_eq_none {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} :
= none l = []
theorem List.not_lt_maximum_of_mem {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} {a : α} {m : α} :
a l = m¬m < a
theorem List.minimum_not_lt_of_mem {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} {a : α} {m : α} :
a l = m¬a < m
theorem List.not_lt_maximum_of_mem' {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} {a : α} (ha : a l) :
¬ < a
theorem List.not_lt_minimum_of_mem' {α : Type u_1} [] [DecidableRel fun x x_1 => x < x_1] {l : List α} {a : α} (ha : a l) :
¬a <
theorem List.maximum_concat {α : Type u_1} [] (a : α) (l : List α) :
List.maximum (l ++ [a]) = max () a
theorem List.le_maximum_of_mem {α : Type u_1} [] {l : List α} {a : α} {m : α} :
a l = ma m
theorem List.minimum_le_of_mem {α : Type u_1} [] {l : List α} {a : α} {m : α} :
a l = mm a
theorem List.le_maximum_of_mem' {α : Type u_1} [] {l : List α} {a : α} (ha : a l) :
a
theorem List.minimum_le_of_mem' {α : Type u_1} [] {l : List α} {a : α} (ha : a l) :
a
theorem List.minimum_concat {α : Type u_1} [] (a : α) (l : List α) :
List.minimum (l ++ [a]) = min () a
theorem List.maximum_cons {α : Type u_1} [] (a : α) (l : List α) :
List.maximum (a :: l) = max (a) ()
theorem List.minimum_cons {α : Type u_1} [] (a : α) (l : List α) :
List.minimum (a :: l) = min (a) ()
theorem List.maximum_le_of_forall_le {α : Type u_1} [] {l : List α} {b : } (h : ∀ (a : α), a la b) :
theorem List.le_minimum_of_forall_le {α : Type u_1} [] {l : List α} {b : } (h : ∀ (a : α), a lb a) :
theorem List.maximum_eq_coe_iff {α : Type u_1} [] {l : List α} {m : α} :
= m m l ∀ (a : α), a la m
theorem List.minimum_eq_coe_iff {α : Type u_1} [] {l : List α} {m : α} :
= m m l ∀ (a : α), a lm a
theorem List.coe_le_maximum_iff {α : Type u_1} [] {l : List α} {a : α} :
a b, b l a b
theorem List.minimum_le_coe_iff {α : Type u_1} [] {l : List α} {a : α} :
a b, b l b a
theorem List.maximum_ne_bot_of_ne_nil {α : Type u_1} [] {l : List α} (h : l []) :
theorem List.minimum_ne_top_of_ne_nil {α : Type u_1} [] {l : List α} (h : l []) :
theorem List.maximum_ne_bot_of_length_pos {α : Type u_1} [] {l : List α} (h : 0 < ) :
theorem List.minimum_ne_top_of_length_pos {α : Type u_1} [] {l : List α} (h : 0 < ) :
def List.maximum_of_length_pos {α : Type u_1} [] {l : List α} (h : 0 < ) :
α

The maximum value in a non-empty List.

Instances For
def List.minimum_of_length_pos {α : Type u_1} [] {l : List α} (h : 0 < ) :
α

The minimum value in a non-empty List.

Instances For
@[simp]
theorem List.coe_maximum_of_length_pos {α : Type u_1} [] {l : List α} (h : 0 < ) :
@[simp]
theorem List.coe_minimum_of_length_pos {α : Type u_1} [] {l : List α} (h : 0 < ) :
@[simp]
theorem List.le_maximum_of_length_pos_iff {α : Type u_1} [] {l : List α} {b : α} (h : 0 < ) :
b
@[simp]
theorem List.minimum_of_length_pos_le_iff {α : Type u_1} [] {l : List α} {b : α} (h : 0 < ) :
b
theorem List.le_maximum_of_length_pos_of_mem {α : Type u_1} [] {l : List α} {a : α} (h : a l) (w : 0 < ) :
theorem List.minimum_of_length_pos_le_of_mem {α : Type u_1} [] {l : List α} {a : α} (h : a l) (w : 0 < ) :
theorem List.getElem_le_maximum_of_length_pos {α : Type u_1} [] {l : List α} {i : } (w : i < ) (h : optParam (0 < ) (_ : 0 < )) :
theorem List.minimum_of_length_pos_le_getElem {α : Type u_1} [] {l : List α} {i : } (w : i < ) (h : optParam (0 < ) (_ : 0 < )) :
@[simp]
theorem List.foldr_max_of_ne_nil {α : Type u_1} [] [] {l : List α} (h : l []) :
↑(List.foldr max l) =
theorem List.max_le_of_forall_le {α : Type u_1} [] [] (l : List α) (a : α) (h : ∀ (x : α), x lx a) :
theorem List.le_max_of_le {α : Type u_1} [] [] {l : List α} {a : α} {x : α} (hx : x l) (h : a x) :
@[simp]
theorem List.foldr_min_of_ne_nil {α : Type u_1} [] [] {l : List α} (h : l []) :
↑(List.foldr min l) =
theorem List.le_min_of_forall_le {α : Type u_1} [] [] (l : List α) (a : α) (h : ∀ (x : α), x la x) :
theorem List.min_le_of_le {α : Type u_1} [] [] (l : List α) (a : α) {x : α} (hx : x l) (h : x a) :