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 #

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

Disjoint sum of multisets.

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