Documentation

Mathlib.Data.Multiset.Bind

Bind operation for multisets #

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

Main declarations #

Join #

def Multiset.join {α : Type u_1} :

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} :
@[simp]
theorem Multiset.join_cons {α : Type u_1} (s : Multiset α) (S : Multiset (Multiset α)) :
@[simp]
@[simp]
theorem Multiset.singleton_join {α : Type u_1} (a : Multiset α) :
@[simp]
theorem Multiset.mem_join {α : Type u_1} {a : α} {S : Multiset (Multiset α)} :
a Multiset.join S 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 u_2} {r : αβProp} {s : Multiset (Multiset α)} {t : Multiset (Multiset β)} (h : Multiset.Rel (Multiset.Rel r) s t) :

Bind #

def Multiset.bind {α : Type u_1} {β : Type u_2} (s : Multiset α) (f : α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
@[simp]
theorem Multiset.coe_bind {α : Type u_1} {β : Type u_2} (l : List α) (f : αList β) :
(Multiset.bind l fun a => ↑(f a)) = ↑(List.bind l f)
@[simp]
theorem Multiset.zero_bind {α : Type u_2} {β : Type u_1} (f : αMultiset β) :
@[simp]
theorem Multiset.cons_bind {α : Type u_2} {β : Type u_1} (a : α) (s : Multiset α) (f : αMultiset β) :
@[simp]
theorem Multiset.singleton_bind {α : Type u_2} {β : Type u_1} (a : α) (f : αMultiset β) :
Multiset.bind {a} f = f a
@[simp]
theorem Multiset.add_bind {α : Type u_2} {β : Type u_1} (s : Multiset α) (t : Multiset α) (f : αMultiset β) :
@[simp]
theorem Multiset.bind_zero {α : Type u_2} {β : Type u_1} (s : Multiset α) :
(Multiset.bind s fun x => 0) = 0
@[simp]
theorem Multiset.bind_add {α : Type u_2} {β : Type u_1} (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_2} {β : Type u_1} (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_2} {β : Type u_1} (s : Multiset α) (f : αβ) :
(Multiset.bind s fun x => {f x}) = Multiset.map f s
@[simp]
theorem Multiset.mem_bind {α : Type u_1} {β : Type u_2} {b : β} {s : Multiset α} {f : αMultiset β} :
b Multiset.bind s f a, a s b f a
@[simp]
theorem Multiset.card_bind {α : Type u_2} {β : Type u_1} (s : Multiset α) (f : αMultiset β) :
Multiset.card (Multiset.bind s f) = Multiset.sum (Multiset.map (Multiset.card f) s)
theorem Multiset.bind_congr {α : Type u_2} {β : Type u_1} {f : αMultiset β} {g : αMultiset β} {m : Multiset α} :
(∀ (a : α), a mf a = g a) → Multiset.bind m f = Multiset.bind m g
theorem Multiset.bind_hcongr {α : Type u_2} {β : Type u_1} {β' : Type u_1} {m : Multiset α} {f : αMultiset β} {f' : αMultiset β'} (h : β = β') (hf : ∀ (a : α), a mHEq (f a) (f' a)) :
theorem Multiset.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : Multiset α) (n : αMultiset β) (f : βγ) :
theorem Multiset.bind_map {α : Type u_1} {β : Type u_3} {γ : 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 u_2} {γ : Type u_3} {s : Multiset α} {f : αMultiset β} {g : βMultiset γ} :
theorem Multiset.bind_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (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 u_2} {γ : Type u_3} (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_2} {β : Type u_1} [inst : AddCommMonoid β] (s : Multiset α) (t : αMultiset β) :
@[simp]
theorem Multiset.prod_bind {α : Type u_2} {β : Type u_1} [inst : CommMonoid β] (s : Multiset α) (t : αMultiset β) :
theorem Multiset.rel_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {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) :
theorem Multiset.count_sum {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] {m : Multiset β} {f : βMultiset α} {a : α} :
theorem Multiset.count_bind {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] {m : Multiset β} {f : βMultiset α} {a : α} :
theorem Multiset.le_bind {α : Type u_1} {β : Type u_2} {f : αMultiset β} (S : Multiset α) {x : α} (hx : x S) :
theorem Multiset.attach_bind_coe {α : Type u_1} {β : Type u_2} (s : Multiset α) (f : αMultiset β) :
(Multiset.bind (Multiset.attach s) fun i => f i) = Multiset.bind s f

Product of two multisets #

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

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

Equations

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

Equations
@[simp]
theorem Multiset.coe_product {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
l₁ ×ˢ l₂ = ↑(l₁ ×ˢ l₂)
@[simp]
theorem Multiset.zero_product {α : Type u_1} {β : Type u_2} (t : Multiset β) :
0 ×ˢ t = 0
@[simp]
theorem Multiset.cons_product {α : Type u_1} {β : Type u_2} (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 u_2} (s : Multiset α) :
s ×ˢ 0 = 0
@[simp]
theorem Multiset.product_cons {α : Type u_1} {β : Type u_2} (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 u_2} (a : α) (b : β) :
{a} ×ˢ {b} = {(a, b)}
@[simp]
theorem Multiset.add_product {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset α) (u : Multiset β) :
(s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
@[simp]
theorem Multiset.product_add {α : Type u_1} {β : Type u_2} (s : Multiset α) (t : Multiset β) (u : Multiset β) :
s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
@[simp]
theorem Multiset.mem_product {α : Type u_1} {β : Type u_2} {s : Multiset α} {t : Multiset β} {p : α × β} :
p s ×ˢ t p.fst s p.snd t
@[simp]
theorem Multiset.card_product {α : Type u_2} {β : Type u_1} (s : Multiset α) (t : Multiset β) :
Multiset.card (s ×ˢ t) = Multiset.card s * Multiset.card t

Disjoint sum of multisets #

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

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

Equations
@[simp]
theorem Multiset.coe_sigma {α : Type u_1} {σ : αType u_2} (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_2} (t : (a : α) → Multiset (σ a)) :
@[simp]
theorem Multiset.cons_sigma {α : Type u_1} {σ : αType u_2} (a : α) (s : Multiset α) (t : (a : α) → Multiset (σ a)) :
@[simp]
theorem Multiset.sigma_singleton {α : Type u_1} {β : Type u_2} (a : α) (b : αβ) :
(Multiset.sigma {a} fun a => {b a}) = {{ fst := a, snd := b a }}
@[simp]
theorem Multiset.add_sigma {α : Type u_1} {σ : αType u_2} (s : Multiset α) (t : Multiset α) (u : (a : α) → Multiset (σ a)) :
@[simp]
theorem Multiset.sigma_add {α : Type u_2} {σ : αType u_1} (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.mem_sigma {α : Type u_1} {σ : αType u_2} {s : Multiset α} {t : (a : α) → Multiset (σ a)} {p : (a : α) × σ a} :
p Multiset.sigma s t p.fst s p.snd t p.fst
@[simp]
theorem Multiset.card_sigma {α : Type u_1} {σ : αType u_2} (s : Multiset α) (t : (a : α) → Multiset (σ a)) :
Multiset.card (Multiset.sigma s t) = Multiset.sum (Multiset.map (fun a => Multiset.card (t a)) s)