mulSupport_update_eq_ite — Mathlib

English

mulSupport (update f x y) equals if y = 1 then mulSupport f \\ { x } else insert x (mulSupport f).

Русский

mulSupport(update f x y) равно if y = 1 то mulSupport f без {x} иначе {x} добавляем mulSupport f.

LaTeX

$$$ \\mathrm{mulSupport}(\\mathrm{update}\\ f\\ x\\ y) = \\mathrm{ite}(y=1, \\mathrm{mulSupport}(f) \\setminus \\{ x \\}, \\mathrm{insert}\\ x (\\mathrm{mulSupport}(f))) $$$

Lean4

@[to_additive]
theorem mulSupport_update_eq_ite [DecidableEq ι] [DecidableEq M] (f : ι → M) (x : ι) (y : M) :
    mulSupport (update f x y) = if y = 1 then mulSupport f \ { x } else insert x (mulSupport f) := by
  rcases eq_or_ne y 1 with rfl | hy <;> simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

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