English
If the orders of two formal power series are different, the order of their sum equals the infimum of the two orders.
Русский
Если порядки двух формальных степенных рядов различны, то порядок их суммы равен наибольшему нижнему пределу двух порядков.
LaTeX
$$$\operatorname{order}(\phi + \psi) = \operatorname{order}(\phi) \sqcap \operatorname{order}(\psi)\quad\text{if } \operatorname{order}(\phi) \neq \operatorname{order}(\psi)$$$
Lean4
/-- The order of the sum of two formal power series
is the minimum of their orders if their orders differ. -/
theorem order_add_of_order_ne (φ ψ : R⟦X⟧) (h : order φ ≠ order ψ) : order (φ + ψ) = order φ ⊓ order ψ :=
by
refine le_antisymm ?_ (min_order_le_order_add _ _)
rcases h.lt_or_gt with (φ_lt_ψ | ψ_lt_φ)
· apply order_add_of_order_ne.aux _ _ φ_lt_ψ
· simpa only [add_comm, inf_comm] using order_add_of_order_ne.aux _ _ ψ_lt_φ
