toFinsupp_support

Mathlib.Data.Finsupp.ToDFinsupp

URI: https://scilib.ai/kg/mathlib#DFinsupp.toFinsupp_support

English

In the DFinsupp setting, toFinsupp preserves addition: toFinsupp (f + g) = toFinsupp f + toFinsupp g.

Русский

Для DFinsupp отображение toFinsupp сохраняет сложение: toFinsupp (f + g) = toFinsupp f + toFinsupp g.

LaTeX

$$(toFinsupp (f + g) : ι →₀ M) = toFinsupp f + toFinsupp g$$

Lean4

@[simp]
theorem toFinsupp_support (f : Π₀ _ : ι, M) : f.toFinsupp.support = f.support :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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