instCanonicallyOrderedAdd — Mathlib

English

The additive structure on multisets is canonically ordered: from a ≤ b one can obtain b by adding some multiset to a.

Русский

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

LaTeX

$$$\\forall a,b:\\ a \\le b \\Rightarrow \\exists c:\\ a+c=b.$$$

Lean4

instance : CanonicallyOrderedAdd (Multiset α)
    where
  le_add_self := le_add_left
  le_self_add := le_add_right
  exists_add_of_le h := exists_add_of_le h

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