Projection of a product-generic filter

ID: projection-of-a-product-generic-filter

For a generic filter in product forcing, let be its coordinate projections. They are filters in an ordered set. Given and , choose separate pairs witnessing their membership and then a common strengthening in . Upward closure puts in , 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.

New to topics? Read the docs here!