Minima and maxima #
min? #
theorem
List.min?_eq_some_iff
{α : Type u_1}
{a : α}
[Min α]
[LE α]
(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 α}
(anti : ∀ (a b : α), a ∈ xs → b ∈ xs → a ≤ b → b ≤ a → a = b := by exact fun a b _ _ => Std.Antisymm.antisymm a b)
:
theorem
List.foldl_min
{α : Type u_1}
[Min α]
[Std.IdempotentOp min]
[Std.Associative min]
{l : List α}
{a : α}
:
max? #
theorem
List.foldl_max
{α : Type u_1}
[Max α]
[Std.IdempotentOp max]
[Std.Associative max]
{l : List α}
{a : α}
: