Finite Chain is Order-Isomorphic to Finite Ordinal

From ProofWiki
Jump to navigation Jump to search


Let $\struct {S, \preceq}$ be an ordered set.

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

Then for some finite ordinal $\mathbf n$:

$\struct {C, {\preceq \restriction_C} }$ is order-isomorphic to $\mathbf n$.

That is:

$\struct {C, {\preceq \restriction_C} }$ is order-isomorphic to $\N_n$

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

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


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 behaves like Equivalence Relation.

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

$\map g 0 = \min C$
$\map g {k + 1} = \map \min {C \setminus \map g {N_k} }$