ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Deduction system
Zermelo-Fraenkel set theory
Binary cartesian set product
Binary relation
Definition D467
Injective map
Formulation 0
A D1104: Binary relation structure $M = (X \times Y, f)$ is an injective map
(1) \begin{equation} \forall \, x \in X : \forall \, y, y' \in Y \left( (x, y), (x, y') \in f \quad \implies \quad y = y' \right) \end{equation} (D358: Right-unique binary relation)
(2) \begin{equation} \forall \, x \in X : \exists \, y \in Y : (x, y) \in f \end{equation} (D359: Left-total binary relation)
(3) \begin{equation} \forall \, x, x' \in X : \forall \, y \in Y \left( (x, y), (x', y) \in f \quad \implies \quad x = x' \right) \end{equation} (D357: Left-unique binary relation)
Formulation 1
A D18: Map $f : X \to Y$ is injective if and only if \begin{equation} \forall \, x, y \in X \left( f(x) = f(y) \quad \implies \quad x = y \right) \end{equation}
Set of injections
Canonical identity map is an injection
Identity map is an injection
Injectivity is hereditary
Singleton map is injection from set to power set