Set of symbols
Deduction system
Zermelo-Fraenkel set theory
Binary cartesian set product
Binary relation
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}
Dual definition
» Surjective map
Also known as
Injection, Set monomorphism
Child definitions
» D2222: Set of injections
» R399: Injectivity is hereditary
» R2767: Identity map is an injection
» R3919: Probability measure need not be an injection
» R4055: Singleton map is injection from set to power set
» R301: Canonical identity map is an injection
» R5077: Injection from the natural number plane to the set of natural numbers