English
The variables of a product are contained in the union of the variables of the factors.
Русский
Переменные произведения лежат в объединении переменных множителей.
LaTeX
$$$$ (\prod i \in s, f_i).\mathrm{vars} \subseteq s.\mathrm{biUnion} (\lambda i, (f_i).\mathrm{vars}) $$$$
Lean4
theorem vars_mul [DecidableEq σ] (φ ψ : MvPolynomial σ R) : (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars :=
by
simp_rw [vars_def, ← Multiset.toFinset_add, Multiset.toFinset_subset]
exact Multiset.subset_of_le degrees_mul_le