union_le_union_right — Mathlib

English

Let s, t, u be multisets. If s is a submultiset of t (s ≤ t), then s ∪ u is a submultiset of t ∪ u (s ∪ u ≤ t ∪ u).

Русский

Пусть s, t, u — мультимножества. Если s является подмножество по мультинаборам к t (s ≤ t), то s ∪ u является подмножеством к t ∪ u (s ∪ u ≤ t ∪ u).

LaTeX

$$$\\forall \\alpha\\, s,t,u \\in \\mathrm{Multiset}(\\alpha),\\ s \\le t \\Rightarrow s \\cup u \\le t \\cup u.$$$

Lean4

@[gcongr]
theorem union_le_union_right (h : s ≤ t) (u) : s ∪ u ≤ t ∪ u :=
  Multiset.add_le_add_right <| Multiset.sub_le_sub_right h

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