# Bind operation for multisets #

This file defines a few basic operations on Multiset, notably the monadic bind.

## Main declarations #

• Multiset.join: The join, aka union or sum, of multisets.
• Multiset.bind: The bind of a multiset-indexed family of multisets.
• Multiset.product: Cartesian product of two multisets.
• Multiset.sigma: Disjoint sum of multisets in a sigma type.

### Join #

def Multiset.join {α : Type u_1} :
Multiset ()

join S, where S is a multiset of multisets, is the lift of the list join operation, that is, the union of all the sets. join {{1, 2}, {1, 2}, {0, 1}} = {0, 1, 1, 1, 2, 2}

Equations
• Multiset.join = Multiset.sum
Instances For
theorem Multiset.coe_join {α : Type u_1} (L : List (List α)) :
((List.map Multiset.ofList L)).join = L.join
@[simp]
theorem Multiset.join_zero {α : Type u_1} :
@[simp]
theorem Multiset.join_cons {α : Type u_1} (s : ) (S : Multiset ()) :
(s ::ₘ S).join = s + S.join
@[simp]
theorem Multiset.join_add {α : Type u_1} (S : Multiset ()) (T : Multiset ()) :
(S + T).join = S.join + T.join
@[simp]
theorem Multiset.singleton_join {α : Type u_1} (a : ) :
{a}.join = a
@[simp]
theorem Multiset.mem_join {α : Type u_1} {a : α} {S : Multiset ()} :
a S.join sS, a s
@[simp]
theorem Multiset.card_join {α : Type u_1} (S : Multiset ()) :
Multiset.card S.join = (Multiset.map (Multiset.card) S).sum
@[simp]
theorem Multiset.map_join {α : Type u_1} {β : Type v} (f : αβ) (S : Multiset ()) :
Multiset.map f S.join = ().join
@[simp]
theorem Multiset.sum_join {α : Type u_1} [] {S : Multiset ()} :
S.join.sum = (Multiset.map Multiset.sum S).sum
@[simp]
theorem Multiset.prod_join {α : Type u_1} [] {S : Multiset ()} :
S.join.prod = (Multiset.map Multiset.prod S).prod
theorem Multiset.rel_join {α : Type u_1} {β : Type v} {r : αβProp} {s : Multiset ()} {t : Multiset ()} (h : Multiset.Rel () s t) :
Multiset.Rel r s.join t.join

### Bind #

def Multiset.bind {α : Type u_1} {β : Type v} (s : ) (f : α) :

s.bind f is the monad bind operation, defined as (s.map f).join. It is the union of f a as a ranges over s.

