Dual of Order Type is Well-Defined Mapping
Theorem
The dual operation on order types is a well-defined mapping.
Proof
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {S_1, \succcurlyeq_1}$ and $\struct {S_2, \succcurlyeq_2}$ denote the dual ordered sets of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$.
Let $\struct {S_1, \preccurlyeq_1} \cong \struct {S_2, \preccurlyeq_2}$, where $\cong$ denotes order isomorphism.
Let $\varrho = \map \ot {S_1, \preccurlyeq_1}$ denote the order type of $\struct {S_1, \preccurlyeq_1}$.
By definition of order type:
- $\varrho = \map \ot {S_1, \preccurlyeq_1} = \map \ot {S_2, \preccurlyeq_2}$
as $\struct {S_1, \preccurlyeq_1} \cong \struct {S_2, \preccurlyeq_2}$
Let $\varrho^*$ denote the denote the dual of $\varrho$.
Thus by definition:
- $\varrho^* = \map \ot {S_1, \succcurlyeq_1}$
From Order Types of Duals of Isomorphic Sets are Equal:
- $\varrho^* = \map \ot {S_2, \succcurlyeq_2}$
The result follows by definition of well-defined mapping.
$\blacksquare$
Sources
- 1996: Winfried Just and Martin Weese: Discovering Modern Set Theory. I: The Basics ... (previous) ... (next): Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations