foldl_monotone — Mathlib

English

If every f a b is monotone in a for fixed b, then the left fold of f over a list is monotone in its initial value.

Русский

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

LaTeX

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

Lean4

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

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