vars_mul — Mathlib

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

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