support_add — Mathlib

English

The support of the sum of two finitely supported functions is contained in the union of their supports: supp(g1 + g2) ⊆ supp(g1) ∪ supp(g2).

Русский

Поддержка суммы двух функций с конечной поддержкой содержится в объединении их поддержек: supp(g1 + g2) ⊆ supp(g1) ∪ supp(g2).

LaTeX

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

Lean4

theorem support_add [DecidableEq ι] : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
  support_zipWith

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