toFinsupp_add

Mathlib.Data.Finsupp.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.toFinsupp_add

English

The map toFinsupp respects addition: toFinsupp(s + t) = toFinsupp(s) + toFinsupp(t).

Русский

Преобразование toFinsupp сохраняет сложение: toFinsupp(s + t) = toFinsupp(s) + toFinsupp(t).

LaTeX

$$$\mathrm{toFinsupp}(s + t) = \mathrm{toFinsupp}(s) + \mathrm{toFinsupp}(t)$$$

Lean4

theorem toFinsupp_add (s t : Multiset α) : toFinsupp (s + t) = toFinsupp s + toFinsupp t :=
  _root_.map_add toFinsupp s t

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

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

Разделы

Аффилиация

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