ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map
Definition D467
Injective map

A D1104: Binary relation structure $M = (X \times Y, f)$ is an injective map
 (1) $$\forall \, x \in X : \forall \, y, y' \in Y \left( (x, y), (x, y') \in f \quad \implies \quad y = y' \right)$$ (D358: Right-unique binary relation) (2) $$\forall \, x \in X : \exists \, y \in Y : (x, y) \in f$$ (D359: Left-total binary relation) (3) $$\forall \, x, x' \in X : \forall \, y \in Y \left( (x, y), (x', y) \in f \quad \implies \quad x = x' \right)$$ (D357: Left-unique binary relation)

A D18: Map $f : X \to Y$ is injective if and only if $$\forall \, x, y \in X \left( f(x) = f(y) \quad \implies \quad x = y \right)$$
Children
 ▶ Set of injections
Results
 ▶ Canonical identity map is an injection ▶ Identity map is an injection ▶ Injectivity is hereditary ▶ Singleton map is injection from set to power set