English
If idx is finite and Φ ∈ MvPolynomial idx ℚ, then the set of variables of wittStructureRat p Φ n is contained in univ ×ˢ range(n+1).
Русский
Пусть idx конечен. Тогда переменные wittStructureRat p Φ n лежат внутри универсального множества × диапазон(n+1).
LaTeX
$$$(\\mathrm{wittStructureRat}\\ p \\ Φ \\ n).\\mathrm{vars} \\subseteq \\mathrm{Finset.univ} \\timesˢ \\mathrm{Finset.range}(n+1)$$$
Lean4
theorem wittStructureRat_vars [Fintype idx] (Φ : MvPolynomial idx ℚ) (n : ℕ) :
(wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1) :=
by
rw [wittStructureRat]
intro x hx
simp only [Finset.mem_product, true_and, Finset.mem_univ, Finset.mem_range]
obtain ⟨k, hk, hx'⟩ := mem_vars_bind₁ _ _ hx
obtain ⟨i, -, hx''⟩ := mem_vars_bind₁ _ _ hx'
obtain ⟨j, hj, rfl⟩ := mem_vars_rename _ _ hx''
rw [wittPolynomial_vars, Finset.mem_range] at hj
replace hk := xInTermsOfW_vars_subset p _ hk
grind
-- we could relax the fintype on `idx`, but then we need to cast from finset to set.
-- for our applications `idx` is always finite.
