English
Let P be a property of functions f ∈ Π₀ i, β i. If P holds for 0 and whenever f i = 0 and b ≠ 0 and P f holds, then P (single i b + f). Then P holds for all f.
Русский
Пусть P — свойство функции f ∈ Π₀ i, β i. Если P выполняется для нуля, и если из f, удовлетворяющего f i = 0 и b ≠ 0, следует P (single i b + f), то P верно для всех f.
LaTeX
$$$ P(0) \\land \\forall i\\forall b\\forall f\\ (f(i) = 0 \\land b \\neq 0 \\land P(f) \\rightarrow P(\\\\mathrm{single} i b + f)) \\Rightarrow \\forall f\\, P(f) $$$
Lean4
theorem erase_add_single (i : ι) (f : Π₀ i, β i) : f.erase i + single i (f i) = f :=
ext fun i' =>
if h : i = i' then by subst h; simp only [add_apply, single_apply, erase_apply, zero_add, dite_eq_ite, if_true]
else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), add_zero]
