wittPolyProd_vars — Mathlib

English

The variables of the Witt polynomial product lie inside a specified finite product set: the product of all variables across the two indices up to n.

Русский

Переменные произведения Witt-полиномов лежат внутри заданного конечного множества переменных, охватывающего обе координаты до n.

LaTeX

$$$\text{wittPolyProd }(p,n).vars \subseteq \text{univ} \times \text{range}(n+1).$$$

Lean4

theorem wittPolyProd_vars (n : ℕ) : (wittPolyProd p n).vars ⊆ univ ×ˢ range (n + 1) :=
  by
  rw [wittPolyProd]
  apply Subset.trans (vars_mul _ _)
  refine union_subset ?_ ?_ <;>
    · refine Subset.trans (vars_rename _ _) ?_
      simp [wittPolynomial_vars, image_subset_iff]

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