Set of All Completely Irreducible Elements is Smallest Order Generating
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below algebraic lattice.
Then $\map {\operatorname {Irr} } L$ is order generating and
- $\forall X \subseteq S: X$ is order generating $\implies \map {\operatorname {Irr} } L \subseteq X$
where $\map {\operatorname {Irr} } L$ denotes the set of all completely irreducible elements of $L$.
Proof
By Not Preceding implies Exists Completely Irreducible Element in Algebraic Lattice:
- $\forall x, y \in S: y \npreceq x \implies \exists p \in \map {\operatorname {Irr} } L: p \preceq x \land p \npreceq y$
Thus by Order Generating iff Not Preceding implies There Exists Element Preceding and Not Preceding:
- $\map {\operatorname {Irr} } L$ is order generating.
Let $X \subseteq S$ such that
- $X$ is order generating.
Let $x \in \map {\operatorname {Irr} } L$.
By definition of $\operatorname {Irr}$:
- $x$ is completely irreducible.
Thus by Order Generating Subset Includes Completely Irreducible Elements:
- $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:32