English
Let f: α → β → β, b ∈ β, x ∈ α, xs ∈ List α. Then folding f over the list xs concatenated with [x] yields the same as folding f over xs with the updated base (f x b): foldr f b (xs ++ [x]) = foldr f (f x b) xs.
Русский
Пусть f: α → β → β, b ∈ β, x ∈ α, xs — список α. Тогда свёртка f по списку xs, дополненному элементом x справа, равна свёртке по xs с обновлённой базой f x b: foldr f b (xs ++ [x]) = foldr f (f x b) xs.
LaTeX
$$$$\operatorname{foldr} f\, b\, (xs \\ text{++} [x]) = \operatorname{foldr} f\, (f\, x\, b)\, xs.$$$$
Lean4
theorem foldr_concat (f : α → β → β) (b : β) (x : α) (xs : List α) :
List.foldr f b (xs ++ [x]) = (List.foldr f (f x b) xs) := by simp only [List.foldr_append, List.foldr]
