Joint injectivity of a pair of functions (source code)

= Joint injectivity of a pair of functions
{title2=$f_1(y)=f_1(z),\ f_2(y)=f_2(z)\Rightarrow y=z$}

The <pairing map to a Cartesian product> is <injective> exactly when its coordinate <functions> are jointly injective in the displayed sense. Either coordinate being <injective> is sufficient, but neither need be <injective> individually. For example, pairing three points with $(0,0),(0,1),(1,0)$ distinguishes all points even though each coordinate separately identifies two of them.