Way Below Closure is Lower Section

Theorem

Let $L = \struct {S, \vee, \preceq}$ be an ordered set.

Let $x \in S$.

Then

$x^\ll$ is a lower section.

Proof

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.

$\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 2