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 #
Bind #
@[simp]
@[simp]
theorem
Multiset.dedup_bind_dedup
{α : Type u_1}
{β : Type v}
[DecidableEq α]
[DecidableEq β]
(s : Multiset α)
(f : α → Multiset β)
:
Product of two multisets #
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
Instances For
@[simp]