mathlib3 documentation

data.multiset.bind

Bind operation for multisets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

Join #

source
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
source
theorem multiset.coe_join {α : Type u_1} (L : list (list α)) :
↑(list.map coe L).join = ↑(L.join)
source
@[simp]
theorem multiset.join_zero {α : Type u_1} :
0.join = 0
source
@[simp]
theorem multiset.join_cons {α : Type u_1} (s : multiset α) (S : multiset (multiset α)) :
(s ::ₘ S).join = s + S.join
source
@[simp]
theorem multiset.join_add {α : Type u_1} (S T : multiset (multiset α)) :
(S + T).join = S.join + T.join
source
@[simp]
theorem multiset.singleton_join {α : Type u_1} (a : multiset α) :
{a}.join = a
source
@[simp]
theorem multiset.mem_join {α : Type u_1} {a : α} {S : multiset (multiset α)} :
a ∈ S.join ↔ ∃ (s : multiset α) (H : s ∈ S), a ∈ s
source
@[simp]
theorem multiset.card_join {α : Type u_1} (S : multiset (multiset α)) :
⇑multiset.card S.join = (multiset.map ⇑multiset.card S).sum
source
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) :
multiset.rel r s.join t.join

Bind #

source
def multiset.bind {α : Type u_1} {β : Type u_2} (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
source
@[simp]
theorem multiset.coe_bind {α : Type u_1} {β : Type u_2} (l : list α) (f : α → list β) :
↑l.bind (λ (a : α), ↑(f a)) = ↑(l.bind f)
source
@[simp]
theorem multiset.zero_bind {α : Type u_1} {β : Type u_2} (f : α → multiset β) :
0.bind f = 0
source
@[simp]
theorem multiset.cons_bind {α : Type u_1} {β : Type u_2} (a : α) (s : multiset α) (f : α → multiset β) :
(a ::ₘ s).bind f = f a + s.bind f
source
@[simp]
theorem multiset.singleton_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α → multiset β) :
{a}.bind f = f a
source
@[simp]
theorem multiset.add_bind {α : Type u_1} {β : Type u_2} (s t : multiset α) (f : α → multiset β) :
(s + t).bind f = s.bind f + t.bind f
source
@[simp]
theorem multiset.bind_zero {α : Type u_1} {β : Type u_2} (s : multiset α) :
s.bind (λ (a : α), 0) = 0
source
@[simp]
theorem multiset.bind_add {α : Type u_1} {β : Type u_2} (s : multiset α) (f g : α → multiset β) :
s.bind (λ (a : α), f a + g a) = s.bind f + s.bind g
source
@[simp]
theorem multiset.bind_cons {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → β) (g : α → multiset β) :
s.bind (λ (a : α), f a ::ₘ g a) = multiset.map f s + s.bind g
source
@[simp]
theorem multiset.bind_singleton {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → β) :
s.bind (λ (x : α), {f x}) = multiset.map f s
source
@[simp]
theorem multiset.mem_bind {α : Type u_1} {β : Type u_2} {b : β} {s : multiset α} {f : α → multiset β} :
b ∈ s.bind f ↔ ∃ (a : α) (H : a ∈ s), b ∈ f a
source
@[simp]
theorem multiset.card_bind {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → multiset β) :
⇑multiset.card (s.bind f) = (multiset.map (⇑multiset.card ∘ f) s).sum
source
theorem multiset.bind_congr {α : Type u_1} {β : Type u_2} {f g : α → multiset β} {m : multiset α} :
(∀ (a : α), a ∈ m → f a = g a) → m.bind f = m.bind g
source
theorem multiset.bind_hcongr {α : Type u_1} {β β' : Type u_2} {m : multiset α} {f : α → multiset β} {f' : α → multiset β'} (h : β = β') (hf : ∀ (a : α), a ∈ m → f a == f' a) :
m.bind f == m.bind f'
source
theorem multiset.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : α → multiset β) (f : β → γ) :
multiset.map f (m.bind n) = m.bind (λ (a : α), multiset.map f (n a))
source
theorem multiset.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : β → multiset γ) (f : α → β) :
(multiset.map f m).bind n = m.bind (λ (a : α), n (f a))
source
theorem multiset.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : multiset α} {f : α → multiset β} {g : β → multiset γ} :
(s.bind f).bind g = s.bind (λ (a : α), (f a).bind g)
source
theorem multiset.bind_bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : multiset β) {f : α → β → multiset γ} :
m.bind (λ (a : α), n.bind (λ (b : β), f a b)) = n.bind (λ (b : β), m.bind (λ (a : α), f a b))
source
theorem multiset.bind_map_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : multiset α) (n : multiset β) {f : α → β → γ} :
m.bind (λ (a : α), multiset.map (λ (b : β), f a b) n) = n.bind (λ (b : β), multiset.map (λ (a : α), f a b) m)
source
@[simp]
theorem multiset.prod_bind {α : Type u_1} {β : Type u_2} [comm_monoid β] (s : multiset α) (t : α → multiset β) :
(s.bind t).prod = (multiset.map (λ (a : α), (t a).prod) s).prod
source
@[simp]
theorem multiset.sum_bind {α : Type u_1} {β : Type u_2} [add_comm_monoid β] (s : multiset α) (t : α → multiset β) :
(s.bind t).sum = (multiset.map (λ (a : α), (t a).sum) s).sum
source
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) :
multiset.rel p (s.bind f) (t.bind g)
source
theorem multiset.count_sum {α : Type u_1} {β : Type u_2} [decidable_eq α] {m : multiset β} {f : β → multiset α} {a : α} :
multiset.count a (multiset.map f m).sum = (multiset.map (λ (b : β), multiset.count a (f b)) m).sum
source
theorem multiset.count_bind {α : Type u_1} {β : Type u_2} [decidable_eq α] {m : multiset β} {f : β → multiset α} {a : α} :
multiset.count a (m.bind f) = (multiset.map (λ (b : β), multiset.count a (f b)) m).sum
source
theorem multiset.le_bind {α : Type u_1} {β : Type u_2} {f : α → multiset β} (S : multiset α) {x : α} (hx : x ∈ S) :
f x ≤ S.bind f
source
@[simp]
theorem multiset.attach_bind_coe {α : Type u_1} {β : Type u_2} (s : multiset α) (f : α → multiset β) :
s.attach.bind (λ (i : {x // x ∈ s}), f ↑i) = s.bind f

Product of two multisets #

source
def multiset.product {α : Type u_1} {β : Type u_2} (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
source
@[simp]
theorem multiset.coe_product {α : Type u_1} {β : Type u_2} (l₁ : list α) (l₂ : list β) :
↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)
source
@[simp]
theorem multiset.zero_product {α : Type u_1} {β : Type u_2} (t : multiset β) :
0 ×ˢ t = 0
source
@[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
source
@[simp]
theorem multiset.product_zero {α : Type u_1} {β : Type u_2} (s : multiset α) :
s ×ˢ 0 = 0
source
@[simp]
theorem multiset.product_cons {α : Type u_1} {β : Type u_2} (b : β) (s : multiset α) (t : multiset β) :
s ×ˢ (b ::ₘ t) = multiset.map (λ (a : α), (a, b)) s + s ×ˢ t
source
@[simp]
theorem multiset.product_singleton {α : Type u_1} {β : Type u_2} (a : α) (b : β) :
{a} ×ˢ {b} = {(a, b)}
source
@[simp]
theorem multiset.add_product {α : Type u_1} {β : Type u_2} (s t : multiset α) (u : multiset β) :
(s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
source
@[simp]
theorem multiset.product_add {α : Type u_1} {β : Type u_2} (s : multiset α) (t u : multiset β) :
s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
source
@[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
source
@[simp]
theorem multiset.card_product {α : Type u_1} {β : Type u_2} (s : multiset α) (t : multiset β) :
⇑multiset.card (s ×ˢ t) = ⇑multiset.card s * ⇑multiset.card t

Disjoint sum of multisets #

source
@[protected]
def multiset.sigma {α : Type u_1} {σ : α → Type u_5} (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
source
@[simp]
theorem multiset.coe_sigma {α : Type u_1} {σ : α → Type u_5} (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :
↑l₁.sigma (λ (a : α), ↑(l₂ a)) = ↑(l₁.sigma l₂)
source
@[simp]
theorem multiset.zero_sigma {α : Type u_1} {σ : α → Type u_5} (t : Π (a : α), multiset (σ a)) :
0.sigma t = 0
source
@[simp]
theorem multiset.cons_sigma {α : Type u_1} {σ : α → Type u_5} (a : α) (s : multiset α) (t : Π (a : α), multiset (σ a)) :
(a ::ₘ s).sigma t = multiset.map (sigma.mk a) (t a) + s.sigma t
source
@[simp]
theorem multiset.sigma_singleton {α : Type u_1} {β : Type u_2} (a : α) (b : α → β) :
{a}.sigma (λ (a : α), {b a}) = {⟨a, b a⟩}
source
@[simp]
theorem multiset.add_sigma {α : Type u_1} {σ : α → Type u_5} (s t : multiset α) (u : Π (a : α), multiset (σ a)) :
(s + t).sigma u = s.sigma u + t.sigma u
source
@[simp]
theorem multiset.sigma_add {α : Type u_1} {σ : α → Type u_5} (s : multiset α) (t u : Π (a : α), multiset (σ a)) :
s.sigma (λ (a : α), t a + u a) = s.sigma t + s.sigma u
source
@[simp]
theorem multiset.mem_sigma {α : Type u_1} {σ : α → Type u_5} {s : multiset α} {t : Π (a : α), multiset (σ a)} {p : Σ (a : α), σ a} :
p ∈ s.sigma t ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst
source
@[simp]
theorem multiset.card_sigma {α : Type u_1} {σ : α → Type u_5} (s : multiset α) (t : Π (a : α), multiset (σ a)) :
⇑multiset.card (s.sigma t) = (multiset.map (λ (a : α), ⇑multiset.card (t a)) s).sum