min_order_le_order_add — Mathlib

English

The minimum of the orders of x and y is at most the order of x+y: min(x.order, y.order) ≤ (x+y).order.

Русский

Минимум порядков x и y не превосходит порядок суммы: min(x.order, y.order) ≤ (x+y).order.

LaTeX

$$$$ \min\left( x.order, y.order \right) \le (x+y).order. $$$$

Lean4

theorem min_order_le_order_add {Γ} [Zero Γ] [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x + y ≠ 0) :
    min x.order y.order ≤ (x + y).order := by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  rw [order_of_ne hx, order_of_ne hy, order_of_ne hxy]
  exact HahnSeries.min_le_min_add hx hy hxy

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