instIsOrderedAddMonoid — Mathlib

English

If α is an ordered additive monoid, then its opposite αᵐᵒᵖ is also an IsOrderedAddMonoid.

Русский

Если α — упорядоченный аддитивный моноид, то противоположный моноид αᵐᵒᵖ также упорядочен по аддитивному порядку.

LaTeX

$$IsOrderedAddMonoid(αᵐᵒᵖ)$$

Lean4

instance [IsOrderedAddMonoid α] : IsOrderedAddMonoid αᵐᵒᵖ where
  add_le_add_left a b hab c := add_le_add_left (by simpa) c.unop

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