untop₀_neg — Mathlib

English

For AddCommGroup α, LinearOrder α, IsOrderedAddMonoid α, (-a).untop₀ = -a.untop₀ for any a in WithTop α.

Русский

Для AddCommGroup α, LinearOrder α, IsOrderedAddMonoid α: (-a).untop₀ = -a.untop₀.

LaTeX

$$$[AddCommGroup \alpha] [LinearOrder \alpha] [IsOrderedAddMonoid \alpha]\; (-a).untop_0 = -a.untop_0$$$

Lean4

@[simp]
theorem untop₀_neg [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a : WithTop α) : (-a).untop₀ = -a.untop₀ :=
  by
  cases a with
  | top => simp
  | coe a =>
    rw [← LinearOrderedAddCommGroup.coe_neg, untop₀_coe]
    simp

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