Ultrafilter selection from a partition-rich family (source code)

= Ultrafilter selection from a partition-rich family

Let $S$ be a nonempty <set> and $\mathscr P\subseteq\mathcal P(S)$ be upward closed. An <ultrafilter> all of whose members lie in $\mathscr P$ exists exactly when every finite <set partition> of $S$ has a cell in $\mathscr P$. For sufficiency, the complements of sets outside $\mathscr P$ have the <finite intersection property>: a finite cover by such sets could be disjointified into a partition with no cell in $\mathscr P$. The <ultrafilter lemma> extends the generated proper <filter>. Necessity follows because an <ultrafilter> selects exactly one cell of every finite partition. This criterion requires partition richness of the whole ground set; it does not assert that the complement family is closed under unions.