DEF-INJ. Injection.
An injection / one-to-one function is a function that is injective, i.e. a function $f$ such that
\[\forall x,y\in\operatorname{dom}f :\enspace f(x)=f(y) \enspace\Rightarrow\enspace x=y.\]
PROP-INJ-EMP.
$\varnothing$ is an injection.