English
An induction principle for foldr over multisets: given a predicate q on α, a predicate p on β, and a function f with left-commutativity, from base case p x and inductive step, one can conclude p (foldr f x s).
Русский
Принцип индукции по foldr над мультимножество: имея предикат q на α, предикат p на β и функцию f со свойством левостороннего коммутирования, из базового случая p x и индуктивного шага можно заключить p (foldr f x s).
LaTeX
$$$$ \\text{foldr_induction'}\\,(f, x, q, p, s, hpqf, px, q_s) : p(\\operatorname{foldr} f x s) $$$$
Lean4
theorem foldr_swap (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) :
foldr f b s = foldl (fun x y => f y x) b s :=
Quot.inductionOn s fun _l => coe_foldr_swap _ _ _
