Way Below Closure is Ideal in Bounded Below Join Semilattice

Theorem

Let $L = \struct {S, \vee, \preceq}$ be a bounded below join semilattice.

Let $x \in S$.

Then

$x^\ll$ is ideal in $L$.

Proof

By Way Below Closure is Directed in Bounded Below Join Semilattice:

$x^\ll$ is a non-empty directed set.

Let $y \in x^\ll, z \in S$ such that

$z \preceq y$

By definition of way below closure:

$y \ll x$

By definition of reflexivity:

$x \preceq x$

By Preceding and Way Below implies Way Below:

$z \ll x$

Thus by definition of way below closure:

$z \in x^\ll$

Thus by definition

$x^\ll$ is a lower section.

Thus by definition

$x^\ll$ is an ideal in $L$.

$\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_3:funcreg 1
• Mizar article WAYBEL_3:funcreg 2
• Mizar article WAYBEL_3:funcreg 4