foldl_concat — Mathlib

English

For any f: β → α → β, b ∈ β, x ∈ α, xs : List α, foldl f b (xs ++ [x]) = f (foldl f b xs) x.

Русский

Для любого f: β → α → β, b, x, xs, выполняется foldl f b (xs ++ [x]) = f (foldl f b xs) x.

LaTeX

$$$\\\\forall {f:\\\\beta \\\\to \\\\alpha \\\\to \\\\beta} {b:\\\\beta} {x:\\\\alpha} {xs:\\\\text{List }\\\\alpha}, \\\\operatorname{foldl} f b (xs ++ [x]) = f (\\\\operatorname{foldl} f b xs) x.$$$

Lean4

theorem foldl_concat (f : β → α → β) (b : β) (x : α) (xs : List α) :
    List.foldl f b (xs ++ [x]) = f (List.foldl f b xs) x := by simp only [List.foldl_append, List.foldl]

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