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) |
