single_add_erase — Mathlib

English

For any i, f, we have single i (f i) + f.erase i = f.

Русский

Для любого i, f выполняется single i (f i) + f.erase i = f.

LaTeX

$$$ \\mathrm{single}_i (f i) + f.erase i = f $$$

Lean4

theorem single_add_erase (i : ι) (f : Π₀ i, β i) : single i (f i) + f.erase i = f :=
  ext fun i' =>
    if h : i = i' then by subst h; simp only [add_apply, single_apply, erase_apply, add_zero, dite_eq_ite, if_true]
    else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), zero_add]

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