ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F6559 on R2767: Identity map is an injection
F6559
Formulation 0
Let $X$ be a D11: Set such that
(i) $I : X \to Y$ is an D440: Identity map on $X$
Then $I$ is an D467: Injective map.