coe_foldr_swap — Mathlib

English

The foldr over a multiset represented by a list l equals the left-fold of f with arguments reversed over l.

Русский

Сворачивание foldr над мультимножество, представленном списком l, эквивалентно левому сворачиванию с обращённой последовательностью аргументов.

LaTeX

$$$$ \\operatorname{foldr} f b (\\operatorname{Multiset}.ofList l) = \\operatorname{List}.foldl (\\lambda x y. f y x) b l $$$$

Lean4

theorem coe_foldr_swap (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) :
    foldr f b l = l.foldl (fun x y => f y x) b :=
  (congr_arg (foldr f b) (coe_reverse l)).symm.trans foldr_reverse

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