Closed Interval of Naturally Ordered Semigroup with Successor equals Union with Successor

From ProofWiki
Jump to navigation Jump to search

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 x \in \left[{m \,.\,.\, n \circ 1}\right]\)
\(\displaystyle \) \(\iff\) \(\displaystyle m \preceq x \land x \preceq \left({n \circ 1}\right)\) Definition of Closed Interval
\(\displaystyle \) \(\iff\) \(\displaystyle m \preceq x \land \left({x \prec n \circ 1 \lor x = n \circ 1}\right)\) Definition of Strictly Precedes


\(\displaystyle \) \(\) \(\displaystyle x \in \left[{m \,.\,.\, n}\right] \cup \left\{ {n \circ 1}\right\}\)
\(\displaystyle \) \(\iff\) \(\displaystyle m \preceq x \land \left({x \preceq n \lor x = n \circ 1}\right)\) Definitions of Closed Interval and Union
\(\displaystyle \) \(\iff\) \(\displaystyle m \preceq x \land \left({x \prec n \lor x = n \lor x = n \circ 1}\right)\) Definition of Strictly Precedes
\(\displaystyle \) \(\iff\) \(\displaystyle m \preceq x \land \left({x \prec n \circ 1 \lor x = n \circ 1}\right)\) Definition of Strictly Precedes


Thus:

$\left[{m \,.\,.\, n \circ 1}\right] = \left[{m \,.\,.\, n}\right] \cup \left\{{n \circ 1}\right\}$

$\blacksquare$


Sources