Principal filter in an ordered set (source code)

= Principal filter in an ordered set
{title2=$\uparrow p=\{q:p\leq q\}$}

= Principal filter
{synonym}

The principal <filter in an ordered set> generated by $p$ contains exactly the elements above $p$. It is upward closed, and $p$ is a common lower bound in the filter for any two of its members. With <standard notation for forcing>, these are the conditions weaker than $p$. The principal filter need not be a <generic filter>: a dense <set> can require a strict strengthening. The compatible-condition filter in <a forcing atom determines a ground-model generic filter> includes strengthenings as well as weakenings and can therefore be strictly larger.