English
If each function f_i has finite support, then the product over i ∈ s of f_i, viewed as a function of the base variable, also has finite support contained in the union of the supports of the f_i.
Русский
Если каждый f_i имеет конечную опору, то произведение по i∈s функций x ↦ f_i(x) тоже имеет конечную опору, вложенную в объединение опор всех f_i.
LaTeX
$$$\\operatorname{mulSupport}\\bigl(x \\mapsto \\prod_{i \\in s} f_i(x)\\bigr) \\subseteq \\bigcup_{i \\in s} \\operatorname{mulSupport}(f_i).$$$
Lean4
@[to_additive]
theorem mulSupport_prod (s : Finset ι) (f : ι → κ → M) :
mulSupport (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i) :=
by
simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, notMem_mulSupport]
exact fun x ↦ prod_eq_one
