isOrderedAddMonoid — Mathlib

English

ZNum forms an ordered additive monoid, i.e., addition is order-preserving: a ≤ b implies a+c ≤ b+c.

Русский

ZNum образует упорядоченный аддитивный монади, т.е. сложение сохраняет порядок: a ≤ b ⇒ a+c ≤ b+c.

LaTeX

$$$$\text{IsOrderedAddMonoid}(ZNum) \quad\text{with }\ a \le b \Rightarrow a+c \le b+c.$$$$

Lean4

instance isOrderedAddMonoid : IsOrderedAddMonoid ZNum :=
  { add_le_add_left := add_le_add_left }

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