Definition:Ultrafilter (Order Theory)

Definition

Let $O = \left({S, \preceq}\right)$ be an ordered set.

Let $F$ be a filter in $O$.

Then $F$ is ultrafilter (on $O$) if and only if

$F$ is proper subset of $S$ and

for all filter $G$ in $O$: $\left({F \subseteq G \implies F = G \lor G = S}\right)$

Sources

• Mizar article WAYBEL_7:def 3