Dense subset of a forcing order

A subset $D$ of a forcing order $P$ is dense if every $p\in P$ has a stronger condition $q\le p$ in $D$. This order-density condition is the one used by a generic filter; it is distinct from density in an arbitrarily specified topology.

For the convention that larger conditions are stronger, density above $p$ means every strengthening of $p$ has a further strengthening in $D$. It is the extension-cone density usually called dense below a forcing condition when smaller conditions are stronger. The sign must be translated with the order convention, rather than copied unchanged.

A set $D\subseteq \mathbb{P}$ is dense below $p$ when every $q\le p$ has an extension $r\le q$ belonging to $D$.

If $p\in G$ and a ground-model set $D$ is dense below a forcing condition $p$, then the generic filter $G$ meets $D$. Add all incompatible forcing conditions with $p$ to $D$. The enlarged set is globally dense: a condition compatible with $p$ first has a common strengthening, then a further strengthening in $D$. Genericity meets the enlargement, and directedness excludes its incompatible part.