erase_idem

Mathlib.Data.Finsupp.Single

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

English

Erasing the same coordinate twice is the same as erasing it once: erase a (erase a f) = erase a f.

Русский

Стирание одной и той же координаты дважды равно стиранию один раз: erase a (erase a f) = erase a f.

LaTeX

$$erase a (erase a f) = erase a f$$

Lean4

theorem erase_idem (f : α →₀ M) (a : α) : erase a (erase a f) = erase a f := by
  rw [erase_eq_update_zero, erase_eq_update_zero, update_idem]

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

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

Разделы

Аффилиация

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