totalDegree_finsetSum_le — Mathlib

English

Let {f_i} be a finite family of multivariate polynomials. If every f_i has total degree at most d, then the total degree of their sum is at most d.

Русский

Пусть {f_i} — конечное множество многочленов в нескольких переменных. Если каждый f_i имеет общую степень не более d, то общая степень их суммы не превосходит d.

LaTeX

$$$\\\\forall ι \\\\ {s : Finset ι} \\\\ {f : ι → MvPolynomial σ R} \\\\ {d : \\mathbb{N}}, \\\\ (\\\\forall i \\\\in s, (f i).totalDegree \\\\le d) \\\\Rightarrow (s.sum f).totalDegree \\\\le d$$$

Lean4

theorem totalDegree_finsetSum_le {ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} {d : ℕ}
    (hf : ∀ i ∈ s, (f i).totalDegree ≤ d) : (s.sum f).totalDegree ≤ d :=
  (totalDegree_finset_sum ..).trans <| Finset.sup_le hf

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