# Disjoint sum of multisets #

This file defines the disjoint sum of two multisets as Multiset (α ⊕ β). Beware not to confuse with the Multiset.sum operation which computes the additive sum.

## Main declarations #

• Multiset.disjSum: s.disjSum t is the disjoint sum of s and t.
def Multiset.disjSum {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
Multiset (α β)

Disjoint sum of multisets.

Equations
Instances For
@[simp]
theorem Multiset.zero_disjSum {α : Type u_1} {β : Type u_2} (t : ) :
= Multiset.map Sum.inr t
@[simp]
theorem Multiset.disjSum_zero {α : Type u_1} {β : Type u_2} (s : ) :
s.disjSum 0 = Multiset.map Sum.inl s
@[simp]
theorem Multiset.card_disjSum {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
Multiset.card (s.disjSum t) = Multiset.card s + Multiset.card t
theorem Multiset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } {x : α β} :
x s.disjSum t (as, = x) bt, = x
@[simp]
theorem Multiset.inl_mem_disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } {a : α} :
s.disjSum t a s
@[simp]
theorem Multiset.inr_mem_disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } {b : β} :
s.disjSum t b t
theorem Multiset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disjSum t₁ s₂.disjSum t₂
theorem Multiset.disjSum_mono_left {α : Type u_1} {β : Type u_2} (t : ) :
Monotone fun (s : ) => s.disjSum t
theorem Multiset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : ) :
Monotone s.disjSum
theorem Multiset.disjSum_lt_disjSum_of_lt_of_le {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ < s₂) (ht : t₁ t₂) :
s₁.disjSum t₁ < s₂.disjSum t₂
theorem Multiset.disjSum_lt_disjSum_of_le_of_lt {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ < t₂) :
s₁.disjSum t₁ < s₂.disjSum t₂
theorem Multiset.disjSum_strictMono_left {α : Type u_1} {β : Type u_2} (t : ) :
StrictMono fun (s : ) => s.disjSum t
theorem Multiset.disjSum_strictMono_right {α : Type u_1} {β : Type u_2} (s : ) :
StrictMono s.disjSum
theorem Multiset.Nodup.disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } (hs : s.Nodup) (ht : t.Nodup) :
(s.disjSum t).Nodup