instIsOrderedCancelAddMonoid — Mathlib

English

ℕ is an ordered cancellative additive monoid: order is compatible with addition and addition is cancellative with respect to ≤.

Русский

ℕ является упорядоченным отменяемым моноидом по сложению: порядок совместим с сложением, а сложение отменяемо относительно ≤.

LaTeX

$$$\text{IsOrderedCancelAddMonoid}(\mathbb{N})$ and the usual axioms: a ≤ b \Rightarrow a+c ≤ b+c, \text{ and } a+c ≤ b+c \Rightarrow a ≤ b.$$$

Lean4

instance instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid ℕ
    where
  add_le_add_left := @Nat.add_le_add_left
  le_of_add_le_add_left := @Nat.le_of_add_le_add_left

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