Set of Meet Irreducible Elements Excluded Top is Order Generating
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \vee, \wedge, \preceq}$ be a continuous complete lattice.
Let $X = \map {\mathit {IRR} } L \setminus \set \top$
where:
- $\map {\mathit {IRR} } L$ denotes the set of all meet irreducible element of $S$
- $\top$ denotes the top of $L$.
Then $X$ is order generating.
Proof
We will prove that:
- $\forall x, y \in S: \paren {y \npreceq x \implies \exists p \in X: x \preceq p \land y \npreceq p}$
Let $x, y \in S$ such that:
- $y \npreceq x$
By Not Preceding implies There Exists Meet Irreducible Element Not Preceding:
- $\exists p \in S: p$ is meet irreducible and $x \preceq p$ and $y \npreceq p$
By definition of greatest element:
- $p \ne \top$ and $p \in \map {\mathit {IRR} } L$
By definitions of difference and singleton:
- $p \in X$
Thus
- $\exists p \in X: x \preceq p \land y \npreceq p$
$\Box$
Hence by Order Generating iff Not Preceding implies There Exists Element Preceding and Not Preceding:
- $X$ is order generating.
$\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_6:18