Strictly Precede and Step Condition and not Precede implies Joins are equal
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
- Mizar article WAYBEL16:27