support_sum — Mathlib

English

The support of a sum over a family is contained in the union of the supports of each summand.

Русский

Опора суммы по семье находится в объединении опор слагаемых.

LaTeX

$$$(f.sum\\ g).\\operatorname{support} \\subseteq f.\\operatorname{support} \\biUnion \\bigl( (g\\ a (f.coeff a)).\\operatorname{support} \\bigr)$$$

Lean4

theorem support_sum {k' G' : Type*} [DecidableEq G'] [AddCommMonoid k'] {f : SkewMonoidAlgebra k G}
    {g : G → k → SkewMonoidAlgebra k' G'} : (f.sum g).support ⊆ f.support.biUnion fun a ↦ (g a (f.coeff a)).support :=
  by
  simp_rw [support, toFinsupp_sum']
  apply Finsupp.support_sum

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