\begin{definition}[Definition:Multiset]
A '''multiset''' is a pair $\struct {S, \mu}$ where:
:$S$ is a set
:$\mu: S \to \N_{>0}$ is a mapping to the strictly positive natural numbers
For $s \in S$ the natural number $\map \mu s$ is called the '''multiplicity''' of $s$.
Note that the '''multiplicities''' of elements is finite: we do not allow infinitely many occurrences of the same element, though the set $S$ itself may be finite, countably infinite or uncountably infinite.
\end{definition}