Singleton is Directed and Filtered Subset
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \precsim}$ be a preordered set.
Let $x$ be an element of $S$.
Then $\set x$ is directed and filtered subset of $S$.
Proof
Let $y, z \in \set x$.
By definition of singleton:
- $ y = x \land z = x$
By definition of reflexivity:
- $y \precsim x \land z \precsim x$
Thus:
- $\exists h \in \set x: y \precsim h \land z \precsim h$
Thus by definition:
- $\set x$ is a directed subset of $S$.
$\set x$ is a filtered subset of $S$ by mutatis mutandis.
$\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:5