foldr_monotone — Mathlib

English

If for each a, the function b ↦ f(a,b) is monotone, then the right fold over a list is monotone in its result.

Русский

Если для каждого a функция b ↦ f(a,b) монотонна, то сложение справа по списку монотонно.

LaTeX

$$$[Preorder \\beta]\\\\ {f : \\alpha \\to \\beta \\to \\beta}\\\\ (H : \\forall a, Monotone (f a))\\\\ (l : List \\alpha) \\,\\to\\, Monotone (\\lambda b, List.foldr f b l)$$$

Lean4

theorem foldr_monotone [Preorder β] {f : α → β → β} (H : ∀ a, Monotone (f a)) (l : List α) :
    Monotone fun b ↦ l.foldr f b := fun _ _ h ↦ List.recOn l h fun i _ hl ↦ H i hl

Похожие утверждения