erase_ne

Mathlib.Data.Finsupp.Single

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

English

If a' ≠ a, then (f.erase a) a' = f a'.

Русский

Если a' не равно a, то (f.erase a) a' = f a'.

LaTeX

$$$a' \neq a \Rightarrow (f.erase a) a' = f a'$$$

Lean4

@[simp]
theorem erase_ne {a a' : α} {f : α →₀ M} (h : a' ≠ a) : (f.erase a) a' = f a' := by
  classical simp only [erase, coe_mk, h, ite_false]

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

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

Разделы

Аффилиация

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