ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F3750 on D18: Map
F3750
Formulation 0
A D4: Binary relation $M = (X \times Y, f)$ is a map if and only if
(1) $\forall \, x \in X : \forall \, y, y' \in Y \, ((x, y), (x, y') \in f \quad \Rightarrow \quad y = y')$ (D358: Right-unique binary relation)
(2) $\forall \, x \in X : \exists \, y \in Y : (x, y) \in f$ (D359: Left-total binary relation)