Upper Closure of Element is Filter

Theorem

Let $\struct {S, \preceq}$ be an ordered set.

Let $s$ be an element of $S$.

Then:

$s^\succeq$ is a filter in $\struct {S, \preceq}$

where $s^\succeq$ denotes the upper closure of $s$.

Proof

By Singleton is Directed and Filtered Subset

$\set s$ is a filtered subset of $S$

By Filtered iff Upper Closure Filtered:

$\set s^\succeq$ is a filtered subset of $S$

By Upper Closure is Upper Section:

$\set s^\succeq$ is a upper section in $S$

By Upper Closure of Singleton

$\set s^\succeq = s^\succeq$

By definition of reflexivity:

$s \preceq s$

By definition of upper closure of element:

$s \in s^\succeq$

Thus by definition:

$s^\succeq$ is non-empty, filtered and upper.

Thus by definition:

$s^\succeq$ is a filter in $\struct {S, \preceq}$

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL_0:funcreg 9
• Mizar article WAYBEL_0:funcreg 13