support_erase

Mathlib.Data.DFinsupp.Defs

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

English

Erasing the i-th coordinate reduces the support by erasing i from it.

Русский

Удаление i-й координаты уменьшает опору, удаляя i из неё.

LaTeX

$$$(\\mathrm{erase}\\,i\\;f).\\mathrm{support} = f.{\\mathrm{support}}.\\mathrm{erase}\\ i$$$

Lean4

@[simp]
theorem support_erase (i : ι) (f : Π₀ i, β i) : (f.erase i).support = f.support.erase i :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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