# 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`.

source
def Multiset.disjSum {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β) :
Multiset (α ⊕ β)

Disjoint sum of multisets.

Equations

- s.disjSum t = Multiset.map Sum.inl s + Multiset.map Sum.inr t

Instances For

source
@[simp]
theorem Multiset.zero_disjSum {α : Type u_1} {β : Type u_2} (t : Multiset β) :
disjSum 0 t = map Sum.inr t
source
@[simp]
theorem Multiset.disjSum_zero {α : Type u_1} {β : Type u_2} (s : Multiset α) :
s.disjSum 0 = map Sum.inl s
source
@[simp]
theorem Multiset.card_disjSum {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β) :
(s.disjSum t).card = s.card + t.card
source
theorem Multiset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {x : α ⊕ β} :
x ∈ s.disjSum t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x
source
@[simp]
theorem Multiset.inl_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {a : α} :
Sum.inl a ∈ s.disjSum t ↔ a ∈ s
source
@[simp]
theorem Multiset.inr_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {b : β} :
Sum.inr b ∈ s.disjSum t ↔ b ∈ t
source
theorem Multiset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} {t₁ t₂ : Multiset β} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :
s₁.disjSum t₁ ≤ s₂.disjSum t₂
source
theorem Multiset.disjSum_mono_left {α : Type u_1} {β : Type u_2} (t : Multiset β) :
Monotone fun (s : Multiset α) => s.disjSum t
source
theorem Multiset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : Multiset α) :
Monotone s.disjSum
source
theorem Multiset.disjSum_lt_disjSum_of_lt_of_le {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} {t₁ t₂ : Multiset β} (hs : s₁ < s₂) (ht : t₁ ≤ t₂) :
s₁.disjSum t₁ < s₂.disjSum t₂
source
theorem Multiset.disjSum_lt_disjSum_of_le_of_lt {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} {t₁ t₂ : Multiset β} (hs : s₁ ≤ s₂) (ht : t₁ < t₂) :
s₁.disjSum t₁ < s₂.disjSum t₂
source
theorem Multiset.disjSum_strictMono_left {α : Type u_1} {β : Type u_2} (t : Multiset β) :
StrictMono fun (s : Multiset α) => s.disjSum t
source
theorem Multiset.disjSum_strictMono_right {α : Type u_1} {β : Type u_2} (s : Multiset α) :
StrictMono s.disjSum
source
theorem Multiset.Nodup.disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} (hs : s.Nodup) (ht : t.Nodup) :
(s.disjSum t).Nodup
source
theorem Multiset.map_disjSum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Multiset α} {t : Multiset β} (f : α ⊕ β → γ) :
map f (s.disjSum t) = map (fun (x : α) => f (Sum.inl x)) s + map (fun (x : β) => f (Sum.inr x)) t