English
Let t be a finite set of indices and φ_i be polynomials for i in t. Then the set of variables appearing in the sum ∑_{i∈t} φ_i is contained in the union of the variable sets of the φ_i.
Русский
Пусть t — конечное множество индексов, и для каждого i ∈ t полином φ_i. Тогда множество переменных, встречающихся в сумме ∑_{i∈t} φ_i, содержится в объединении переменных полиномов φ_i.
LaTeX
$$$ (\sum_{i \in t} \phi_i).vars \subseteq \mathrm{Finset.biUnion}_{i \in t} (\phi_i).vars $$$
Lean4
theorem vars_sum_subset [DecidableEq σ] : (∑ i ∈ t, φ i).vars ⊆ Finset.biUnion t fun i => (φ i).vars := by
classical
induction t using Finset.induction_on with
| empty => simp
| insert _ _ has hsum =>
rw [Finset.biUnion_insert, Finset.sum_insert has]
refine Finset.Subset.trans (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
assumption
