English
Let op be an idempotent commutative associative operation on α, and s a multiset of α. Then deduplicating s does not change the fold with initial b:\n(dedup s).fold op b = s.fold op b.
Русский
Пусть op идемпотентна и коммутативна. Для мультисета s выполнено, что свёртка после удаления дубликатов совпадает со свёрткой исходного множества: (dedup s).fold op b = s.fold op b.
LaTeX
$$$\\operatorname{fold}_{op}(b, \\operatorname{dedup}(s)) = \\operatorname{fold}_{op}(b, s)$$$
Lean4
@[simp]
theorem fold_dedup_idem [DecidableEq α] [hi : Std.IdempotentOp op] (s : Multiset α) (b : α) :
(dedup s).fold op b = s.fold op b :=
Multiset.induction_on s (by simp) fun a s IH => by
by_cases h : a ∈ s; swap; · simp [IH, h]
simp only [h, dedup_cons_of_mem, IH, fold_cons_left]
show fold op b s = op a (fold op b s)
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]
