Dual of Order Type is Well-Defined Mapping

From ProofWiki
Jump to navigation Jump to search

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