Definition:Ultrafilter (Order Theory)
Jump to navigation
Jump to search
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