Lexicographic Product of Family of Ordered Sets is Ordered Set

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {I, \preceq}$ be a well-ordered set.

For each $i \in I$, let $\struct {S_i, \preccurlyeq_i}$ be an ordered set.

Let $\ds D = \prod_{i \mathop \in I} S_i$ be the Cartesian product of the family $\family {\struct {S_i, \preccurlyeq_i} }_{i \mathop \in I}$ indexed by $I$.

Let $\preccurlyeq_D$ be the lexicographic order on $D$, defined as:

$\forall u, v \in D: u \preccurlyeq_D v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in I$ such that $\map u i \ne \map v i$} \end {cases}$


Then $\struct {D, \preccurlyeq_D}$ is an ordered set.


Proof

For a subset $J$ of $I$, let $D_J$ be defined as:

$\ds D_J = \prod_{i \mathop \in J} S_i$

Similarly, let $\preccurlyeq_J$ be the lexicographic order on $D_J$:

$\forall u, v \in D_J: u \preccurlyeq_J v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in J$ such that $\map u i \ne \map v i$} \end {cases}$


Let $Y$ be the subset of $I$ defined as:

$\ds Y = \leftset {y \in I: \struct {D_Y, \preccurlyeq_Y} }$ is an ordered set $\rightset{}$


We require to show that $Y = I$.


Let $b \in I$ be the smallest element of $I$.

Let $J = \set b$.

We have that:

\(\ds D_J\) \(=\) \(\ds \prod_{i \mathop \in J} S_i\)
\(\ds \) \(=\) \(\ds S_b\)
\(\ds \leadsto \ \ \) \(\ds \preccurlyeq_J\) \(=\) \(\ds \preccurlyeq_b\)

We have that $\struct {S_b, \preccurlyeq b}$ is an ordered set.

Thus $b \in Y$ by definition of $Y$.


Let $s \in I$ such that:

$\forall t \in I: t \prec s \implies t \in Y$

Let $T = \set {t \in I: t \prec s}$.

We have that $T \subseteq I$ such that:

$\struct {D_T, \preccurlyeq_T}$ is an ordered set.

Now we consider the lexicographic product $D_T \otimes^l S_s$.

By Lexicographic Order is Ordering:

$\struct {D_T \times S_s, \preccurlyeq l}$ is an ordered set.

We have that $\preccurlyeq l$ is defined as:

$\tuple {u, s_1} \preccurlyeq_l \tuple {v, s_2} \iff \tuple {u \prec_T v} \lor \paren {u = v \land s_1 \preccurlyeq_s s_2}$

But $\preccurlyeq_T$ is defined as:

$\forall u, v \in D_T: u \preccurlyeq_T v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in T$ such that $\map u i \ne \map v i$} \end {cases}$

Let $T' = T \cup \set s$.

We see that $\preccurlyeq l$ is the same as:

$\forall u, v \in D_{T'}: u \preccurlyeq_{T'} v \iff \begin {cases} u = v \\ \map u i \preccurlyeq_i \map v i & \text {for the $\preceq$-smallest $i \in T'$ such that $\map u i \ne \map v i$} \end {cases}$

That is:

$s \in Y$


Thus we have shown that:

$\paren {\forall t \in I: t \prec s \implies t \in Y} \implies s \in Y$

By Induction on Well-Ordered Set it follows that $Y = I$.

The result follows.

$\blacksquare$



Sources