count_sum' — Mathlib

English

For a finite set s ⊆ ι and a function f: ι → Multiset α, the count of a in the sum ∑_{x∈s} f(x) equals the sum of counts: count_a(∑_{x∈s} f(x)) = ∑_{x∈s} count_a(f(x)).

Русский

Для конечного множества s ⊆ ι и функции f: ι → Multiset α число вхождений a в суммы ∑_{x∈s} f(x) равно сумме чисел вхождений a в каждом f(x).

LaTeX

$$$\operatorname{count}_a\left(\sum_{x \in s} f(x)\right) = \sum_{x \in s} \operatorname{count}_a\left(f(x)\right)$$$

Lean4

theorem count_sum' {s : Finset ι} {a : α} {f : ι → Multiset α} : count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x) :=
  by
  dsimp only [Finset.sum]
  rw [count_sum]

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