degBound — Mathlib

English

For constructible data S in R[X], the degree bound is defined as the supremum, over all constructible components C in S, of the sum of the degrees of the polynomials g_i appearing in C, plus one.

Русский

Для конструктивных данных S в R[X] граница степеней определяется как верхняя граница по всем компонентам C из S суммы степеней полиномов g_i, появляющихся в C, плюс один.

LaTeX

$$$\degBound(S) = \sup_{C} \sum_i \deg( C.g_i ) + 1$$$

Lean4

/-- The degree bound on a constructible set for Chevalley's theorem for the inclusion `R ↪ R[X]`. -/
def degBound (S : ConstructibleSetData R[X]) : ℕ :=
  S.sup fun C ↦ ∑ i, (C.g i).degree.succ

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