Upper Closure of Element is Filter
Jump to navigation
Jump to search
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$
- $\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:
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