Filter (mathematics) (source code)

= Filter
{disambiguate=mathematics}
{title2=$G\subseteq P$}
{wiki}

= Filter in an ordered set
{synonym}

= 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.