Lower Closure of Directed Subset is Ideal
Jump to navigation
Jump to search
Theorem
Let $\mathscr S = \struct {S, \preceq}$ be an ordered set.
Let $D$ be a directed subset of $S$.
Then
- $D^\preceq$ is an ideal in $\mathscr S$
where $D^\preceq$ denotes the lower closure of $D$.
Proof
By Directed iff Lower Closure Directed:
- $D^\preceq$ is directed.
By Lower Closure is Lower Section:
- $D^\preceq$ is a lower section.
Thus by definition
- $D^\preceq$ is an ideal in $\mathscr S$
$\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 10
- Mizar article WAYBEL_0:funcreg 15