Strict Lower Closure of Sum with One

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\left({S, \circ, \preceq}\right)$ be a naturally ordered semigroup.


Then:

$\forall n \in \left({S, \circ, \preceq}\right): \left({n \circ 1}\right)^\prec = n^\prec \cup \left\{{n}\right\}$

where $n^\prec$ is defined as the strict lower closure of $n$, that is, the set of elements strictly preceding $n$.


Proof

First note that as $\left({S, \circ, \preceq}\right)$ is well-ordered and hence totally ordered, the Trichotomy Law applies.


Thus:

\(\displaystyle \forall m \in S:\) \(\) \(\displaystyle m \notin n^\prec\)
\(\displaystyle \) \(\iff\) \(\displaystyle \neg \ m \prec n\) Definition of Strict Lower Closure
\(\displaystyle \) \(\iff\) \(\displaystyle m = n \lor n \prec m\) Trichotomy Law
\(\displaystyle \) \(\iff\) \(\displaystyle n \preceq m\) Definition of Strictly Precede


So:

\(\displaystyle \forall p \in S:\) \(\) \(\displaystyle p \notin \left({n \circ 1}\right)^\prec\)
\(\displaystyle \) \(\iff\) \(\displaystyle n \circ 1 \preceq p\) from the above
\(\displaystyle \) \(\iff\) \(\displaystyle n \prec p\) Sum with One is Immediate Successor in Naturally Ordered Semigroup


Similarly:

\(\displaystyle \forall p \in S:\) \(\) \(\displaystyle p \notin n^\prec \cup \left\{ {n}\right\}\)
\(\displaystyle \) \(\iff\) \(\displaystyle n \preceq p \land n \ne p\) from the above
\(\displaystyle \) \(\iff\) \(\displaystyle n \prec p\) Definition of Strictly Precede


So:

$p \notin n^\prec \cup \left\{{n}\right\} \iff p \notin \left({n \circ 1}\right)^\prec$


Thus:

$\complement_S \left({\left({n \circ 1}\right)^\prec}\right) = \complement_S \left({n^\prec \cup \left\{{n}\right\}}\right)$

from the definition of relative complement.


So:

\(\displaystyle \left({n \circ 1}\right)^\prec\) \(=\) \(\displaystyle \complement_S \left({\complement_S \left({\left({n \circ 1}\right)^\prec}\right)}\right)\) Relative Complement of Relative Complement
\(\displaystyle \) \(=\) \(\displaystyle \complement_S \left({\complement_S \left({n^\prec \cup \left\{ {n}\right\} }\right)}\right)\) from above
\(\displaystyle \) \(=\) \(\displaystyle n^\prec \cup \left\{ {n}\right\}\) Relative Complement of Relative Complement

$\blacksquare$


Sources