English
For a nonempty list l over a linear order with bottom element, the folded maximum equals the list maximum: foldr max ⊥ l = maximum(l).
Русский
Для непустого списка l над линейным порядком с нижним элементом, свертка max с⊥ даёт максимум списка: foldr max ⊥ l = maximum(l).
LaTeX
$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)] [\\mathrm{OrderBot}(\\alpha)], \\forall l : \\List(\\alpha), l \\neq \\emptyset \\Rightarrow \\mathrm{foldr}(\\max) \\bot \\ l = l.maximum$$$
Lean4
@[simp]
theorem foldr_max_of_ne_nil (h : l ≠ []) : ↑(l.foldr max ⊥) = l.maximum := by
induction l with
| nil => contradiction
| cons hd tl IH =>
rw [maximum_cons, foldr, WithBot.coe_max]
by_cases h : tl = []
· simp [h]
· simp [IH h]
