Finite repetition-free sequence (source code)

= Finite repetition-free sequence
{title2=$\operatorname{Inj}({<}\omega,X)$}

= Finite injective sequence
{synonym}

A <finite repetition-free sequence> in a <set> $X$ is an <injective function> from an initial segment $\{0,\ldots,k-1\}$ of the <natural numbers> into $X$, including the empty <sequence> for $k=0$. For a <finite set> of size $m$, the number of these <sequences> is
$$
\sum_{k=0}^m\frac{m!}{(m-k)!}.
$$
The order of each list is part of the data, so it can be enumerated without choosing an order on its underlying support.