le_weightedOrder_prod — Mathlib

English

For a finite family, the sum of orders is bounded above by the order of the product.

Русский

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

LaTeX

$$s.sum (fun i => (f i).weightedOrder w) ≤ (s.prod (fun i => f i)).weightedOrder w$$

Lean4

theorem le_weightedOrder_prod {R : Type*} [CommSemiring R] {ι : Type*} (w : σ → ℕ) (f : ι → MvPowerSeries σ R)
    (s : Finset ι) : ∑ i ∈ s, (f i).weightedOrder w ≤ (∏ i ∈ s, f i).weightedOrder w := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih =>
    rw [Finset.sum_cons ha, Finset.prod_cons ha]
    exact le_trans (add_le_add_left ih _) (le_weightedOrder_mul _)

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