instIsOrderedCancelAddMonoid — Mathlib

English

The multiset with addition forms an ordered cancel additive monoid: adding the same multiset to both sides preserves order, and if a ≤ b then there exists c with a + c = b.

Русский

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

LaTeX

$$$\\forall a,b,c:\\ \\ a \\le b \\Rightarrow a+c \\le b+c$ and $\\exists c\\; (a+c=b).$$$

Lean4

instance : IsOrderedCancelAddMonoid (Multiset α)
    where
  add_le_add_left := fun _ _ => add_le_add_left
  le_of_add_le_add_left := fun _ _ _ => le_of_add_le_add_left

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