English
For any finitely supported f: α → M and a ∈ α, the expression (if a ∈ support(f) then f(a) else 0) equals f(a).
Русский
Для любой f: α →₀ M и a ∈ α, выражение (если a принадлежит поддержке f, то f(a), иначе 0) равно f(a).
LaTeX
$$$$ \\big(\\text{if } a \\in \\mathrm{supp}(f) \\text{ then } f(a) \\text{ else } 0\\big) = f(a) $$$$
Lean4
/-- The left-hand side of `sum_ite_self_eq` simplifies; this is the variant that is useful for `simp`.
-/
@[simp]
theorem if_mem_support [DecidableEq α] {N : Type*} [Zero N] (f : α →₀ N) (a : α) :
(if a ∈ f.support then f a else 0) = f a :=
by
simp only [mem_support_iff, ne_eq, ite_eq_left_iff, not_not]
exact fun h ↦ h.symm