count_sum — Mathlib

English

Count distributes over map and sum: count a (map f m).sum = sum (m.map (count a ∘ f)).

Русский

Подсчёт распределяется по отображению и сумме: count a (map f m).sum = sum (m.map (count a ∘ f)).

LaTeX

$$$\\mathrm{count}\\ a\\ (\\mathrm{map}\\ f\\ m).\\mathrm{sum} = \\mathrm{sum}(\\mathrm{map}\\ (\\mathrm{count}\\ a \\circ f)\\ m)$$$

Lean4

theorem count_sum [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} :
    count a (map f m).sum = sum (m.map fun b => count a <| f b) :=
  Multiset.induction_on m (by simp) (by simp)

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