totalDegree_finset_sum — Mathlib

English

The total degree of a Finset sum is bounded by the supremum over the degrees of summands.

Русский

Общая степень суммы по Finset не превышает верхнюю границу степеней слагаемых.

LaTeX

$$$\operatorname{totalDegree}\left(\sum_{i \in s} f(i)\right) \le \operatorname{Finset.sup}(s)\, (\operatorname{totalDegree}(f(i)))$$$

Lean4

theorem totalDegree_finset_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (s.sum f).totalDegree ≤ Finset.sup s fun i => (f i).totalDegree := by
  induction s using Finset.cons_induction with
  | empty => exact zero_le _
  | cons a s has hind =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

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