Set of Meet Irreducible Elements Excluded Top is Order Generating

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