instLinearOrderedAddCommGroupWithTopOfIsOrderedAddMonoid

English

abv(a - b) = abv(b - a).

Русский

abv(a - b) = abv(b - a).

LaTeX

$$abv(a - b) = abv(b - a)$$

Lean4

instance [LinearOrder α] [IsOrderedAddMonoid α] : LinearOrderedAddCommGroupWithTop (WithTop α)
    where
  __ := WithTop.linearOrderedAddCommMonoidWithTop
  __ := WithTop.nontrivial
  sub_eq_add_neg a b := by cases a <;> cases b <;> simp [← coe_sub, ← coe_neg, sub_eq_add_neg]
  neg_top := WithTop.map_top _
  zsmul := zsmulRec
  add_neg_cancel := by
    rintro (a | a) ha
    · exact (ha rfl).elim
    · exact (WithTop.coe_add ..).symm.trans (WithTop.coe_eq_coe.2 (add_neg_cancel a))

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