Closed Interval of Successor
From ProofWiki
Theorem
Let $\left({S, \circ, \preceq}\right)$ be a naturally ordered semigroup.
Then:
- $\forall m, n \in \left({S, \circ, \preceq}\right): m \preceq n \implies \left[{m \,.\,.\, n \circ 1}\right] = \left[{m \,.\,.\, n}\right] \cup \left\{{n \circ 1}\right\}$
where $\left[{m \,.\,.\, n}\right]$ is the closed interval between $m$ and $n$.
Proof
Let $m \preceq n$. Then:
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\) | \(\displaystyle x \in \left[{m \,.\,.\, n \circ 1}\right]\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | |||
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\iff\) | \(\displaystyle m \preceq x \land x \preceq \left({n \circ 1}\right)\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | Definition of Closed Interval | ||
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\iff\) | \(\displaystyle m \preceq x \land \left({x \prec n \circ 1 \lor x = n \circ 1}\right)\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | Definition of strictly precedes |
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\) | \(\displaystyle x \in \left[{m \,.\,.\, n}\right] \cup \left\{ {n \circ 1}\right\}\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | |||
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\iff\) | \(\displaystyle m \preceq x \land \left({x \preceq n \lor x = n \circ 1}\right)\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | Definitions of Closed Interval and Union | ||
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\iff\) | \(\displaystyle m \preceq x \land \left({x \prec n \lor x = n \lor x = n \circ 1}\right)\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | Definition of strictly precedes | ||
| \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | \(\iff\) | \(\displaystyle m \preceq x \land \left({x \prec n \circ 1 \lor x = n \circ 1}\right)\) | \(\displaystyle \) | \(\displaystyle \) | \(\displaystyle \) | Definition of strictly precedes |
Thus:
- $\left[{m \,.\,.\, n \circ 1}\right] = \left[{m \,.\,.\, n}\right] \cup \left\{{n \circ 1}\right\}$
$\blacksquare$
Sources
- Seth Warner: Modern Algebra (1965)... (previous)... (next): $\S 16$: Corollary $16.4.2$
