toMultiset_apply

Mathlib.Data.Finsupp.Multiset

URI: https://scilib.ai/kg/mathlib#Finsupp.toMultiset_apply

English

The value of toMultiset on a finitely supported function f equals the sum over α of n • singleton(a).

Русский

Значение toMultiset на функции f с конечной опорой равно сумме по α из n • {a}.

LaTeX

$$$$ toMultiset(f) = f.sum\\, (\\lambda a\\, n.\\ n \\cdot \\{a\\}). $$$$

Lean4

theorem toMultiset_apply (f : α →₀ ℕ) : toMultiset f = f.sum fun a n => n • { a } :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru