degree_sum_le — Mathlib

English

The degree of a sum of polynomials is at most the supremum of their degrees.

Русский

Степень суммы множителей не превышает верхнюю грань степеней слагаемых.

LaTeX

$$$\deg\left(\sum_{i \in s} f(i)\right) \le \sup_{i \in s} \deg(f(i))$$$

Lean4

theorem degree_sum_le (s : Finset ι) (f : ι → R[X]) : degree (∑ i ∈ s, f i) ≤ s.sup fun b => degree (f b) :=
  Finset.cons_induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl]) fun a s has ih =>
    calc
      degree (∑ i ∈ cons a s has, f i) ≤ max (degree (f a)) (degree (∑ i ∈ s, f i)) := by rw [Finset.sum_cons];
        exact degree_add_le _ _
      _ ≤ _ := by rw [sup_cons]; exact max_le_max le_rfl ih

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