mulSupport_update_of_ne_one — Mathlib

English

For any f : ι → M and x ∈ ι and y ≠ 1, mulSupport (update f x y) = insert x (mulSupport f).

Русский

При обновлении функции f в точке x значением y ≠ 1, mulSupport увеличивается на x: mulSupport(update f x y) = insert x mulSupport(f).

LaTeX

$$$ \\mathrm{mulSupport}(\\mathrm{update}\\ f\\ x\\ y) = \\mathrm{insert}\\ x \\big( \\mathrm{mulSupport}(f) \\big) $$$

Lean4

@[to_additive]
theorem mulSupport_update_of_ne_one [DecidableEq ι] (f : ι → M) (x : ι) {y : M} (hy : y ≠ 1) :
    mulSupport (update f x y) = insert x (mulSupport f) := by ext a; obtain rfl | hne := eq_or_ne a x <;> simp [*]

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