min_order_le_order_add — Mathlib

English

The order of the sum of two formal power series is at least the minimum of their orders.

Русский

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

LaTeX

$$$\operatorname{order}(\phi + \psi) \ge \min\big(\operatorname{order}(\phi),\operatorname{order}(\psi)\big)$$$

Lean4

/-- The order of the sum of two formal power series
is at least the minimum of their orders. -/
theorem min_order_le_order_add (φ ψ : R⟦X⟧) : min (order φ) (order ψ) ≤ order (φ + ψ) :=
  by
  refine le_order _ _ ?_
  simp +contextual [coeff_of_lt_order]

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