instIsOrderedAddMonoid — Mathlib

English

The natural numbers ℕ form an ordered additive monoid; addition preserves order: a ≤ b implies a + c ≤ b + c for all a,b,c ∈ ℕ.

Русский

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

LaTeX

$$$\forall a,b,c \in \mathbb{N},\ a \le b \Rightarrow a+c \le b+c.$$$

Lean4

instance instIsOrderedAddMonoid : IsOrderedAddMonoid ℕ where add_le_add_left := @Nat.add_le_add_left

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