mathlib3 documentation

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 #

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

Disjoint sum of multisets.

Equations
source
@[simp]
theorem multiset.zero_disj_sum {α : Type u_1} {β : Type u_2} (t : multiset β) :
0.disj_sum t = multiset.map sum.inr t
source
@[simp]
theorem multiset.disj_sum_zero {α : Type u_1} {β : Type u_2} (s : multiset α) :
s.disj_sum 0 = multiset.map sum.inl s
source
@[simp]
theorem multiset.card_disj_sum {α : Type u_1} {β : Type u_2} (s : multiset α) (t : multiset β) :
⇑multiset.card (s.disj_sum t) = ⇑multiset.card s + ⇑multiset.card t
source
theorem multiset.mem_disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {x : α ⊕ β} :
x ∈ s.disj_sum t ↔ (∃ (a : α), a ∈ s ∧ sum.inl a = x) ∨ ∃ (b : β), b ∈ t ∧ sum.inr b = x
source
@[simp]
theorem multiset.inl_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {a : α} :
sum.inl a ∈ s.disj_sum t ↔ a ∈ s
source
@[simp]
theorem multiset.inr_mem_disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} {b : β} :
sum.inr b ∈ s.disj_sum t ↔ b ∈ t
source
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₂
source
theorem multiset.disj_sum_mono_left {α : Type u_1} {β : Type u_2} (t : multiset β) :
monotone (λ (s : multiset α), s.disj_sum t)
source
theorem multiset.disj_sum_mono_right {α : Type u_1} {β : Type u_2} (s : multiset α) :
monotone s.disj_sum
source
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₂
source
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₂
source
theorem multiset.disj_sum_strict_mono_left {α : Type u_1} {β : Type u_2} (t : multiset β) :
strict_mono (λ (s : multiset α), s.disj_sum t)
source
theorem multiset.disj_sum_strict_mono_right {α : Type u_1} {β : Type u_2} (s : multiset α) :
strict_mono s.disj_sum
source
@[protected]
theorem multiset.nodup.disj_sum {α : Type u_1} {β : Type u_2} {s : multiset α} {t : multiset β} (hs : s.nodup) (ht : t.nodup) :
(s.disj_sum t).nodup