Dense subset of a forcing order (source code)

= Dense subset of a forcing order
{wiki=Dense_set}

A subset $D$ of a forcing order $\mathbb P$ is dense when every $p\in\mathbb P$ has a stronger extension $q\leq p$ in $D$.