Cartesian product ($X\times Y$)

The Cartesian product $X\times Y$ is the set of ordered pairs $(x,y)$ with $x\in X$ and $y\in Y$.

Given functions $f_i:Y\to X_i$, there is a unique function $g:Y\to X_1\times X_2$ whose coordinate projection maps are $f_1,f_2$. It is the displayed pointwise pairing. Equality of ordered pairs is equality of both coordinates, which proves uniqueness and makes the Cartesian product a categorical product in the Category of sets.

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.

A finite tuple is an ordered list of finitely many entries; coordinates can repeat, and their positions matter. A tuple of length $n$ from a set $M$ is an element of the Cartesian product $M^n$. The empty tuple has length zero. Finite tuples support Scott formulas in a back-and-forth method construction, where matching tuples determine a partial isomorphism of structures.