erase_add — Mathlib

English

For any a, the operation erase distributes over addition: erase a (f + f') = erase a f + erase a f'.

Русский

Для любого a операция стирания распределяется по сложению: erase a (f + f') = erase a f + erase a f'.

LaTeX

$$$\\erase a (f + f') = \\erase a f + \\erase a f'$$$

Lean4

@[simp]
theorem erase_add (a : ι) (f f' : ι →₀ M) : erase a (f + f') = erase a f + erase a f' :=
  by
  ext s; by_cases hs : s = a
  · rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
  rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]

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