\begin{definition}[Definition:Injection/Definition 1 a]
A mapping $f$ is '''an injection''', or '''injective''' {{iff}}:
:$\forall x_1, x_2 \in \Dom f: x_1 \ne x_2 \implies \map f {x_1} \ne \map f {x_2}$
That is, distinct elements of the domain are mapped to distinct elements of the codomain.
\end{definition}