# Lemmas about `List.min?` and `List.max?. #

## Minima and maxima #

### min? #

source
@[simp]
theorem List.min?_nil {α : Type u_1} [Min α] :
[].min? = none
source
theorem List.min?_cons' {α : Type u_1} {x : α} [Min α] {xs : List α} :
(x :: xs).min? = some (foldl min x xs)
source
@[simp]
theorem List.min?_cons {α : Type u_1} {x : α} [Min α] [Std.Associative min] {xs : List α} :
(x :: xs).min? = some (xs.min?.elim x (min x))
source
@[simp]
theorem List.min?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] :
xs.min? = none ↔ xs = []
source
theorem List.isSome_min?_of_mem {α : Type u_1} {l : List α} [Min α] {a : α} (h : a ∈ l) :
l.min?.isSome = true
source
theorem List.min?_eq_head? {α : Type u} [Min α] {l : List α} (h : Pairwise (fun (a b : α) => min a b = a) l) :
l.min? = l.head?
source
theorem List.min?_mem {α : Type u_1} {a : α} [Min α] [Std.MinEqOr α] {xs : List α} :
xs.min? = some a → a ∈ xs
source
theorem List.le_min?_iff {α : Type u_1} {a : α} [Min α] [LE α] [Std.LawfulOrderInf α] {xs : List α} :
xs.min? = some a → ∀ {x : α}, x ≤ a ↔ ∀ (b : α), b ∈ xs → x ≤ b
source
theorem List.min?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] {xs : List α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α] :
xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b
source
theorem List.min?_eq_min?_attach {α : Type u_1} [Min α] [Std.MinEqOr α] {xs : List α} :
xs.min? = Option.map Subtype.val xs.attach.min?
source
theorem List.min?_eq_some_iff_subtype {α : Type u_1} {a : α} [Min α] [LE α] {xs : List α} [Std.MinEqOr α] [Std.IsLinearOrder { x : α // x ∈ xs }] [Std.LawfulOrderMin { x : α // x ∈ xs }] :
xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b
source
theorem List.min?_replicate {α : Type u_1} [Min α] [Std.IdempotentOp min] {n : Nat} {a : α} :
(replicate n a).min? = if n = 0 then none else some a
source
@[simp]
theorem List.min?_replicate_of_pos {α : Type u_1} [Min α] [Std.MinEqOr α] {n : Nat} {a : α} (h : 0 < n) :
(replicate n a).min? = some a
source
theorem List.foldl_min {α : Type u_1} [Min α] [Std.IdempotentOp min] [Std.Associative min] {l : List α} {a : α} :
foldl min a l = min a (l.min?.getD a)

This lemma is also applicable given the following instances:

    [LE α] [Min α] [IsLinearOrder α] [LawfulOrderMin α]

### max? #

source
@[simp]
theorem List.max?_nil {α : Type u_1} [Max α] :
[].max? = none
source
theorem List.max?_cons' {α : Type u_1} {x : α} [Max α] {xs : List α} :
(x :: xs).max? = some (foldl max x xs)
source
@[simp]
theorem List.max?_cons {α : Type u_1} {x : α} [Max α] [Std.Associative max] {xs : List α} :
(x :: xs).max? = some (xs.max?.elim x (max x))
source
@[simp]
theorem List.max?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] :
xs.max? = none ↔ xs = []
source
theorem List.isSome_max?_of_mem {α : Type u_1} {l : List α} [Max α] {a : α} (h : a ∈ l) :
l.max?.isSome = true
source
theorem List.max?_eq_head? {α : Type u} [Max α] {l : List α} (h : Pairwise (fun (a b : α) => max a b = a) l) :
l.max? = l.head?
source
theorem List.max?_mem {α : Type u_1} {a : α} [Max α] [Std.MaxEqOr α] {xs : List α} :
xs.max? = some a → a ∈ xs
source
theorem List.max?_le_iff {α : Type u_1} {a : α} [Max α] [LE α] [Std.LawfulOrderSup α] {xs : List α} :
xs.max? = some a → ∀ {x : α}, a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x
source
theorem List.max?_eq_some_iff {α : Type u_1} {a : α} [Max α] [LE α] {xs : List α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α] :
xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a
source
theorem List.max?_eq_max?_attach {α : Type u_1} [Max α] [Std.MaxEqOr α] {xs : List α} :
xs.max? = Option.map Subtype.val xs.attach.max?
source
theorem List.max?_eq_some_iff_subtype {α : Type u_1} {a : α} [Max α] [LE α] {xs : List α} [Std.MaxEqOr α] [Std.IsLinearOrder { x : α // x ∈ xs }] [Std.LawfulOrderMax { x : α // x ∈ xs }] :
xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a
source
@[deprecated List.max?_eq_some_iff (since := "2025-08-01")]
theorem List.max?_eq_some_iff_legacy {α : Type u_1} {a : α} [Max α] [LE α] [anti : Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2] (le_refl : ∀ (a : α), a ≤ a) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a
source
theorem List.max?_replicate {α : Type u_1} [Max α] [Std.IdempotentOp max] {n : Nat} {a : α} :
(replicate n a).max? = if n = 0 then none else some a
source
@[simp]
theorem List.max?_replicate_of_pos {α : Type u_1} [Max α] [Std.MaxEqOr α] {n : Nat} {a : α} (h : 0 < n) :
(replicate n a).max? = some a
source
theorem List.foldl_max {α : Type u_1} [Max α] [Std.IdempotentOp max] [Std.Associative max] {l : List α} {a : α} :
foldl max a l = max a (l.max?.getD a)

This lemma is also applicable given the following instances:

    [LE α] [Min α] [IsLinearOrder α] [LawfulOrderMax α]