supDegree_sum_le — Mathlib

English

For a finite collection of polynomials, the supremum degree of their sum is bounded by the supremum of the sum of individual supremums.

Русский

Для конечной коллекции полиномов верхняя грань степени их суммы ограничена верхней гранью суммы отдельных степеней.

LaTeX

$$$\\sup\\deg(\\sum_{i\\in s} f_i) ≤ \\sum_{i\\in s} \\sup\\deg(f_i)$$$

Lean4

theorem supDegree_sum_le {ι} {s : Finset ι} {f : ι → R[A]} :
    (∑ i ∈ s, f i).supDegree D ≤ s.sup (fun i => (f i).supDegree D) := by
  classical exact (Finset.sup_mono Finsupp.support_finset_sum).trans_eq (Finset.sup_biUnion _ _)

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