sum_multiset_singleton — Mathlib

English

The sum over a Finset of singleton multisets equals the Finset's underlying multiset: ∑ a ∈ s, {a} = s.val.

Русский

Сумма по Финсету мультисетов-одиночек равна базовому мультисету Финсета: ∑ a ∈ s, {a} = s.val.

LaTeX

$$$$ \\sum_{a \\in s} \\{a\\} = s.{\\text{val}} $$$$

Lean4

@[simp]
theorem sum_multiset_singleton (s : Finset ι) : ∑ a ∈ s, { a } = s.val := by
  simp only [sum_eq_multiset_sum, Multiset.sum_map_singleton]

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