Empty-set cases for Cartesian projections (source code)

= Empty-set cases for Cartesian projections
{title2=$p_i:X_1\times X_2\to X_i$}

For a coordinate <projection map> onto $X_i$, write $X_j$ for the other factor. The map is <surjective> exactly when $X_i$ is empty or $X_j$ is nonempty. It is <injective> exactly when $X_i$ is empty or $X_j$ has at most one element. In particular, a <surjection> onto an empty <Cartesian product> need not induce a <surjection> onto a nonempty factor.