instCanonicallyOrderedAdd — Mathlib

English

ℕ is canonically ordered as an additive monoid: for a ≤ b there exists c with a + c = b.

Русский

ℕ является канонически упорядоченным по сложению: если a ≤ b, то существует c такой, что a + c = b.

LaTeX

$$$a \le b \Rightarrow \exists c\, (a+c=b).$$$

Lean4

instance instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℕ
    where
  le_add_self := Nat.le_add_left
  le_self_add := Nat.le_add_right
  exists_add_of_le := Nat.exists_eq_add_of_le

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