update_eq_sub_add_single — Mathlib

English

For a family of additive groups, updating i to b can be expressed as f.update i b = f − single i (f i) + single i b.

Русский

Для семейства групп с сложением обновление i до b равно f − single i (f i) + single i b.

LaTeX

$$$ f.update i b = f - single i (f i) + single i b $$$

Lean4

theorem update_eq_sub_add_single {β : ι → Type*} [∀ i, AddGroup (β i)] (f : Π₀ i, β i) (i : ι) (b : β i) :
    f.update i b = f - single i (f i) + single i b := by rw [update_eq_erase_add_single f i b, erase_eq_sub_single f i]

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