Lattice filter

A lattice filter is a nonempty upward-closed subset closed under finite meets. A proper filter omits the bottom element.

A lattice filter is a filter in an ordered set when that order is a lattice; directedness and upward closure then imply closure under finite meets.

A prime filter is a proper lattice filter $P$ such that $a\vee b\in P$ implies $a\in P$ or $b\in P$.

If a lattice filter $F$ and lattice ideal $I$ in a distributive lattice are disjoint, there is a prime filter of a distributive lattice containing $F$ and disjoint from $I$.

The Boolean prime ideal theorem is the Boolean-algebra version; distributivity gives this corresponding filter-extension statement.