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 : Multiset α) (t : Multiset β) : Multiset (α ⊕ β)

Disjoint sum of multisets.

Equations

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

@[simp]

theorem Multiset.zero_disjSum {α : Type u_1} {β : Type u_2} (t : Multiset β) : Multiset.disjSum 0 t = Multiset.map Sum.inr t

@[simp]

theorem Multiset.disjSum_zero {α : Type u_1} {β : Type u_2} (s : Multiset α) : Multiset.disjSum s 0 = Multiset.map Sum.inl s

@[simp]

theorem Multiset.card_disjSum {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β) : Multiset.card (Multiset.disjSum s t) = Multiset.card s + Multiset.card t

theorem Multiset.mem_disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {x : α ⊕ β} : x ∈ Multiset.disjSum s t ↔ (∃ a ∈ s, Sum.inl a = x) ∨ ∃ b ∈ t, Sum.inr b = x

@[simp]

theorem Multiset.inl_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {a : α} : Sum.inl a ∈ Multiset.disjSum s t ↔ a ∈ s

@[simp]

theorem Multiset.inr_mem_disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {b : β} : Sum.inr b ∈ Multiset.disjSum s t ↔ b ∈ t

theorem Multiset.disjSum_mono {α : Type u_1} {β : Type u_2} {s₁ : Multiset α} {s₂ : Multiset α} {t₁ : Multiset β} {t₂ : Multiset β} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : Multiset.disjSum s₁ t₁ ≤ Multiset.disjSum s₂ t₂

theorem Multiset.disjSum_mono_left {α : Type u_1} {β : Type u_2} (t : Multiset β) : Monotone fun (s : Multiset α) => Multiset.disjSum s t

theorem Multiset.disjSum_mono_right {α : Type u_1} {β : Type u_2} (s : Multiset α) : Monotone (Multiset.disjSum s)

theorem Multiset.disjSum_lt_disjSum_of_lt_of_le {α : Type u_1} {β : Type u_2} {s₁ : Multiset α} {s₂ : Multiset α} {t₁ : Multiset β} {t₂ : Multiset β} (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₁ : Multiset α} {s₂ : Multiset α} {t₁ : Multiset β} {t₂ : Multiset β} (hs : s₁ ≤ s₂) (ht : t₁ < t₂) : Multiset.disjSum s₁ t₁ < Multiset.disjSum s₂ t₂

theorem Multiset.disjSum_strictMono_left {α : Type u_1} {β : Type u_2} (t : Multiset β) : StrictMono fun (s : Multiset α) => Multiset.disjSum s t

theorem Multiset.disjSum_strictMono_right {α : Type u_1} {β : Type u_2} (s : Multiset α) : StrictMono (Multiset.disjSum s)

theorem Multiset.Nodup.disjSum {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} (hs : Multiset.Nodup s) (ht : Multiset.Nodup t) : Multiset.Nodup (Multiset.disjSum s t)