\begin{definition}[Definition:Injection/Definition 2]
An '''injection''' is a relation which is both one-to-one and left-total.
Thus, a relation $f$ is an '''injection''' {{iff}}:
:$(1): \quad \forall x \in \Dom f: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f \implies y_1 = y_2$
:$(2): \quad \forall y \in \Img f: \tuple {x_1, y} \in f \land \tuple {x_2, y} \in f \implies x_1 = x_2$
:$(3): \quad \forall s \in S: \exists t \in T: \tuple {s, t} \in \RR$
\end{definition}