Proper filter (source code)

= Proper filter
{title2=$\varnothing\notin\mathcal F$}

A <proper filter> is an upward-closed family of <subsets> <closed> under finite <intersections> and excluding the <empty set>. This excludes the improper family of all <subsets>. An <ultrafilter> is a maximal <proper filter>.