supDegree_sum_lt — Mathlib

English

For a finite index set s and functions f_i ∈ R[A], the supDegree of the product is at most the sum of the supDegrees.

Русский

Для конечного индекса s и функций f_i сумма supDegree не превосходит произведение.

LaTeX

$$$\left(\prod_{i \in s} f_i\right).supDegree D \le \sum_{i \in s} (f_i).supDegree D$$$

Lean4

theorem supDegree_sum_lt (hs : s.Nonempty) {b : B} (h : ∀ i ∈ s, (f i).supDegree D < b) :
    (∑ i ∈ s, f i).supDegree D < b :=
  by
  refine supDegree_sum_le.trans_lt ((Finset.sup_lt_iff ?_).mpr h)
  obtain ⟨i, hi⟩ := hs; exact bot_le.trans_lt (h i hi)

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