English
Let α be a commutative monoid with a partial order that is compatible with the monoid operation. Then the additive structure on α is an ordered additive monoid; in particular, for all a ≤ b and all c in α, a + c ≤ b + c.
Русский
Пусть α является коммутативным моноидом с частичным порядком, совместимым с операцией моноида. Тогда аддитивная структура на α является упорядоченным аддитивным моноидом; в частности, для любых a ≤ b и любого c в α выполняется a + c ≤ b + c.
LaTeX
$$$[\text{CommMonoid}(\alpha)]\,[\text{PartialOrder}(\alpha)]\,[\text{IsOrderedMonoid}(\alpha)] \Rightarrow \text{IsOrderedAddMonoid}(\mathrm{Additive}(\alpha)).$$$
Lean4
instance isOrderedAddMonoid [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedAddMonoid (Additive α) :=
{ add_le_add_left := @IsOrderedMonoid.mul_le_mul_left α _ _ _ }
