sum_map_singleton — Mathlib

English

Summing the singletons {a} corresponding to each element a of a multiset s yields s itself: the sum of the image of s under a singleton map recovers s.

Русский

Сумма элементов отображения в синглтона {a} по каждому a из multiset s восстанавливает сам s.

LaTeX

$$$\\big( s.map( (\\{ a \\}: Multiset M) ).sum \\big) = s$$$

Lean4

@[simp]
theorem sum_map_singleton (s : Multiset M) : (s.map fun a => ({ a } : Multiset M)).sum = s :=
  Multiset.induction_on s (by simp) (by simp)

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