English
The variables appearing in the scaled polyOfInterest are contained within the universal index set paired with the finite index set {0,...,n}. This bounds the complexity of variable interactions.
Русский
Переменные, которые появляются в масштабированном polyOfInterest, лежат внутри универзального множества индексов, сопряженного с конечным множеством {0,...,n}. Это ограничивает сложность взаимодействий переменных.
LaTeX
$$$\operatorname{vars}\bigl((p^{n+1})^{\phantom{|}} \cdot polyOfInterest\ p\ n\bigr) \subseteq \operatorname{univ} \times\!\operatorname{range}(n+1)$$$
Lean4
theorem mul_polyOfInterest_vars (n : ℕ) : ((p : 𝕄) ^ (n + 1) * polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1) :=
by
rw [mul_polyOfInterest_aux5]
apply Subset.trans (vars_sub_subset _)
refine union_subset ?_ ?_
· apply remainder_vars
· apply wittPolyProdRemainder_vars
