erase_add — Mathlib

English

The erase operation distributes over addition: erase i (f1 + f2) = erase i f1 + erase i f2.

Русский

Операция стирания распределяется по сложению: erase i (f1 + f2) = erase i f1 + erase i f2.

LaTeX

$$$ \\mathrm{erase} i (f_1 + f_2) = \\mathrm{erase} i f_1 + \\mathrm{erase} i f_2 $$$

Lean4

@[simp]
theorem erase_add (i : ι) (f₁ f₂ : Π₀ i, β i) : erase i (f₁ + f₂) = erase i f₁ + erase i f₂ :=
  ext fun _ => by simp [ite_zero_add]

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