Projection of a product-generic filter (source code)

= Projection of a product-generic filter
{title2=$H=G_0\times G_1$}

For a <generic filter> $H$ in <product forcing>, let $G_0,G_1$ be its coordinate projections. They are <filters in an ordered set>. Given $p\in G_0$ and $q\in G_1$, choose separate pairs witnessing their membership and then a common strengthening in $H$. Upward closure puts $(p,q)$ in $H$, proving the displayed equality. Every ground-model dense factor <set> lifts to a dense product <set>, proving genericity of each projection over the ground model.