Way Below is Congruent for Join

Theorem

Let $L = \left({S, \vee, \preceq}\right)$ be a join semilattice.

Then $\ll$ is congruence relation for $\vee$:

$\forall a, b, x, y \in S: a \ll x \land b \ll y \implies a \vee b \ll x \vee y$

where $\ll$ denotes the way below relation.

Proof

Let $a, b, x, y \in S$ such that $a \ll x$ and $b \ll y$

By Join Succeeds Operands:

$x \preceq x \vee y$ and $y \preceq x \vee y$

By Preceding and Way Below implies Way Below and definition of reflexivity:

$a \ll x \vee y$ and $b \ll x \vee y$

Thus by Join is Way Below if Operands are Way Below:

$a \vee b \ll x \vee 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_3:3