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 (Multiset α) → 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

theorem Multiset.coe_join {α : Type u_1} (L : List (List α)) : Multiset.join ↑(List.map Multiset.ofList L) = ↑(List.join L)

@[simp]

theorem Multiset.join_zero {α : Type u_1} : Multiset.join 0 = 0

@[simp]

theorem Multiset.join_cons {α : Type u_1} (s : Multiset α) (S : Multiset (Multiset α)) : Multiset.join (s ::ₘ S) = s + Multiset.join S

@[simp]

theorem Multiset.join_add {α : Type u_1} (S : Multiset (Multiset α)) (T : Multiset (Multiset α)) : Multiset.join (S + T) = Multiset.join S + Multiset.join T

@[simp]

theorem Multiset.singleton_join {α : Type u_1} (a : Multiset α) : Multiset.join {a} = a

@[simp]

theorem Multiset.mem_join {α : Type u_1} {a : α} {S : Multiset (Multiset α)} : a ∈ Multiset.join S ↔ ∃ s ∈ S, a ∈ s

@[simp]

theorem Multiset.card_join {α : Type u_1} (S : Multiset (Multiset α)) : Multiset.card (Multiset.join S) = Multiset.sum (Multiset.map (⇑Multiset.card) S)

theorem Multiset.rel_join {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset (Multiset α)} {t : Multiset (Multiset β)} (h : Multiset.Rel (Multiset.Rel r) s t) : Multiset.Rel r (Multiset.join s) (Multiset.join t)

Bind

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

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

• Multiset.bind s f = Multiset.join (Multiset.map f s)

@[simp]

theorem Multiset.coe_bind {α : Type u_1} {β : Type v} (l : List α) (f : α → List β) : (Multiset.bind ↑l fun (a : α) => ↑(f a)) = ↑(List.bind l f)

@[simp]

theorem Multiset.zero_bind {α : Type u_1} {β : Type v} (f : α → Multiset β) : Multiset.bind 0 f = 0

@[simp]

