foldl_swap — Mathlib

English

For a function f with RightCommutative property, foldl f b s equals foldr (λ x y, f y x) b s.

Русский

Секцию foldl с правым коммутированием можно заменить на foldr с обращенным аргументом: foldl f b s = foldr (λ x y, f y x) b s.

LaTeX

$$$$ \\operatorname{foldl} f b s = \\operatorname{foldr} (\\lambda x y. f y x) b s $$$$

Lean4

theorem foldl_swap (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) :
    foldl f b s = foldr (fun x y => f y x) b s :=
  (foldr_swap _ _ _).symm

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