ThmDex – An index of mathematical definitions, results, and conjectures.

Formulation F1569 on D2901: Multiset

F1569

Formulation 0

An D548: Ordered pair $M = (X, f)$ is a multiset if and only if

(1)	$X$ is a D11: Set
(2)	\begin{equation} f : X \to \mathbb{N} \cup \{ \infty \} \end{equation}