support_prod_subset — Mathlib

English

In a Finset setting, the support of the parametric product is contained in the intersection of the supports of the factors.

Русский

Поддержка произведения над Finset вложена в пересечение поддержек каждого множителя.

LaTeX

$$$\\operatorname{support}\\bigl(j \\mapsto \\prod_{i\\in s} f(i,j)\\bigr) \\subseteq \\bigcap_{i\\in s} \\operatorname{support}(f(i,\\cdot))$$$

Lean4

theorem support_prod_subset (s : Finset ι) (f : ι → κ → M₀) :
    support (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋂ i ∈ s, support (f i) := fun _ hx ↦
  Set.mem_iInter₂.2 fun _ hi H ↦ hx <| prod_eq_zero hi H

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