if_mem_support — Mathlib

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

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