erase_of_notMem_support

Mathlib.Data.Finsupp.Single

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

← MathLib Explorer

English

If a is not in the support of f, then erase a f = f.

Русский

Если a не принадлежит опоре функции f, то erase a f = f.

LaTeX

$$erase a f = f \quad\text{if } a \notin f.support$$

Lean4

@[simp]
theorem erase_of_notMem_support {f : α →₀ M} {a} (haf : a ∉ f.support) : erase a f = f :=
  by
  ext b; by_cases hab : b = a
  · rwa [hab, erase_same, eq_comm, ← notMem_support_iff]
  · rw [erase_ne hab]

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

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

Разделы

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

Аффилиация

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