Minima and maxima

min

def Array.min {α : Type u_1} [Min α] (arr : Array α) (h : arr ≠ #[]) : α

Returns the smallest element of a non-empty array.

Examples:

• #[4].min (by decide) = 4
• #[1, 4, 2, 10, 6].min (by decide) = 1

Equations

• arr.min h = Array.foldl min arr[0] arr 1

min?

def Array.min? {α : Type u_1} [Min α] (arr : Array α) : Option α

Returns the smallest element of the array if it is not empty, or none if it is empty.

Examples:

• #[].min? = none
• #[4].min? = some 4
• #[1, 4, 2, 10, 6].min? = some 1

Equations

• arr.min? = if h : arr ≠ #[] then some (arr.min h) else none

max

def Array.max {α : Type u_1} [Max α] (arr : Array α) (h : arr ≠ #[]) : α

Returns the largest element of a non-empty array.

Examples:

• #[4].max (by decide) = 4
• #[1, 4, 2, 10, 6].max (by decide) = 10

Equations

• arr.max h = Array.foldl max arr[0] arr 1

max?

def Array.max? {α : Type u_1} [Max α] (arr : Array α) : Option α

Returns the largest element of the array if it is not empty, or none if it is empty.

Examples:

• #[].max? = none
• #[4].max? = some 4
• #[1, 4, 2, 10, 6].max? = some 10

Equations

• arr.max? = if h : arr ≠ #[] then some (arr.max h) else none

Compatibility with List

@[simp]

theorem List.min_toArray {α : Type u_1} [Min α] {l : List α} {h : l.toArray ≠ #[]} : l.toArray.min h = l.min ⋯

theorem List.min_eq_min_toArray {α : Type u_1} [Min α] {l : List α} {h : l ≠ []} : l.min h = l.toArray.min ⋯

@[simp]

theorem Array.min_toList {α : Type u_1} [Min α] {xs : Array α} {h : xs.toList ≠ []} : xs.toList.min h = xs.min ⋯

theorem Array.min_eq_min_toList {α : Type u_1} [Min α] {xs : Array α} {h : xs ≠ #[]} : xs.min h = xs.toList.min ⋯

@[simp]

theorem List.min?_toArray {α : Type u_1} [Min α] {l : List α} : l.toArray.min? = l.min?

@[simp]

theorem Array.min?_toList {α : Type u_1} [Min α] {xs : Array α} : xs.toList.min? = xs.min?

@[simp]

theorem List.max_toArray {α : Type u_1} [Max α] {l : List α} {h : l.toArray ≠ #[]} : l.toArray.max h = l.max ⋯

theorem List.max_eq_max_toArray {α : Type u_1} [Max α] {l : List α} {h : l ≠ []} : l.max h = l.toArray.max ⋯

@[simp]

theorem Array.max_toList {α : Type u_1} [Max α] {xs : Array α} {h : xs.toList ≠ []} : xs.toList.max h = xs.max ⋯

theorem Array.max_eq_max_toList {α : Type u_1} [Max α] {xs : Array α} {h : xs ≠ #[]} : xs.max h = xs.toList.max ⋯

@[simp]

theorem List.max?_toArray {α : Type u_1} [Max α] {l : List α} : l.toArray.max? = l.max?

@[simp]

theorem Array.max?_toList {α : Type u_1} [Max α] {xs : Array α} : xs.toList.max? = xs.max?

Lemmas about min?

@[simp]

theorem Array.min?_empty {α : Type u_1} [Min α] : #[].min? = none

@[simp]

theorem Array.min?_singleton {α : Type u_1} [Min α] {x : α} : #[x].min? = some x

theorem Array.min?_singleton_append' {α : Type u_1} {x : α} [Min α] {xs : Array α} : (#[x] ++ xs).min? = some (foldl min x xs)

@[simp]

theorem Array.min?_singleton_append {α : Type u_1} {x : α} [Min α] [Std.Associative min] {xs : Array α} : (#[x] ++ xs).min? = some (xs.min?.elim x (min x))

@[simp]

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

@[simp]

theorem Array.isSome_min?_iff {α : Type u_1} {xs : Array α} [Min α] : xs.min?.isSome = true ↔ xs ≠ #[]

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

theorem Array.isSome_min?_of_ne_empty {α : Type u_1} [Min α] (xs : Array α) (h : xs ≠ #[]) : xs.min?.isSome = true

theorem Array.min?_mem {α : Type u_1} {a : α} [Min α] [Std.MinEqOr α] (xs : Array α) (h : xs.min? = some a) : a ∈ xs

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

theorem Array.min?_eq_some_iff {α : Type u_1} {a : α} [Min α] [LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α] : xs.min? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

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

@[simp]

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

theorem Array.foldl_min {α : Type u_1} [Min α] [Std.IdempotentOp min] [Std.Associative min] {xs : Array α} {a : α} : foldl min a xs = min a (xs.min?.getD a)

Lemmas about max?

@[simp]

theorem Array.max?_empty {α : Type u_1} [Max α] : #[].max? = none

@[simp]

theorem Array.max?_singleton {α : Type u_1} [Max α] {x : α} : #[x].max? = some x

theorem Array.max?_singleton_append' {α : Type u_1} {x : α} [Max α] {xs : Array α} : (#[x] ++ xs).max? = some (foldl max x xs)

@[simp]

theorem Array.max?_singleton_append {α : Type u_1} {x : α} [Max α] [Std.Associative max] {xs : Array α} : (#[x] ++ xs).max? = some (xs.max?.elim x (max x))

@[simp]

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

@[simp]

theorem Array.isSome_max?_iff {α : Type u_1} {xs : Array α} [Max α] : xs.max?.isSome = true ↔ xs ≠ #[]

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

theorem Array.isSome_max?_of_ne_empty {α : Type u_1} [Max α] (xs : Array α) (h : xs ≠ #[]) : xs.max?.isSome = true

theorem Array.max?_mem {α : Type u_1} {a : α} [Max α] [Std.MaxEqOr α] (xs : Array α) (h : xs.max? = some a) : a ∈ xs

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

theorem Array.max?_eq_some_iff {α : Type u_1} {a : α} [Max α] [LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α] : xs.max? = some a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a

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

@[simp]

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

theorem Array.foldl_max {α : Type u_1} [Max α] [Std.IdempotentOp max] [Std.Associative max] {xs : Array α} {a : α} : foldl max a xs = max a (xs.max?.getD a)

Lemmas about min

theorem Array.min?_eq_some_min {α : Type u_1} [Min α] {xs : Array α} (h : xs ≠ #[]) : xs.min? = some (xs.min h)

theorem Array.min_eq_get_min? {α : Type u_1} [Min α] (xs : Array α) (h : xs ≠ #[]) : xs.min h = xs.min?.get ⋯

@[simp]

theorem Array.get_min? {α : Type u_1} [Min α] {xs : Array α} {h : xs.min?.isSome = true} : xs.min?.get h = xs.min ⋯

theorem Array.min_mem {α : Type u_1} [Min α] [Std.MinEqOr α] {xs : Array α} (h : xs ≠ #[]) : xs.min h ∈ xs

theorem Array.min_le_of_mem {α : Type u_1} [Min α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α] {xs : Array α} {a : α} (ha : a ∈ xs) : xs.min ⋯ ≤ a

theorem Array.le_min_iff {α : Type u_1} [Min α] [LE α] [Std.LawfulOrderInf α] {xs : Array α} (h : xs ≠ #[]) {x : α} : x ≤ xs.min h ↔ ∀ (b : α), b ∈ xs → x ≤ b

theorem Array.min_eq_iff {α : Type u_1} {a : α} [Min α] [LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α] (h : xs ≠ #[]) : xs.min h = a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → a ≤ b

@[simp]

theorem Array.min_replicate {α : Type u_1} [Min α] [Std.MinEqOr α] {n : Nat} {a : α} (h : replicate n a ≠ #[]) : (replicate n a).min h = a

theorem Array.foldl_min_eq_min {α : Type u_1} [Min α] [Std.IdempotentOp min] [Std.Associative min] {xs : Array α} (h : xs ≠ #[]) {a : α} : foldl min a xs = min a (xs.min h)

Lemmas about max

theorem Array.max?_eq_some_max {α : Type u_1} [Max α] {xs : Array α} (h : xs ≠ #[]) : xs.max? = some (xs.max h)

theorem Array.max_eq_get_max? {α : Type u_1} [Max α] (xs : Array α) (h : xs ≠ #[]) : xs.max h = xs.max?.get ⋯

@[simp]

theorem Array.get_max? {α : Type u_1} [Max α] {xs : Array α} {h : xs.max?.isSome = true} : xs.max?.get h = xs.max ⋯

theorem Array.max_mem {α : Type u_1} [Max α] [Std.MaxEqOr α] {xs : Array α} (h : xs ≠ #[]) : xs.max h ∈ xs

theorem Array.max_le_iff {α : Type u_1} [Max α] [LE α] [Std.LawfulOrderSup α] {xs : Array α} (h : xs ≠ #[]) {x : α} : xs.max h ≤ x ↔ ∀ (b : α), b ∈ xs → b ≤ x

theorem Array.max_eq_iff {α : Type u_1} {a : α} [Max α] [LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α] (h : xs ≠ #[]) : xs.max h = a ↔ a ∈ xs ∧ ∀ (b : α), b ∈ xs → b ≤ a

theorem Array.le_max_of_mem {α : Type u_1} [Max α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α] {xs : Array α} {a : α} (ha : a ∈ xs) : a ≤ xs.max ⋯

@[simp]

theorem Array.max_replicate {α : Type u_1} [Max α] [Std.MaxEqOr α] {n : Nat} {a : α} (h : replicate n a ≠ #[]) : (replicate n a).max h = a

theorem Array.foldl_max_eq_max {α : Type u_1} [Max α] [Std.IdempotentOp max] [Std.Associative max] {xs : Array α} (h : xs ≠ #[]) {a : α} : foldl max a xs = max a (xs.max h)