erase_single_ne

Mathlib.Data.Finsupp.Single

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

← MathLib Explorer

English

If a ≠ a', then erase a (single a' b) = single a' b.

Русский

Если a ≠ a', то erase a (single a' b) = single a' b.

LaTeX

$$a \neq a' \Rightarrow erase a (single a' b) = single a' b$$

Lean4

theorem erase_single_ne {a a' : α} {b : M} (h : a ≠ a') : erase a (single a' b) = single a' b :=
  by
  ext s; by_cases hs : s = a
  · rw [hs, erase_same, single_eq_of_ne h]
  · rw [erase_ne hs]

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

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

Разделы

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

Аффилиация

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