support_prod — Mathlib

English

The support of the product over a Finset equals the intersection of the supports of the factors.

Русский

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

LaTeX

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

Lean4

theorem support_prod (s : Finset ι) (f : ι → κ → M₀) : support (fun j ↦ ∏ i ∈ s, f i j) = ⋂ i ∈ s, support (f i) :=
  Set.ext fun x ↦ by simp [support, prod_eq_zero_iff]

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