Forcing name for the complement of a generic filter (source code)

= Forcing name for the complement of a generic filter

The <forcing name> $\{(\check p,q):p,q\in\mathbb P,\ q\perp p\}$ evaluates to $\mathbb P\setminus G$. If $p\notin G$, genericity applied to $\{q:q\leq p\text{ or }q\perp p\}$ supplies an incompatible member of $G$. If $p\in G$, directedness prevents such a member.