# Preceding iff Join equals Larger Operand

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

- Mizar article YELLOW_0:24