English
Chevalley’s theorem for mvPolynomialC with degree bounds asserts the existence of a T describing the image of S under a Chevalley-type construction, with explicit degree constraints.
Русский
Теорема Чевалле для mvPolynomialC с ограничениями степеней утверждает существование множества T, описывающего образ S при Чеваллейском конструировании, с явными ограничениями степеней.
LaTeX
$$∀ k m n, ∃ T, comap MvPolynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.n ≤ numBound k (fun i => 1 + (d.map Fin.val).count i) n ∧ ∀ i, C.g i ∈ M ^ (degBound k (fun i => 1 + (d.map Fin.val).count i) n)$$
Lean4
/-- The bound on the degree of the polynomials used to describe the constructible set appearing in
Chevalley's theorem with complexity bound. -/
def degBound (k m n : ℕ) (d : Multiset (Fin m)) : ℕ :=
MvPolynomialC.degBound (k + n) (1 + (d.map Fin.val).count ·) m
