support_add — Mathlib

English

The support of a finite sum is contained in the union of the supports of the summands.

Русский

Опора суммы конечного числа полиномов содержится в объединении опор сомножителей.

LaTeX

$$$\\\\forall f: α \\\\to MvPolynomial\\\\sigma\\\\,R, \\\\operatorname{support}(\\\\sum x, f x) \\\\subseteq \\\\bigcup_x \\, \\operatorname{support}(f x)$$$

Lean4

theorem support_add [DecidableEq σ] : (p + q).support ⊆ p.support ∪ q.support :=
  Finsupp.support_add

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