Way Below has Strong Interpolation Property

Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.

Let $x, z \in S$ such that

$x \ll z \land x \ne z$

Then

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

Proof

By Way Below is Approximating Relation and Way Below Relation is Auxiliary Relation:

$\ll$ is an auxiliary approximating relation on $S$.

Thus by Auxiliary Approximating Relation has Interpolation Property:

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

$\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:51