sum_count_eq_card — Mathlib

English

Let s be a Finset and m a Multiset. If every element of m lies in s, then the sum over a ∈ s of count(a, m) equals card(m).

Русский

Пусть s — конечное множество и m — мультсет. Если каждый элемент m принадлежит s, то сумма по a ∈ s от count(a, m) равна card(m).

LaTeX

$$$$ \\text{If } \\forall a, a \\in m \\Rightarrow a \\in s, \\quad \\sum_{a \\in s} \\mathrm{count}(a,m) = \\mathrm{card}(m). $$$$

Lean4

@[simp]
theorem sum_count_eq_card {s : Finset ι} {m : Multiset ι} (hms : ∀ a ∈ m, a ∈ s) : ∑ a ∈ s, m.count a = card m :=
  by
  rw [← toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]
  congr with a
  simpa using hms a

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