# mathlib3documentation

data.multiset.sum

# Disjoint sum of multisets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.disj_sum: s.disj_sum t is the disjoint sum of s and t.
def multiset.disj_sum {α : Type u_1} {β : Type u_2} (s : multiset α) (t : multiset β) :
multiset β)

Disjoint sum of multisets.

Equations
@[simp]
theorem multiset.zero_disj_sum {α : Type u_1} {β : Type u_2} (t : multiset β) :
0.disj_sum t =
@[simp]
theorem multiset.disj_sum_zero {α : Type u_1} {β : Type u_2} (s : multiset α) :
s.disj_sum 0 =
@[simp]
theorem multiset.card_disj_sum {α : Type u_1} {β : Type u_2} (s : multiset α) (t : multiset β) :
theorem multiset.mem_disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {x : α β} :
x s.disj_sum t ( (a : α), a s = x) (b : β), b t = x
@[simp]
theorem multiset.inl_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {a : α} :
s.disj_sum t a s
@[simp]
theorem multiset.inr_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {b : β} :
s.disj_sum t b t
theorem multiset.disj_sum_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : multiset α} {t₁ t₂ : multiset β} (hs : s₁ s₂) (ht : t₁ t₂) :
s₁.disj_sum t₁ s₂.disj_sum t₂
theorem multiset.disj_sum_mono_left {α : Type u_1} {β : Type u_2} (t : multiset β) :
monotone (λ (s : multiset α), s.disj_sum t)
theorem multiset.disj_sum_mono_right {α : Type u_1} {β : Type u_2} (s : multiset α) :
theorem multiset.disj_sum_lt_disj_sum_of_lt_of_le {α : Type u_1} {β : Type u_2} {s₁ s₂ : multiset α} {t₁ t₂ : multiset β} (hs : s₁ < s₂) (ht : t₁ t₂) :
s₁.disj_sum t₁ < s₂.disj_sum t₂
theorem multiset.disj_sum_lt_disj_sum_of_le_of_lt {α : Type u_1} {β : Type u_2} {s₁ s₂ : multiset α} {t₁ t₂ : multiset β} (hs : s₁ s₂) (ht : t₁ < t₂) :
s₁.disj_sum t₁ < s₂.disj_sum t₂
theorem multiset.disj_sum_strict_mono_left {α : Type u_1} {β : Type u_2} (t : multiset β) :
strict_mono (λ (s : multiset α), s.disj_sum t)
theorem multiset.disj_sum_strict_mono_right {α : Type u_1} {β : Type u_2} (s : multiset α) :
@[protected]
theorem multiset.nodup.disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} (hs : s.nodup) (ht : t.nodup) :