Upper Bounds are Equivalent implies Suprema are equal
Jump to navigation
Jump to search
Theorem
Let $L = \struct {S, \preceq}$ be an ordered set.
Let $X, Y$ be subsets of $S$.
Assume that
- $X$ admits a supremum
and
- $\forall x \in S: x$ is upper bound for $X \iff x$ is upper bound for $Y$
Then $\sup X = \sup Y$
Proof
We will prove that
- $\forall b \in S: b$ is upper bound for $Y \implies \sup X \preceq b$
Let $b \in S$ such that
- $b$ is upper bound for $Y$.
By assumption:
- $b$ is upper bound for $X$.
Thus by definition of supremum:
- $\sup X \preceq b$
$\Box$
By definition of supremum:
- $\sup X$ is upper bound for $X$.
By assumption:
- $\sup X$ is upper bound for $Y$.
Thus by definition of supremum:
- $\sup X = \sup Y$
$\blacksquare$
Sources
- Mizar article YELLOW_0:47