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

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.


Then:

$\forall m, n \in \struct {S, \circ, \preceq}: m \preceq n \implies \closedint m {n \circ 1} = \closedint m n \cup \set {n \circ 1}$

where $\closedint m n$ is the closed interval between $m$ and $n$.


Proof

Let $m \preceq n$. Then:

\(\ds \) \(\) \(\ds x \in \closedint m {n \circ 1}\)
\(\ds \) \(\leadstoandfrom\) \(\ds m \preceq x \land x \preceq \paren {n \circ 1}\) Definition of Closed Interval
\(\ds \) \(\leadstoandfrom\) \(\ds m \preceq x \land \paren {x \prec n \circ 1 \lor x = n \circ 1}\) Definition of Strictly Precede


\(\ds \) \(\) \(\ds x \in \closedint m n \cup \set {n \circ 1}\)
\(\ds \) \(\leadstoandfrom\) \(\ds m \preceq x \land \paren {x \preceq n \lor x = n \circ 1}\) Definition of Closed Interval and Definition of Set Union
\(\ds \) \(\leadstoandfrom\) \(\ds m \preceq x \land \paren {x \prec n \lor x = n \lor x = n \circ 1}\) Definition of Strictly Precede
\(\ds \) \(\leadstoandfrom\) \(\ds m \preceq x \land \paren {x \prec n \circ 1 \lor x = n \circ 1}\) Definition of Strictly Precede


Thus:

$\closedint m {n \circ 1} = \closedint m n \cup \set {n \circ 1}$

$\blacksquare$


Sources