min_orderTop_le_orderTop_add — Mathlib

English

The minimum of the orderTop values is at most the orderTop of the sum: min(x.orderTop, y.orderTop) ≤ (x+y).orderTop.

Русский

Минимум значений orderTop не превосходит orderTop суммы: min(x.orderTop, y.orderTop) ≤ (x+y).orderTop.

LaTeX

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

Lean4

theorem min_orderTop_le_orderTop_add {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} :
    min x.orderTop y.orderTop ≤ (x + y).orderTop :=
  by
  by_cases hx : x = 0; · simp [hx]
  by_cases hy : y = 0; · simp [hy]
  by_cases hxy : x + y = 0; · simp [hxy]
  rw [orderTop_of_ne_zero hx, orderTop_of_ne_zero hy, orderTop_of_ne_zero hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
  exact HahnSeries.min_le_min_add hx hy hxy

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