# mathlibdocumentation

data.list.min_max

# 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 an with_top α, the smallest element of l for nonempty lists, and ⊤ for []

def list.argmax₂ {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : option α) (b : α) :

Auxiliary definition to define argmax

Equations
def list.argmax {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (l : list α) :

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

Equations
• l = l
def list.argmin {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (l : list α) :

argmin f l returns some a, where a of l that minimises 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. argmin f [] = none

Equations
• l = l
@[simp]
theorem list.argmax_two_self {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) :
(some a) a = a
@[simp]
theorem list.argmax_nil {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) :
@[simp]
theorem list.argmin_nil {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) :
@[simp]
theorem list.argmax_singleton {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {a : α} :
[a] = some a
@[simp]
theorem list.argmin_singleton {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {a : α} :
[a] = a
@[simp]
theorem list.foldl_argmax₂_eq_none {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} {o : option α} :
o l = none
theorem list.argmax_mem {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} {m : α} :
m lm l
theorem list.argmin_mem {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} {m : α} :
m lm l
@[simp]
theorem list.argmax_eq_none {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} :
l = none
@[simp]
theorem list.argmin_eq_none {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {l : list α} :
l = none
theorem list.le_argmax_of_mem {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {a m : α} {l : list α} :
a lm lf a f m
theorem list.argmin_le_of_mem {α : Type u_1} {β : Type u_2} [linear_order β] {f : α → β} {a m : α} {l : list α} :
a lm lf m f a
theorem list.argmax_concat {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) (l : list α) :
(l ++ [a]) = l).cases_on (some a) (λ (c : α), ite (f a f c) (some c) (some a))
theorem list.argmin_concat {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) (l : list α) :
(l ++ [a]) = l).cases_on (some a) (λ (c : α), ite (f c f a) (some c) (some a))
theorem list.argmax_cons {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) (l : list α) :
(a :: l) = l).cases_on (some a) (λ (c : α), ite (f c f a) (some a) (some c))
theorem list.argmin_cons {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) (a : α) (l : list α) :
(a :: l) = l).cases_on (some a) (λ (c : α), ite (f a f c) (some a) (some c))
theorem list.index_of_argmax {α : Type u_1} {β : Type u_2} [linear_order β] [decidable_eq α] {f : α → β} {l : list α} {m : α} :
m l∀ {a : α}, a lf m f a
theorem list.index_of_argmin {α : Type u_1} {β : Type u_2} [linear_order β] [decidable_eq α] {f : α → β} {l : list α} {m : α} :
m l∀ {a : α}, a lf a f m
theorem list.mem_argmax_iff {α : Type u_1} {β : Type u_2} [linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
m l 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} [linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
l = 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} [linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
m l 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} [linear_order β] [decidable_eq α] {f : α → β} {m : α} {l : list α} :
l = some m m l (∀ (a : α), a lf m f a) ∀ (a : α), a lf a f m
def list.maximum {α : Type u_1} [linear_order α] (l : list α) :

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

Equations
def list.minimum {α : Type u_1} [linear_order α] (l : list α) :

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

Equations
@[simp]
theorem list.maximum_nil {α : Type u_1} [linear_order α] :
@[simp]
theorem list.minimum_nil {α : Type u_1} [linear_order α] :
@[simp]
theorem list.maximum_singleton {α : Type u_1} [linear_order α] (a : α) :
@[simp]
theorem list.minimum_singleton {α : Type u_1} [linear_order α] (a : α) :
theorem list.maximum_mem {α : Type u_1} [linear_order α] {l : list α} {m : α} :
l.maximum = mm l
theorem list.minimum_mem {α : Type u_1} [linear_order α] {l : list α} {m : α} :
l.minimum = mm l
@[simp]
theorem list.maximum_eq_none {α : Type u_1} [linear_order α] {l : list α} :
@[simp]
theorem list.minimum_eq_none {α : Type u_1} [linear_order α] {l : list α} :
theorem list.le_maximum_of_mem {α : Type u_1} [linear_order α] {a m : α} {l : list α} :
a ll.maximum = ma m
theorem list.minimum_le_of_mem {α : Type u_1} [linear_order α] {a m : α} {l : list α} :
a ll.minimum = mm a
theorem list.le_maximum_of_mem' {α : Type u_1} [linear_order α] {a : α} {l : list α} (ha : a l) :
theorem list.le_minimum_of_mem' {α : Type u_1} [linear_order α] {a : α} {l : list α} (ha : a l) :
theorem list.maximum_concat {α : Type u_1} [linear_order α] (a : α) (l : list α) :
(l ++ [a]).maximum = a
theorem list.minimum_concat {α : Type u_1} [linear_order α] (a : α) (l : list α) :
(l ++ [a]).minimum = a
theorem list.maximum_cons {α : Type u_1} [linear_order α] (a : α) (l : list α) :
theorem list.minimum_cons {α : Type u_1} [linear_order α] (a : α) (l : list α) :
theorem list.maximum_eq_coe_iff {α : Type u_1} [linear_order α] {m : α} {l : list α} :
l.maximum = m m l ∀ (a : α), a la m
theorem list.minimum_eq_coe_iff {α : Type u_1} [linear_order α] {m : α} {l : list α} :
l.minimum = m m l ∀ (a : α), a lm a

Note: since there is no typeclass for both linear_order and has_top, nor a typeclass dual to canonically_linear_ordered_add_monoid α we cannot express these lemmas generally for minimum; instead we are limited to doing so on order_dual α`.

theorem list.maximum_eq_coe_foldr_max_of_ne_nil {M : Type u_3} (l : list M) (h : l list.nil) :
theorem list.minimum_eq_coe_foldr_min_of_ne_nil {M : Type u_3} (l : list (order_dual M)) (h : l list.nil) :
theorem list.max_le_of_forall_le {M : Type u_3} (l : list M) (n : M) (h : ∀ (x : M), x lx n) :
n
theorem list.le_min_of_le_forall {M : Type u_3} (l : list (order_dual M)) (n : order_dual M) (h : ∀ (x : , x ln x) :
n
theorem list.max_nat_le_of_forall_le (l : list ) (n : ) (h : ∀ (x : ), x lx n) :
l n