Strictly Precede and Step Condition and not Precede implies Joins are equal

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S, \vee, \preceq}$ be a join semilattice.

Let $p, q, u \in S$ be such that:

$p \prec q$ and $\paren {\forall s \in S: p \prec s \implies q \preceq s}$ and $u \npreceq p$


Then:

$p \vee u = q \vee u$


Proof

From the definition of join, it is required to prove that:

$\forall s \in S: p \preceq s \land u \preceq s \implies q \vee u \preceq s$


Let $s \in S$ be such that:

$p \preceq s$ and $u \preceq s$

We have:

$p \ne s$

By definition of strictly precede:

$p \prec s$

By assumption:

$q \preceq s$

Thus by definition of the join $q \vee u$:

$q \vee u \preceq s$

and hence, as desired:

$q \vee u = p \vee u$

$\blacksquare$


Sources