min_weightedOrder_le_add — Mathlib

English

The weighted order of the sum is at least the minimum of the two orders.

Русский

Порядок суммы не меньшe минимума двух порядков.

LaTeX

$$min(f.weightedOrder w, g.weightedOrder w) ≤ (f+g).weightedOrder w$$

Lean4

/-- The order of the sum of two formal power series is at least the minimum of their orders. -/
theorem min_weightedOrder_le_add : min (f.weightedOrder w) (g.weightedOrder w) ≤ (f + g).weightedOrder w :=
  by
  apply le_weightedOrder w
  simp +contextual only [coeff_eq_zero_of_lt_weightedOrder w, lt_min_iff, map_add, add_zero, imp_true_iff]

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