support_add — Mathlib

English

Let g1, g2 be dfinsupps indexed by ι with values in β i. Then the support of g1 + g2 is contained in the union of the supports of g1 and g2.

Русский

Пусть g1, g2 — dfinsupp-объекты над β i. Тогда supp(g1+g2) ⊆ supp(g1) ∪ supp(g2).

LaTeX

$$$\\mathrm{supp}(g_1+g_2) \\subseteq \\mathrm{supp}(g_1) \\cup \\mathrm{supp}(g_2)$$$

Lean4

theorem support_add [∀ i, AddZeroClass (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {g₁ g₂ : Π₀ i, β i} :
    (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
  support_zipWith

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