Filter in an ordered set
= Filter in an ordered set
{title2=$G\subseteq P$}
= Filters in an ordered set
{synonym}
A filter is a nonempty upward-closed <subset> $G$ of a <partial order> such that every two members have a common lower bound in $G$. With <standard notation for forcing>, lower means stronger, so these are exactly the directed filters used to define a <generic filter>. The <projection of a product-generic filter> uses these properties before genericity of its factor filters is proved.