support_add_eq — Mathlib

English

If the supports of g1 and g2 are disjoint, then the support of g1 + g2 is exactly the union of their supports.

Русский

Если supports g1 и g2 не пересекаются, то supp(g1 + g2) = supp(g1) ∪ supp(g2).

LaTeX

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

Lean4

theorem support_add_eq [DecidableEq ι] (h : Disjoint g₁.support g₂.support) :
    (g₁ + g₂).support = g₁.support ∪ g₂.support :=
  le_antisymm support_zipWith fun a ha => by cases (Finset.mem_union_of_disjoint h).mp ha <;> simp_all

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