Preceding implies if Less Upper Bound then Greater Upper Bound
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
- $x \preceq y$
Let $X \subseteq S$.
Then
- $x$ is upper bound for $X \implies y$ is upper bound for $X$
and
- $y$ is lower bound for $X \implies x$ is lower bound for $X$.
Proof
First Implication
Let $x$ be upper bound for $X$,
Let $z \in X$.
By definition of upper bound:
- $z \preceq x$
Thus by definition of transitivity:
- $z \preceq y$
$\Box$
Second Implication
This follows by mutatis mutandis.
$\blacksquare$
Sources
- Mizar article YELLOW_0:4