theorem Multiset.cons_bind {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (f : α → Multiset β) : Multiset.bind (a ::ₘ s) f = f a + Multiset.bind s f

@[simp]

theorem Multiset.singleton_bind {α : Type u_1} {β : Type v} (a : α) (f : α → Multiset β) : Multiset.bind {a} f = f a

@[simp]

theorem Multiset.add_bind {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset α) (f : α → Multiset β) : Multiset.bind (s + t) f = Multiset.bind s f + Multiset.bind t f

@[simp]

theorem Multiset.bind_zero {α : Type u_1} {β : Type v} (s : Multiset α) : (Multiset.bind s fun (x : α) => 0) = 0

@[simp]

theorem Multiset.bind_add {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) (g : α → Multiset β) : (Multiset.bind s fun (a : α) => f a + g a) = Multiset.bind s f + Multiset.bind s g

@[simp]

theorem Multiset.bind_cons {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) (g : α → Multiset β) : (Multiset.bind s fun (a : α) => f a ::ₘ g a) = Multiset.map f s + Multiset.bind s g

@[simp]

theorem Multiset.bind_singleton {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) : (Multiset.bind s fun (x : α) => {f x}) = Multiset.map f s

@[simp]

theorem Multiset.mem_bind {α : Type u_1} {β : Type v} {b : β} {s : Multiset α} {f : α → Multiset β} : b ∈ Multiset.bind s f ↔ ∃ a ∈ s, b ∈ f a

@[simp]

theorem Multiset.card_bind {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) : Multiset.card (Multiset.bind s f) = Multiset.sum (Multiset.map (⇑Multiset.card ∘ f) s)

theorem Multiset.bind_congr {α : Type u_1} {β : Type v} {f : α → Multiset β} {g : α → Multiset β} {m : Multiset α} : (∀ a ∈ m, f a = g a) → Multiset.bind m f = Multiset.bind m g

theorem Multiset.bind_hcongr {α : Type u_1} {β : Type v} {β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'} (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (Multiset.bind m f) (Multiset.bind m f')

theorem Multiset.map_bind {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : α → Multiset β) (f : β → γ) : Multiset.map f (Multiset.bind m n) = Multiset.bind m fun (a : α) => Multiset.map f (n a)

theorem Multiset.bind_map {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : β → Multiset γ) (f : α → β) : Multiset.bind (Multiset.map f m) n = Multiset.bind m fun (a : α) => n (f a)

theorem Multiset.bind_assoc {α : Type u_1} {β : Type v} {γ : Type u_2} {s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ} : Multiset.bind (Multiset.bind s f) g = Multiset.bind s fun (a : α) => Multiset.bind (f a) g

theorem Multiset.bind_bind {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : α → β → Multiset γ} : (Multiset.bind m fun (a : α) => Multiset.bind n fun (b : β) => f a b) = Multiset.bind n fun (b : β) => Multiset.bind m fun (a : α) => f a b

theorem Multiset.bind_map_comm {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (n : Multiset β) {f : α → β → γ} : (Multiset.bind m fun (a : α) => Multiset.map (fun (b : β) => f a b) n) = Multiset.bind n fun (b : β) => Multiset.map (fun (a : α) => f a b) m

@[simp]

theorem Multiset.sum_bind {α : Type u_1} {β : Type v} [AddCommMonoid β] (s : Multiset α) (t : α → Multiset β) : Multiset.sum (Multiset.bind s t) = Multiset.sum (Multiset.map (fun (a : α) => Multiset.sum (t a)) s)

@[simp]

theorem Multiset.prod_bind {α : Type u_1} {β : Type v} [CommMonoid β] (s : Multiset α) (t : α → Multiset β) : Multiset.prod (Multiset.bind s t) = Multiset.prod (Multiset.map (fun (a : α) => Multiset.prod (t a)) s)

theorem Multiset.rel_bind {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {r : α → β → Prop} {p : γ → δ → Prop} {s : Multiset α} {t : Multiset β} {f : α → Multiset γ} {g : β → Multiset δ} (h : (r ⇒ Multiset.Rel p) f g) (hst : Multiset.Rel r s t) : Multiset.Rel p (Multiset.bind s f) (Multiset.bind t g)

theorem Multiset.count_sum {α : Type u_1} {β : Type v} [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} : Multiset.count a (Multiset.sum (Multiset.map f m)) = Multiset.sum (Multiset.map (fun (b : β) => Multiset.count a (f b)) m)

theorem Multiset.count_bind {α : Type u_1} {β : Type v} [DecidableEq α] {m : Multiset β} {f : β → Multiset α} {a : α} : Multiset.count a (Multiset.bind m f) = Multiset.sum (Multiset.map (fun (b : β) => Multiset.count a (f b)) m)

theorem Multiset.le_bind {α : Type u_4} {β : Type u_5} {f : α → Multiset β} (S : Multiset α) {x : α} (hx : x ∈ S) : f x ≤ Multiset.bind S f

theorem Multiset.attach_bind_coe {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) : (Multiset.bind (Multiset.attach s) fun (i : { x : α // x ∈ s }) => f ↑i) = Multiset.bind s f

@[simp]

theorem Multiset.nodup_bind {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → Multiset β} : Multiset.Nodup (Multiset.bind s f) ↔ (∀ a ∈ s, Multiset.Nodup (f a)) ∧ Multiset.Pairwise (fun (a b : α) => Multiset.Disjoint (f a) (f b)) s

@[simp]

theorem Multiset.dedup_bind_dedup {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → Multiset β) : Multiset.dedup (Multiset.bind (Multiset.dedup s) f) = Multiset.dedup (Multiset.bind s f)

Product of two multisets

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

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

Equations

• Multiset.product s t = Multiset.bind s fun (a : α) => Multiset.map (Prod.mk a) t

instance Multiset.instSProd {α : Type u_1} {β : Type v} : SProd (Multiset α) (Multiset β) (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 : Multiset β) : 0 ×ˢ t = 0

@[simp]

theorem Multiset.cons_product {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (t : Multiset β) : (a ::ₘ s) ×ˢ t = Multiset.map (Prod.mk a) t + s ×ˢ t

@[simp]

theorem Multiset.product_zero {α : Type u_1} {β : Type v} (s : Multiset α) : s ×ˢ 0 = 0

@[simp]

theorem Multiset.product_cons {α : Type u_1} {β : Type v} (b : β) (s : Multiset α) (t : Multiset β) : 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 : Multiset α) (t : Multiset α) (u : Multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u

@[simp]

theorem Multiset.product_add {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) (u : Multiset β) : s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u

@[simp]

theorem Multiset.card_product {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) : Multiset.card (s ×ˢ t) = Multiset.card s * Multiset.card t

@[simp]

theorem Multiset.mem_product {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} {p : α × β} : p ∈ Multiset.product s t ↔ p.1 ∈ s ∧ p.2 ∈ t

theorem Multiset.Nodup.product {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} : Multiset.Nodup s → Multiset.Nodup t → Multiset.Nodup (s ×ˢ t)

Disjoint sum of multisets

def Multiset.sigma {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (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

• Multiset.sigma s t = Multiset.bind s fun (a : α) => Multiset.map (Sigma.mk a) (t a)

@[simp]

theorem Multiset.coe_sigma {α : Type u_1} {σ : α → Type u_4} (l₁ : List α) (l₂ : (a : α) → List (σ a)) : (Multiset.sigma ↑l₁ fun (a : α) => ↑(l₂ a)) = ↑(List.sigma l₁ l₂)

@[simp]

theorem Multiset.zero_sigma {α : Type u_1} {σ : α → Type u_4} (t : (a : α) → Multiset (σ a)) : Multiset.sigma 0 t = 0

@[simp]

theorem Multiset.cons_sigma {α : Type u_1} {σ : α → Type u_4} (a : α) (s : Multiset α) (t : (a : α) → Multiset (σ a)) : Multiset.sigma (a ::ₘ s) t = Multiset.map (Sigma.mk a) (t a) + Multiset.sigma s t

@[simp]

theorem Multiset.sigma_singleton {α : Type u_1} {β : Type v} (a : α) (b : α → β) : (Multiset.sigma {a} fun (a : α) => {b a}) = {{ fst := a, snd := b a }}

@[simp]

theorem Multiset.add_sigma {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : Multiset α) (u : (a : α) → Multiset (σ a)) : Multiset.sigma (s + t) u = Multiset.sigma s u + Multiset.sigma t u

@[simp]

theorem Multiset.sigma_add {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)) (u : (a : α) → Multiset (σ a)) : (Multiset.sigma s fun (a : α) => t a + u a) = Multiset.sigma s t + Multiset.sigma s u

@[simp]

theorem Multiset.card_sigma {α : Type u_1} {σ : α → Type u_4} (s : Multiset α) (t : (a : α) → Multiset (σ a)) : Multiset.card (Multiset.sigma s t) = Multiset.sum (Multiset.map (fun (a : α) => Multiset.card (t a)) s)

@[simp]

theorem Multiset.mem_sigma {α : Type u_1} {σ : α → Type u_4} {s : Multiset α} {t : (a : α) → Multiset (σ a)} {p : (a : α) × σ a} : p ∈ Multiset.sigma s t ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst

theorem Multiset.Nodup.sigma {α : Type u_1} {s : Multiset α} {σ : α → Type u_5} {t : (a : α) → Multiset (σ a)} : Multiset.Nodup s → (∀ (a : α), Multiset.Nodup (t a)) → Multiset.Nodup (Multiset.sigma s t)