orderTop_sub — Mathlib

English

WithTop variant: the minimum of x.orderTop and y.orderTop is not greater than the orderTop of x+y.

Русский

Вариант WithTop: минимум x.orderTop и y.orderTop не больше orderTop суммы x+y.

LaTeX

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

Lean4

theorem orderTop_sub {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : x.orderTop < y.orderTop) :
    (x - y).orderTop = x.orderTop := by
  rw [sub_eq_add_neg]
  rw [← orderTop_neg (x := y)] at hxy
  exact orderTop_add_eq_left hxy

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