Order Generating Subset Includes Completely Irreducible Elements
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be an ordered set.
Let $X \subseteq S$ be an order generating subset of $S$.
Let $x \in S$ be a completely irreducible element of $S$.
Then $x \in X$.
Proof
By definition of order generating:
- $x^\succeq \cap X$ admits an infimum and $x = \map \inf {x^\succeq \cap X}$
By Completely Irreducible and Subset Admits Infimum Equals Element implies Element Belongs to Subset:
- $x \in x^\succeq \cap X$
Thus by definition of intersection:
- $x \in X$
$\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 WAYBEL16:25