Way Below has Interpolation Property

Theorem

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.

Let $x, z \in S$ such that

$x \ll z$

Then

$\exists y \in S: x \ll y \land y \ll z$

Proof

Case $x \ne z$:

By Way Below has Strong Interpolation Property:

$\exists y \in S: x \ll y \land y \ll z \land x \ne y$

Thus

$\exists y \in S: x \ll y \land y \ll z$

Case $x = z$:

Define $y = x$

Thus

$x \ll y \land y \ll z$

$\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_4:52