Documentation

Init.Data.List.MinMax

Lemmas about List.minimum? and `List.maximum?. #

Minima and maxima #

minimum? #

@[simp]
theorem List.minimum?_nil {α : Type u_1} [Min α] :
[].minimum? = none
theorem List.minimum?_cons {α : Type u_1} {x : α} [Min α] {xs : List α} :
(x :: xs).minimum? = some (List.foldl min x xs)
@[simp]
theorem List.minimum?_eq_none_iff {α : Type u_1} {xs : List α} [Min α] :
xs.minimum? = none xs = []
theorem List.minimum?_mem {α : Type u_1} {a : α} [Min α] (min_eq_or : ∀ (a b : α), min a b = a min a b = b) {xs : List α} :
xs.minimum? = some aa xs
theorem 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.minimum? = some a∀ (x : α), x a ∀ (b : α), b xsx b
theorem List.minimum?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] [anti : Antisymm fun (x x_1 : α) => x x_1] (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.minimum? = some a a xs ∀ (b : α), b xsa b
theorem List.minimum?_replicate {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) :
(List.replicate n a).minimum? = if n = 0 then none else some a
@[simp]
theorem List.minimum?_replicate_of_pos {α : Type u_1} [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
(List.replicate n a).minimum? = some a

maximum? #

@[simp]
theorem List.maximum?_nil {α : Type u_1} [Max α] :
[].maximum? = none
theorem List.maximum?_cons {α : Type u_1} {x : α} [Max α] {xs : List α} :
(x :: xs).maximum? = some (List.foldl max x xs)
@[simp]
theorem List.maximum?_eq_none_iff {α : Type u_1} {xs : List α} [Max α] :
xs.maximum? = none xs = []
theorem List.maximum?_mem {α : Type u_1} {a : α} [Max α] (min_eq_or : ∀ (a b : α), max a b = a max a b = b) {xs : List α} :
xs.maximum? = some aa xs
theorem 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.maximum? = some a∀ (x : α), a x ∀ (b : α), b xsb x
theorem List.maximum?_eq_some_iff {α : Type u_1} {a : α} [Max α] [LE α] [anti : Antisymm fun (x x_1 : α) => x x_1] (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.maximum? = some a a xs ∀ (b : α), b xsb a
theorem List.maximum?_replicate {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) :
(List.replicate n a).maximum? = if n = 0 then none else some a
@[simp]
theorem List.maximum?_replicate_of_pos {α : Type u_1} [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
(List.replicate n a).maximum? = some a