instOrderedSub — Mathlib

English

Multiset α carries a submultiset order: s ≤ t if and only if s is a submultiset of t; this order is compatible with addition (submultiset relation is preserved when adding the same multiset).

Русский

Мультимножество α снабжается порядком подмножества: s ≤ t тогда и только тогда, когда s является подпоследовательным мультимножество t; этот порядок совместим с сложением.

LaTeX

$$$s \le t \iff s \text{ is a submultiset of } t.$$$

Lean4

instance : OrderedSub (Multiset α) where tsub_le_iff_right _n _m _k := Multiset.sub_le_iff_le_add

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