support_erase — Mathlib

English

Let f be a finitely supported function f: α →₀ M. Then the support of the erased function at a equals the original support with a removed: (f.erase a).support = f.support.erase a.

Русский

Пусть f: α →₀ M имеет конечную опору. Тогда опора стирания в точке a равна опоре исходной функции без элемента a: (f.erase a).support = f.support.erase a.

LaTeX

$$$ (f.erase a).\operatorname{support} = f.\operatorname{support}.erase a $$$

Lean4

@[simp]
theorem support_erase [DecidableEq α] {a : α} {f : α →₀ M} : (f.erase a).support = f.support.erase a := by
  classical
  dsimp only [erase]
  congr!

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