Result on D467: Injective map
Identity map is injection
Formulation 0
Let $X$ be a D11: Set.
Let $I : X \to Y$ be an D440: Identity map on $X$.
Then $I$ is a D467: Injective map.
Proofs
Proof 0
Let $X$ be a D11: Set.
Let $I : X \to Y$ be an D440: Identity map on $X$.
If $x, y \in X$ are such $I$ maps them on to the same value, then \begin{equation} x = I(x) = I(y) = y \end{equation} which establishes injectivity of $I$. $\square$