le_order_prod — Mathlib

English

For a finite index set s, the sum of the orders of a family of power series is bounded above by the order of the product of the family.

Русский

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

LaTeX

$$$ \sum_{i \in s} (\operatorname{ord}(f_i)) \le \operatorname{ord}\Big( \prod_{i \in s} f_i \Big) $$$

Lean4

theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*} (f : ι → MvPowerSeries σ R) (s : Finset ι) :
    ∑ i ∈ s, (f i).order ≤ (∏ i ∈ s, f i).order :=
  le_weightedOrder_prod _ _ _

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