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

Minima and maxima

min?

@[simp]

theorem List.min?_nil {α : Type u_1} [Min α] : [].min? = none

theorem List.min?_cons' {α : Type u_1} {x : α} [Min α] {xs : List α} : (x :: xs).min? = some (foldl min x xs)

@[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))

@[simp]

theorem List.min?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] : xs.min? = none ↔ xs = []

theorem List.isSome_min?_of_mem {α : Type u_1} {l : List α} [Min α] {a : α} (h : a ∈ l) : l.min?.isSome = true

theorem List.min?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) {xs : List α} : xs.min? = some a → a ∈ xs

theorem List.le_min?_iff {α : Type u_1} {a : α} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.min? = some a → ∀ {x : α}, x ≤ a ↔ ∀ (b : α), b ∈ xs → x ≤ b

theorem List.min?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2] (le_refl : ∀ (a : α), a ≤ a) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

theorem List.min?_replicate {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) : (replicate n a).min? = if n = 0 then none else some a

@[simp]

theorem List.min?_replicate_of_pos {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) : (replicate n a).min? = some a

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)

max?

@[simp]

theorem List.max?_nil {α : Type u_1} [Max α] : [].max? = none

theorem List.max?_cons' {α : Type u_1} {x : α} [Max α] {xs : List α} : (x :: xs).max? = some (foldl max x xs)

@[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))

@[simp]

theorem List.max?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] : xs.max? = none ↔ xs = []

theorem List.isSome_max?_of_mem {α : Type u_1} {l : List α} [Max α] {a : α} (h : a ∈ l) : l.max?.isSome = true

theorem List.max?_mem {α : Type u_1} {a : α} [Max α] (min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) {xs : List α} : xs.max? = some a → a ∈ xs

theorem List.max?_le_iff {α : Type u_1} {a : α} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : xs.max? = some a → ∀ {x : α}, a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x

theorem List.max?_eq_some_iff {α : 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

theorem List.max?_replicate {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) : (replicate n a).max? = if n = 0 then none else some a

@[simp]

theorem List.max?_replicate_of_pos {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) : (replicate n a).max? = some a

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)

@[reducible, inline, deprecated List.min?_nil (since := "2024-09-29")]

abbrev List.minimum?_nil {α : Type u_1} [Min α] : [].min? = none

Equations

• @List.minimum?_nil = @List.min?_nil

@[reducible, inline, deprecated List.min?_cons (since := "2024-09-29")]

abbrev List.minimum?_cons {α : Type u_1} {x : α} [Min α] [Std.Associative min] {xs : List α} : (x :: xs).min? = some (xs.min?.elim x (min x))

Equations

• @List.minimum?_cons = @List.min?_cons

@[reducible, inline, deprecated List.min?_eq_none_iff (since := "2024-09-29")]

abbrev List.mininmum?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] : xs.min? = none ↔ xs = []

Equations

• @List.mininmum?_eq_none_iff = @List.min?_eq_none_iff

@[reducible, inline, deprecated List.min?_mem (since := "2024-09-29")]

abbrev List.minimum?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) {xs : List α} : xs.min? = some a → a ∈ xs

Equations

• @List.minimum?_mem = @List.min?_mem

@[reducible, inline, deprecated List.le_min?_iff (since := "2024-09-29")]

abbrev List.le_minimum?_iff {α : Type u_1} {a : α} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.min? = some a → ∀ {x : α}, x ≤ a ↔ ∀ (b : α), b ∈ xs → x ≤ b

Equations

• @List.le_minimum?_iff = @List.le_min?_iff

@[reducible, inline, deprecated List.min?_eq_some_iff (since := "2024-09-29")]

abbrev List.minimum?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2] (le_refl : ∀ (a : α), a ≤ a) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} : xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

Equations

• @List.minimum?_eq_some_iff = @List.min?_eq_some_iff

@[reducible, inline, deprecated List.min?_replicate (since := "2024-09-29")]

abbrev List.minimum?_replicate {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) : (replicate n a).min? = if n = 0 then none else some a

Equations

• @List.minimum?_replicate = @List.min?_replicate

@[reducible, inline, deprecated List.min?_replicate_of_pos (since := "2024-09-29")]

abbrev List.minimum?_replicate_of_pos {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) : (replicate n a).min? = some a

Equations

• @List.minimum?_replicate_of_pos = @List.min?_replicate_of_pos

@[reducible, inline, deprecated List.max?_nil (since := "2024-09-29")]

abbrev List.maximum?_nil {α : Type u_1} [Max α] : [].max? = none

Equations

• @List.maximum?_nil = @List.max?_nil

@[reducible, inline, deprecated List.max?_cons (since := "2024-09-29")]

abbrev List.maximum?_cons {α : Type u_1} {x : α} [Max α] [Std.Associative max] {xs : List α} : (x :: xs).max? = some (xs.max?.elim x (max x))

Equations

• @List.maximum?_cons = @List.max?_cons

@[reducible, inline, deprecated List.max?_eq_none_iff (since := "2024-09-29")]

abbrev List.maximum?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] : xs.max? = none ↔ xs = []

Equations

• @List.maximum?_eq_none_iff = @List.max?_eq_none_iff

@[reducible, inline, deprecated List.max?_mem (since := "2024-09-29")]

abbrev List.maximum?_mem {α : Type u_1} {a : α} [Max α] (min_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) {xs : List α} : xs.max? = some a → a ∈ xs

Equations

• @List.maximum?_mem = @List.max?_mem

@[reducible, inline, deprecated List.max?_le_iff (since := "2024-09-29")]

abbrev List.maximum?_le_iff {α : Type u_1} {a : α} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} : xs.max? = some a → ∀ {x : α}, a ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x

Equations

• @List.maximum?_le_iff = @List.max?_le_iff

@[reducible, inline, deprecated List.max?_eq_some_iff (since := "2024-09-29")]

abbrev List.maximum?_eq_some_iff {α : 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

Equations

• @List.maximum?_eq_some_iff = @List.max?_eq_some_iff

@[reducible, inline, deprecated List.max?_replicate (since := "2024-09-29")]

abbrev List.maximum?_replicate {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) : (replicate n a).max? = if n = 0 then none else some a

Equations

• @List.maximum?_replicate = @List.max?_replicate

@[reducible, inline, deprecated List.max?_replicate_of_pos (since := "2024-09-29")]

abbrev List.maximum?_replicate_of_pos {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) : (replicate n a).max? = some a

Equations

• @List.maximum?_replicate_of_pos = @List.max?_replicate_of_pos