instIsOrderedCancelAddMonoid — Mathlib

English

NatOrdinal with addition forms an ordered cancel additive monoid: if a ≤ b then a + c ≤ b + c, and conversely, if a + c ≤ b + c then a ≤ b.

Русский

NatOrdinal с операцией сложения образует упорядоченный моноид с отменяемым сложением: a ≤ b тогда и только тогда, когда a + c ≤ b + c.

LaTeX

$$$$ (a \le b) \Rightarrow (a + c \le b + c) \land (a + c \le b + c) \Rightarrow (a \le b) $$$$

Lean4

instance : IsOrderedCancelAddMonoid NatOrdinal :=
  { add_le_add_left := fun _ _ => add_le_add_left
    le_of_add_le_add_left := fun _ _ _ => le_of_add_le_add_left }

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