orderTop_add_eq_right — Mathlib

English

If y.orderTop < x.orderTop, then (x+y).orderTop = y.orderTop.

Русский

Если y.orderTop < x.orderTop, то (x+y).orderTop = y.orderTop.

LaTeX

$$$$ \text{If } y.orderTop < x.orderTop, \text{ then } (x+y).orderTop = y.orderTop. $$$$

Lean4

theorem orderTop_add_eq_right {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hxy : y.orderTop < x.orderTop) :
    (x + y).orderTop = y.orderTop := by
  simpa [← map_add, ← AddOpposite.op_add, hxy] using
    orderTop_add_eq_left (x := addOppositeEquiv.symm (.op y)) (y := addOppositeEquiv.symm (.op x))

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