foldl_strictMono — Mathlib

English

If every b ↦ f a b is strictly monotone in a for each a, then the left fold is strictly monotone in its initial value.

Русский

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

LaTeX

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

Lean4

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

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