# Documentation

Mathlib.Data.Multiset.Sum

# 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
@[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 : ) :
= Multiset.map Sum.inl s
@[simp]
theorem Multiset.card_disjSum {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
Multiset.card () = Multiset.card s + Multiset.card t
theorem Multiset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } {x : α β} :
x (a, a s = x) b, b t = x
@[simp]
theorem Multiset.inl_mem_disjSum {α : Type u_2} {β : Type u_1} {s : } {t : } {a : α} :
a s
@[simp]
theorem Multiset.inr_mem_disjSum {α : Type u_2} {β : Type u_1} {s : } {t : } {b : β} :
b t
theorem Multiset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ : } {s₂ : } {t₁ : } {t₂ : } (hs : s₁ s₂) (ht : t₁ t₂) :
theorem Multiset.disjSum_mono_left {α : Type u_2} {β : Type u_1} (t : ) :
Monotone fun s =>
theorem Multiset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : ) :
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₂) :
Multiset.disjSum s₁ t₁ < Multiset.disjSum s₂ 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₂) :
Multiset.disjSum s₁ t₁ < Multiset.disjSum s₂ t₂
theorem Multiset.disjSum_strictMono_left {α : Type u_2} {β : Type u_1} (t : ) :
StrictMono fun s =>
theorem Multiset.disjSum_strictMono_right {α : Type u_1} {β : Type u_2} (s : ) :
theorem Multiset.Nodup.disjSum {α : Type u_1} {β : Type u_2} {s : } {t : } (hs : ) (ht : ) :