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

• Eq Multiset.join Multiset.sum

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

theorem Multiset.join_zero {α : Type u_1} : Eq (join 0) 0

theorem Multiset.join_cons {α : Type u_1} (s : Multiset α) (S : Multiset (Multiset α)) : Eq (cons s S).join (HAdd.hAdd s S.join)

theorem Multiset.join_add {α : Type u_1} (S T : Multiset (Multiset α)) : Eq (HAdd.hAdd S T).join (HAdd.hAdd S.join T.join)

theorem Multiset.singleton_join {α : Type u_1} (a : Multiset α) : Eq (Singleton.singleton a).join a

theorem Multiset.mem_join {α : Type u_1} {a : α} {S : Multiset (Multiset α)} : Iff (Membership.mem S.join a) (Exists fun (s : Multiset α) => And (Membership.mem S s) (Membership.mem s a))

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

theorem Multiset.map_join {α : Type u_1} {β : Type v} (f : α → β) (S : Multiset (Multiset α)) : Eq (map f S.join) (map (map f) S).join

theorem Multiset.prod_join {α : Type u_1} [CommMonoid α] {S : Multiset (Multiset α)} : Eq S.join.prod (map prod S).prod

theorem Multiset.sum_join {α : Type u_1} [AddCommMonoid α] {S : Multiset (Multiset α)} : Eq S.join.sum (map sum S).sum

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

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

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

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

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

theorem Multiset.cons_bind {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (f : α → Multiset β) : Eq ((cons a s).bind f) (HAdd.hAdd (f a) (s.bind f))

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

theorem Multiset.add_bind {α : Type u_1} {β : Type v} (s t : Multiset α) (f : α → Multiset β) : Eq ((HAdd.hAdd s t).bind f) (HAdd.hAdd (s.bind f) (t.bind f))

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

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

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

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

theorem Multiset.mem_bind {α : Type u_1} {β : Type v} {b : β} {s : Multiset α} {f : α → Multiset β} : Iff (Membership.mem (s.bind f) b) (Exists fun (a : α) => And (Membership.mem s a) (Membership.mem (f a) b))

theorem Multiset.card_bind {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) : Eq (s.bind f).card (map (Function.comp card f) s).sum

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

theorem Multiset.bind_hcongr {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'} (h : Eq β β') (hf : ∀ (a : α), Membership.mem m a → 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 : Multiset α) (n : α → Multiset β) (f : β → γ) : Eq (map f (m.bind n)) (m.bind fun (a : α) => map f (n a))

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

theorem Multiset.bind_assoc {α : Type u_1} {β : Type v} {γ : Type u_2} {s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ} : Eq ((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 : Multiset α) (n : Multiset β) {f : α → β → Multiset γ} : Eq (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 : Multiset α) (n : Multiset β) {f : α → β → γ} : Eq (m.bind fun (a : α) => map (fun (b : β) => f a b) n) (n.bind fun (b : β) => map (fun (a : α) => f a b) m)

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

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

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 : Relator.LiftFun r (Rel p) f g) (hst : Rel r s t) : Rel p (s.bind f) (t.bind g)

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

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

theorem Multiset.le_bind {α : Type u_4} {β : Type u_5} {f : α → Multiset β} (S : Multiset α) {x : α} (hx : Membership.mem S x) : LE.le (f x) (S.bind f)

theorem Multiset.attach_bind_coe {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → Multiset β) : Eq (s.attach.bind fun (i : Subtype fun (x : α) => Membership.mem s x) => f i.val) (s.bind f)

theorem Multiset.nodup_bind {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → Multiset β} : Iff (s.bind f).Nodup (And (∀ (a : α), Membership.mem s a → (f a).Nodup) (Pairwise (Function.onFun Disjoint f) s))

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

theorem Multiset.fold_bind {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) : Eq (fold op (fold op b₀ (map b s)) (s.bind t)) (fold op b₀ (map (fun (i : ι) => fold op (b i) (t i)) s))

Product of two multisets

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

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

Equations

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

def Multiset.instSProd {α : Type u_1} {β : Type v} : SProd (Multiset α) (Multiset β) (Multiset (Prod α β))

Equations

• Eq Multiset.instSProd { sprod := Multiset.product }

theorem Multiset.coe_product {α : Type u_1} {β : Type v} (l₁ : List α) (l₂ : List β) : Eq (SProd.sprod (ofList l₁) (ofList l₂)) (ofList (SProd.sprod l₁ l₂))

theorem Multiset.zero_product {α : Type u_1} {β : Type v} (t : Multiset β) : Eq (SProd.sprod 0 t) 0

theorem Multiset.cons_product {α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (t : Multiset β) : Eq (SProd.sprod (cons a s) t) (HAdd.hAdd (map (Prod.mk a) t) (SProd.sprod s t))

theorem Multiset.product_zero {α : Type u_1} {β : Type v} (s : Multiset α) : Eq (SProd.sprod s 0) 0

theorem Multiset.product_cons {α : Type u_1} {β : Type v} (b : β) (s : Multiset α) (t : Multiset β) : Eq (SProd.sprod s (cons b t)) (HAdd.hAdd (map (fun (a : α) => { fst := a, snd := b }) s) (SProd.sprod s t))

theorem Multiset.product_singleton {α : Type u_1} {β : Type v} (a : α) (b : β) : Eq (SProd.sprod (Singleton.singleton a) (Singleton.singleton b)) (Singleton.singleton { fst := a, snd := b })

theorem Multiset.add_product {α : Type u_1} {β : Type v} (s t : Multiset α) (u : Multiset β) : Eq (SProd.sprod (HAdd.hAdd s t) u) (HAdd.hAdd (SProd.sprod s u) (SProd.sprod t u))

theorem Multiset.product_add {α : Type u_1} {β : Type v} (s : Multiset α) (t u : Multiset β) : Eq (SProd.sprod s (HAdd.hAdd t u)) (HAdd.hAdd (SProd.sprod s t) (SProd.sprod s u))

theorem Multiset.card_product {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) : Eq (SProd.sprod s t).card (HMul.hMul s.card t.card)

theorem Multiset.mem_product {α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} {p : Prod α β} : Iff (Membership.mem (s.product t) p) (And (Membership.mem s p.fst) (Membership.mem t p.snd))

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

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

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

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

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

theorem Multiset.cons_sigma {α : Type u_1} {σ : α → Type u_4} (a : α) (s : Multiset α) (t : (a : α) → Multiset (σ a)) : Eq ((cons a s).sigma t) (HAdd.hAdd (map (Sigma.mk a) (t a)) (s.sigma t))

theorem Multiset.sigma_singleton {α : Type u_1} {β : Type v} (a : α) (b : α → β) : Eq ((Singleton.singleton a).sigma fun (a : α) => Singleton.singleton (b a)) (Singleton.singleton ⟨a, b a⟩)

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

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

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

theorem Multiset.mem_sigma {α : Type u_1} {σ : α → Type u_4} {s : Multiset α} {t : (a : α) → Multiset (σ a)} {p : (a : α) × σ a} : Iff (Membership.mem (s.sigma t) p) (And (Membership.mem s p.fst) (Membership.mem (t p.fst) p.snd))

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