support_add — Mathlib

English

The support of a + b is contained in the union of the supports of a and b.

Русский

Опора суммы a + b содержится в объединении опор a и b.

LaTeX

$$$\\operatorname{support}(a+b) \\subseteq \\operatorname{support}(a) \\cup \\operatorname{support}(b)$$$

Lean4

theorem support_add (a b : FreeAbelianGroup X) : support (a + b) ⊆ a.support ∪ b.support :=
  by
  simp only [support, AddMonoidHom.map_add]
  apply Finsupp.support_add

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