Strict Lower Closure of Sum with One

From ProofWiki
Jump to navigation Jump to search

Theorem

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


Then:

$\forall n \in \struct {S, \circ, \preceq}: \paren {n \circ 1}^\prec = n^\prec \cup \set n$

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 $\struct {S, \circ, \preceq}$ is well-ordered and hence totally ordered, the Trichotomy Law applies.


Thus:

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


So:

\(\ds \forall p \in S: \, \) \(\ds \) \(\) \(\ds p \notin \paren {n \circ 1}^\prec\)
\(\ds \) \(\leadstoandfrom\) \(\ds n \circ 1 \preceq p\) from the above
\(\ds \) \(\leadstoandfrom\) \(\ds n \prec p\) Sum with One is Immediate Successor in Naturally Ordered Semigroup


Similarly:

\(\ds \forall p \in S: \, \) \(\ds \) \(\) \(\ds p \notin n^\prec \cup \set n\)
\(\ds \) \(\leadstoandfrom\) \(\ds n \preceq p \land n \ne p\) from the above
\(\ds \) \(\leadstoandfrom\) \(\ds n \prec p\) Definition of Strictly Precede


So:

$p \notin n^\prec \cup \set n \iff p \notin \paren {n \circ 1}^\prec$


Thus:

$\relcomp S {\paren {n \circ 1}^\prec} = \relcomp S {n^\prec \cup \set n}$

from the definition of relative complement.


So:

\(\ds \paren {n \circ 1}^\prec\) \(=\) \(\ds \relcomp S {\relcomp S {\paren {n \circ 1}^\prec} }\) Relative Complement of Relative Complement
\(\ds \) \(=\) \(\ds \relcomp S {\relcomp S {n^\prec \cup \set n} }\) from above
\(\ds \) \(=\) \(\ds n^\prec \cup \set n\) Relative Complement of Relative Complement

$\blacksquare$


Sources