update_eq_single_add

Mathlib.Algebra.Group.Finsupp

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

← MathLib Explorer

English

If f(a) = 0, then updating f at a by b yields f.update a b = f + single a b.

Русский

Если f(a) = 0, то обновление f в позиции a на b даёт f.update a b = f + single a b.

LaTeX

$$$f(a) = 0 \\Rightarrow f.update a b = f + single a b$$$

Lean4

theorem update_eq_single_add {f : ι →₀ M} {a : ι} (h : f a = 0) (b : M) : f.update a b = single a b + f := by
  rw [update_eq_single_add_erase, erase_of_notMem_support (by simpa)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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