Fubini product of ultrafilters (source code)

= Fubini product of ultrafilters
{c}
{title2=$\mathcal U\otimes\mathcal V$}

For <ultrafilters> $\mathcal U$ on $I$ and $\mathcal V$ on $J$, put
$$
A\in\mathcal U\otimes\mathcal V\quad\Longleftrightarrow\quad\{i\in I:\{j\in J:(i,j)\in A\}\in\mathcal V\}\in\mathcal U.
$$
This is an <ultrafilter> on $I\times J$: upward closure and finite intersection follow at both levels, and the <ultrafilter> dichotomy follows by complementing at both levels. Iterating gives ordered finite products. Projection onto a subsequence of coordinates pushes this product to the product on that subsequence, since omitted coordinates are absent from the tested <first-order formula>. The order of coordinates matters; these products need not be symmetric.