Equations
• s.bind f = ().join
Instances For
@[simp]
theorem Multiset.coe_bind {α : Type u_1} {β : Type v} (l : List α) (f : αList β) :
((l).bind fun (a : α) => (f a)) = (l.bind f)
@[simp]
theorem Multiset.zero_bind {α : Type u_1} {β : Type v} (f : α) :
= 0
@[simp]
theorem Multiset.cons_bind {α : Type u_1} {β : Type v} (a : α) (s : ) (f : α) :
(a ::ₘ s).bind f = f a + s.bind f
@[simp]
theorem Multiset.singleton_bind {α : Type u_1} {β : Type v} (a : α) (f : α) :
{a}.bind f = f a
@[simp]
theorem Multiset.add_bind {α : Type u_1} {β : Type v} (s : ) (t : ) (f : α) :
(s + t).bind f = s.bind f + t.bind f
@[simp]
theorem Multiset.bind_zero {α : Type u_1} {β : Type v} (s : ) :
(s.bind fun (x : α) => 0) = 0
@[simp]
theorem Multiset.bind_add {α : Type u_1} {β : Type v} (s : ) (f : α) (g : α) :
(s.bind fun (a : α) => f a + g a) = s.bind f + s.bind g
@[simp]
theorem Multiset.bind_cons {α : Type u_1} {β : Type v} (s : ) (f : αβ) (g : α) :
(s.bind fun (a : α) => f a ::ₘ g a) = + s.bind g
@[simp]
theorem Multiset.bind_singleton {α : Type u_1} {β : Type v} (s : ) (f : αβ) :
(s.bind fun (x : α) => {f x}) =
@[simp]
theorem Multiset.mem_bind {α : Type u_1} {β : Type v} {b : β} {s : } {f : α} :
b s.bind f as, b f a
@[simp]
theorem Multiset.card_bind {α : Type u_1} {β : Type v} (s : ) (f : α) :
Multiset.card (s.bind f) = (Multiset.map (Multiset.card f) s).sum
theorem Multiset.bind_congr {α : Type u_1} {β : Type v} {f : α} {g : α} {m : } :
(am, f a = g a)m.bind f = m.bind g
theorem Multiset.bind_hcongr {α : Type u_1} {β : Type v} {β' : Type v} {m : } {f : α} {f' : αMultiset β'} (h : β = β') (hf : am, HEq (f a) (f' a)) :
HEq (m.bind f) (m.bind f')
theorem Multiset.map_bind {α : Type u_1} {β : Type v} {γ : Type u_2} (m : ) (n : α) (f : βγ) :
Multiset.map f (m.bind n) = m.bind fun (a : α) => Multiset.map f (n a)
theorem Multiset.bind_map {α : Type u_1} {β : Type v} {γ : Type u_2} (m : ) (n : β) (f : αβ) :
().bind n = m.bind fun (a : α) => n (f a)
theorem Multiset.bind_assoc {α : Type u_1} {β : Type v} {γ : Type u_2} {s : } {f : α} {g : β} :
(s.bind f).bind g = s.bind fun (a : α) => (f a).bind g
theorem Multiset.bind_bind {α : Type u_1} {β : Type v} {γ : Type u_2} (m : ) (n : ) {f : αβ} :
(m.bind fun (a : α) => n.bind fun (b : β) => f a b) = n.bind fun (b : β) => m.bind fun (a : α) => f a b
theorem Multiset.bind_map_comm {α : Type u_1} {β : Type v} {γ : Type u_2} (m : ) (n : ) {f : αβγ} :
(m.bind fun (a : α) => Multiset.map (fun (b : β) => f a b) n) = n.bind fun (b : β) => Multiset.map (fun (a : α) => f a b) m
@[simp]
theorem Multiset.sum_bind {α : Type u_1} {β : Type v} [] (s : ) (t : α) :
(s.bind t).sum = (Multiset.map (fun (a : α) => (t a).sum) s).sum
@[simp]
theorem Multiset.prod_bind {α : Type u_1} {β : Type v} [] (s : ) (t : α) :
(s.bind t).prod = (Multiset.map (fun (a : α) => (t a).prod) s).prod
theorem Multiset.rel_bind {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {r : αβProp} {p : γδProp} {s : } {t : } {f : α} {g : β} (h : () f g) (hst : Multiset.Rel r s t) :
Multiset.Rel p (s.bind f) (t.bind g)
theorem Multiset.count_sum {α : Type u_1} {β : Type v} [] {m : } {f : β} {a : α} :
Multiset.count a ().sum = (Multiset.map (fun (b : β) => Multiset.count a (f b)) m).sum
theorem Multiset.count_bind {α : Type u_1} {β : Type v} [] {m : } {f : β} {a : α} :
Multiset.count a (m.bind f) = (Multiset.map (fun (b : β) => Multiset.count a (f b)) m).sum
theorem Multiset.le_bind {α : Type u_4} {β : Type u_5} {f : α} (S : ) {x : α} (hx : x S) :
f x S.bind f
theorem Multiset.attach_bind_coe {α : Type u_1} {β : Type v} (s : ) (f : α) :
(s.attach.bind fun (i : { x : α // x s }) => f i) = s.bind f
@[simp]
theorem Multiset.nodup_bind {α : Type u_1} {β : Type v} {s : } {f : α} :
(s.bind f).Nodup (as, (f a).Nodup) Multiset.Pairwise (fun (a b : α) => (f a).Disjoint (f b)) s
@[simp]
theorem Multiset.dedup_bind_dedup {α : Type u_1} {β : Type v} [] [] (s : ) (f : α) :
(s.dedup.bind f).dedup = (s.bind f).dedup

### Product of two multisets #

def Multiset.product {α : Type u_1} {β : Type v} (s : ) (t : ) :
Multiset (α × β)

The multiplicity of (a, b) in s ×ˢ t is the product of the multiplicity of a in s and b in t.

Equations
Instances For
instance Multiset.instSProd {α : Type u_1} {β : Type v} :
SProd () () (Multiset (α × β))
Equations
• Multiset.instSProd = { sprod := Multiset.product }
@[simp]
theorem Multiset.coe_product {α : Type u_1} {β : Type v} (l₁ : List α) (l₂ : List β) :
l₁ ×ˢ l₂ = (l₁ ×ˢ l₂)
@[simp]
theorem Multiset.zero_product {α : Type u_1} {β : Type v} (t : ) :
0 ×ˢ t = 0
@[simp]
theorem Multiset.cons_product {α : Type u_1} {β : Type v} (a : α) (s : ) (t : ) :
(a ::ₘ s) ×ˢ t = Multiset.map () t + s ×ˢ t
@[simp]
theorem Multiset.product_zero {α : Type u_1} {β : Type v} (s : ) :
s ×ˢ 0 = 0
@[simp]
theorem Multiset.product_cons {α : Type u_1} {β : Type v} (b : β) (s : ) (t : ) :
s ×ˢ (b ::ₘ t) = Multiset.map (fun (a : α) => (a, b)) s + s ×ˢ t
@[simp]
theorem Multiset.product_singleton {α : Type u_1} {β : Type v} (a : α) (b : β) :
{a} ×ˢ {b} = {(a, b)}
@[simp]
theorem Multiset.add_product {α : Type u_1} {β : Type v} (s : ) (t : ) (u : ) :
(s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
@[simp]
theorem Multiset.product_add {α : Type u_1} {β : Type v} (s : ) (t : ) (u : ) :
s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
@[simp]
theorem Multiset.card_product {α : Type u_1} {β : Type v} (s : ) (t : ) :
Multiset.card (s ×ˢ t) = Multiset.card s * Multiset.card t
@[simp]
theorem Multiset.mem_product {α : Type u_1} {β : Type v} {s : } {t : } {p : α × β} :
p s.product t p.1 s p.2 t
theorem Multiset.Nodup.product {α : Type u_1} {β : Type v} {s : } {t : } :
s.Nodupt.Nodup(s ×ˢ t).Nodup

### Disjoint sum of multisets #

def Multiset.sigma {α : Type u_1} {σ : αType u_4} (s : ) (t : (a : α) → Multiset (σ a)) :
Multiset ((a : α) × σ a)

Multiset.sigma s t is the dependent version of Multiset.product. It is the sum of (a, b) as a ranges over s and b ranges over t a.

Equations
Instances For
@[simp]
theorem Multiset.coe_sigma {α : Type u_1} {σ : αType u_4} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
((l₁).sigma fun (a : α) => (l₂ a)) = (l₁.sigma l₂)
@[simp]
theorem Multiset.zero_sigma {α : Type u_1} {σ : αType u_4} (t : (a : α) → Multiset (σ a)) :
= 0
@[simp]
theorem Multiset.cons_sigma {α : Type u_1} {σ : αType u_4} (a : α) (s : ) (t : (a : α) → Multiset (σ a)) :
(a ::ₘ s).sigma t = Multiset.map () (t a) + s.sigma t
@[simp]
theorem Multiset.sigma_singleton {α : Type u_1} {β : Type v} (a : α) (b : αβ) :
({a}.sigma fun (a : α) => {b a}) = {a, b a}
@[simp]
theorem Multiset.add_sigma {α : Type u_1} {σ : αType u_4} (s : ) (t : ) (u : (a : α) → Multiset (σ a)) :
(s + t).sigma u = s.sigma u + t.sigma u
@[simp]
theorem Multiset.sigma_add {α : Type u_1} {σ : αType u_4} (s : ) (t : (a : α) → Multiset (σ a)) (u : (a : α) → Multiset (σ a)) :
(s.sigma fun (a : α) => t a + u a) = s.sigma t + s.sigma u
@[simp]
theorem Multiset.card_sigma {α : Type u_1} {σ : αType u_4} (s : ) (t : (a : α) → Multiset (σ a)) :
Multiset.card (s.sigma t) = (Multiset.map (fun (a : α) => Multiset.card (t a)) s).sum
@[simp]
theorem Multiset.mem_sigma {α : Type u_1} {σ : αType u_4} {s : } {t : (a : α) → Multiset (σ a)} {p : (a : α) × σ a} :
p s.sigma t p.fst s p.snd t p.fst
theorem Multiset.Nodup.sigma {α : Type u_1} {s : } {σ : αType u_5} {t : (a : α) → Multiset (σ a)} :
s.Nodup(∀ (a : α), (t a).Nodup)(s.sigma t).Nodup