Preceding iff Join equals Larger Operand

From ProofWiki
Jump to navigation Jump to search

Theorem

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

Let $x, y \in S$.

Then

$x \preceq y$ if and only if $x \vee y = y$


Proof

Sufficient Condition

Let

$x \preceq y$

By definition of join:

$x \vee y = \sup \left\{ {x, y}\right\}$

By definitions of upper bound and reflexivity:

$y$ is upper bound for $\left\{ {x, y}\right\}$

and

$\forall z \in S: z$ is upper bound for $\left\{ {x, y}\right\} \implies y \preceq z$

Thus by definition of supremum:

$y = \sup \left\{ {x, y}\right\} = x \vee y$

$\Box$

Necessary Condition

Let

$x \vee y = y$

Thus by Join Succeeds Operands:

$x \preceq y$

$\blacksquare$


Sources