sup_support_finset_prod_le — Mathlib

English

For a finite product over a Finset, the supremum of the degree of the product is bounded by the sum of the supremums of the degrees of the factors.

Русский

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

LaTeX

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

Lean4

theorem sup_support_finset_prod_le (degb0 : degb 0 ≤ 0) (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b) (s : Finset ι)
    (f : ι → R[A]) : (∏ i ∈ s, f i).support.sup degb ≤ ∑ i ∈ s, (f i).support.sup degb :=
  (sup_support_multiset_prod_le degb0 degbm _).trans_eq <| congr_arg _ <| Multiset.map_map _ _ _

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