Finite Chain is Order-Isomorphic to Finite Ordinal

From ProofWiki
Jump to navigation Jump to search


Let $\left({S, \preceq}\right)$ be an ordered set.

Let $C$ be a finite chain in $S$.

Then for some finite ordinal $\mathbf n$:

$\left({C, {\preceq \restriction_C} }\right)$ is order-isomorphic to $\mathbf n$.

That is:

$\left({C, {\preceq \restriction_C} }\right)$ is order-isomorphic to $\N_n$

where $\N_n$ is the initial segment of $\N$ determined by $n$:

$\N_n = \left\{ {k \in \N: k < n}\right\} = \left\{ {0, 1, \ldots, n - 1}\right\}$


By the definition of finite set:

there exists an $n \in \N$ such that there exists a bijection $f: C \to \N_n$.

This $n$ is unique by Equality of Natural Numbers and Set Equivalence is Equivalence Relation.

Define a mapping $g: \N_n \to C$ recursively as:

$g \left({0}\right) = \min C$
$g \left({k + 1}\right) = \min \left({ C \setminus g \left({N_k}\right) }\right)$