support_mul — Mathlib

English

For g1,g2 : Finsupp α β with MulZeroClass β and DecidableEq α, the support of g1 * g2 is contained in the intersection of supports: (g1 * g2).support ⊆ g1.support ∩ g2.support.

Русский

Для g1,g2 : Finsupp α β с MulZeroClass β и DecidableEq α, опора g1 * g2 ⊆ опора g1 ∩ опора g2.

LaTeX

$$$ (g_1 * g_2).\\operatorname{support} \\subseteq g_1.\\operatorname{support} \\cap g_2.\\operatorname{support} $$$

Lean4

theorem support_mul [DecidableEq α] {g₁ g₂ : α →₀ β} : (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support :=
  subset_inter support_mul_subset_left support_mul_subset_right

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