nyuuzyou/wikis huggingface dataset:
Order Isomorphism is Reflexive

== Theorem ==
Let $\struct {S, \preccurlyeq}$ be an ordered set.
Then $\struct {S, \preccurlyeq}$ is isomorphic to itself.
== Proof ==
Let $I_S: S \to S$ denote the identity mapping on $S$.
From Identity Mapping is Order Isomorphism, $I_S: \struct {S, \preccurlyeq} \to \struct {S, \preccurlyeq}$ is an order isomorphism.
The result follows.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $24 \ \text {(a)}$
Category:Order Isomorphisms
Category:Reflexive Relations
Order Isomorphism is Surjective Order Embedding

== Theorem ==
Let $\struct {S, \preceq_1}$ and $\struct {T, \preceq_2}$ be ordered sets.
Let $f: S \to T$ be a mapping.
Then $f$ is an order isomorphism :
:$(1): \quad f$ is a surjection
:$(2): \quad \forall x, y \in S: x \preceq_1 y \iff \map f x \preceq_2 \map f y$
That is, $f$ is an order embedding which is also a surjection.
== Proof ==
=== Necessary Condition ===
Suppose $f$ is an order isomorphism.
Then by definition $f$ is a bijection and so a surjection.
Also by definition, $f$ is increasing, and so:
:$\forall x, y \in S: x \preceq_1 y \implies \map f x \preceq_2 \map f y$
Also by definition $f^{-1}$ is also a bijection which is increasing, and so:
:$\forall x, y \in S: \map f x \preceq_2 \map f y \implies x = \map {f^{-1} } {\map f x} \preceq_1 \map {f^{-1} } {\map f y} = y$
and so:
:$\forall x, y \in S: x \preceq_1 y \iff \map f x \preceq_2 \map f y$
=== Sufficient Condition ===
Suppose $f: S \to T$ is a mapping such that:
:$f$ is a surjection;
:$\forall x, y \in S: x \preceq_1 y \iff \map f x \preceq_2 \map f y$
From Order Embedding is Injection we have that $f$ is an injection.
As, by hypothesis, it is also surjective, it follows that it is a bijection.
Now, suppose $a, b \in T$.
As $f$ is surjective:
:$\exists x, y \in S: \map f x = a, \map f y = b$
As $f$ is bijective, then:
:$x = \map {f^{-1} } a, y = \map {f^{-1} } b$
So by hypothesis:
:$a \preceq_2 b \implies \map f x \preceq_2 \map f y \implies \map {f^{-1} } a = x \preceq_1 y = \map {f^{-1} } b$
Hence, by definition, $f$ is an order isomorphism.
== Sources ==
* : $\S 7$: Theorem $7.1$
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $19$
Category:Order Isomorphisms
Category:Order Embeddings
Category:Surjections
Order Isomorphism is Symmetric

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {S_1, \preccurlyeq_1}$ be isomorphic to $\struct {S_2, \preccurlyeq_2}$.
Then $\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {S_1, \preccurlyeq_1}$.
== Proof ==
Let $\phi: S_1 \to S_2$ be an order isomorphism from $\struct {S_1, \preccurlyeq_1}$ to $\struct {S_2, \preccurlyeq_2}$.
From Inverse of Order Isomorphism is Order Isomorphism, $\phi^{-1}: S_2 \to S_1$ is an order isomorphism from $\struct {S_2, \preccurlyeq_2}$ to $\struct {S_1, \preccurlyeq_1}$.
The result follows.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $24 \ \text {(b)}$
Category:Order Isomorphisms
Category:Symmetric Relations
Order Isomorphism is Transitive

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$, $\struct {S_2, \preccurlyeq_2}$ and $\struct {S_3, \preccurlyeq_3}$ be ordered sets.
Let $\struct {S_1, \preccurlyeq_1}$ be isomorphic to $\struct {S_2, \preccurlyeq_2}$.
Let $\struct {S_2, \preccurlyeq_2}$ be isomorphic to $\struct {S_3, \preccurlyeq_3}$.
Then $\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {S_3, \preccurlyeq_3}$.
== Proof ==
Let $\phi: S_1 \to S_2$ be an order isomorphism from $\struct {S_1, \preccurlyeq_1}$ to $\struct {S_2, \preccurlyeq_2}$.
Let $\psi: S_2 \to S_3$ be an order isomorphism from $\struct {S_2, \preccurlyeq_2}$ to $\struct {S_3, \preccurlyeq_3}$.
From Composite of Order Isomorphisms is Order Isomorphism, $\psi \circ \phi: S_1 \to S_3$ is an order isomorphism from $\struct {S_1, \preccurlyeq_1}$ to $\struct {S_3, \preccurlyeq_3}$.
The result follows.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $24 \ \text {(c)}$
Category:Order Isomorphisms
Category:Examples of Transitive Relations
Order Isomorphism on Lattice preserves Lattice Structure

== Theorem ==
Let $\struct {S, \preccurlyeq_1}$ and $\struct {T, \preccurlyeq_2}$ be ordered sets.
Let $\phi: \struct {S, \preccurlyeq_1} \to \struct {T, \preccurlyeq_2}$ be an order isomorphism.
Then $\struct {S, \preccurlyeq_1}$ is a lattice $\struct {T, \preccurlyeq_2}$ is also a lattice.
== Proof ==
Let $\struct {S, \preccurlyeq_1}$ be a lattice
Then by definition $\preccurlyeq_1$ is a lattice ordering.
We need to show that for all $x, y \in S$, the ordered set $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$ admits both a supremum and an infimum. 
Let $x, y \in S$.
Then $\struct {\set {x, y}, \preccurlyeq_1}$ admits both a supremum and an infimum.
Let $c = \map \sup {\set {x, y}, \preccurlyeq_1}$.
Then by definition of supremum:
:$\forall s \in \set {x, y}: s \preccurlyeq_1 c$
:$\forall d \in S: c \preccurlyeq_1 d$
where $d$ is an upper bound of $\struct {\set {x, y}, \preccurlyeq_1} \subseteq S$.
Now consider the image of $\set {x, y}$ under $\phi$.
By definition of order isomorphism:
:$\forall \map \phi s \in \set {\map \phi x, \map \phi y}: \map \phi c \preccurlyeq_2 \map \phi s$
:$\forall \map \phi d \in T: \map \phi c \preccurlyeq_2 \map \phi d$
where $\map \phi d$ is an upper bound of $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2} \subseteq T$.
So by definition of supremum:
:$\map \phi c = \map \sup {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$
That is, $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$ admits a supremum.
Using a similar technique it can be shown that:
:If $c = \map \inf {\set {x, y}, \preccurlyeq}$, then:
:$\map \phi c = \map \inf {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$
Hence $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$ admits both a supremum and an infimum.
That is, $\preccurlyeq_2$ is a lattice ordering and so $\struct {T, \preccurlyeq_2}$ is a lattice.
By Inverse of Order Isomorphism is Order Isomorphism, if $\phi$ is an order isomorphism then so is $\phi^{-1}$.
So the same technique is used to show that if $\struct {T, \preccurlyeq_2}$ is a lattice then so is $\struct {S, \preccurlyeq_1}$.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Theorem $14.4$
Category:Lattice Theory
Category:Order Isomorphisms
Order Isomorphism on Strictly Well-Founded Relation preserves Strictly Well-Founded Structure

== Theorem ==
Let $A_1$ and $A_2$ be classes.
Let $\prec_1$ and $\prec_2$ be relations.
Let $\phi: \struct {A_1, \prec_1} \to \struct {A_2, \prec_2}$ be an order isomorphism.
Then $\struct {A_1, \prec_1}$ is a strictly well-founded structure $\struct {A_2, \prec_2}$ is also a strictly well-founded structure.
== Proof ==
Take any nonempty subset $B \subseteq A_1$.
From Order Isomorphism Preserves Strictly Minimal Elements:
:$x$ is a strictly minimal element of $B$ $\map \phi x$ is a strictly minimal element of $\phi \sqbrk B$.
By the definition of strictly well-founded relation, $\struct {A_1, \prec_1}$ is strictly well-founded $\struct {A_2, \prec_2}$ is strictly well-founded.
== Sources ==
* : $\S 6.32$
Category:Order Isomorphisms
Order Isomorphism on Totally Ordered Set preserves Total Ordering

== Theorem ==
Let $\struct {S, \preccurlyeq_1}$ and $\struct {T, \preccurlyeq_2}$ be ordered sets.
Let $\phi: \struct {S, \preccurlyeq_1} \to \struct {T, \preccurlyeq_2}$ be an order isomorphism.
Then $\struct {S, \preccurlyeq_1}$ is a totally ordered set $\struct {T, \preccurlyeq_2}$ is also a totally ordered set.
== Proof ==
=== Necessary Condition ===
Let $\struct {S, \preccurlyeq_1}$ be a totally ordered set
Then by definition $\preccurlyeq_1$ is a total ordering.
Let $x, y \in S$.
Then either $x \preccurlyeq_1 y$ or $y \preccurlyeq_1 x$.
From the definition of order isomorphism, either:
:$\map \phi x \preccurlyeq_2 \map \phi y$
or:
:$\map \phi y \preccurlyeq_2 \map \phi x$
and so by definition $\preccurlyeq_2$ is also a total ordering.
So by definition $\struct {T, \preccurlyeq_2}$ is also a totally ordered set.
=== Sufficient Condition ===
By Inverse of Order Isomorphism is Order Isomorphism, if $\phi$ is an order isomorphism then so is $\phi^{-1}$.
Applying the other implication (proven above) to $\phi^{-1}$, it follows that if $\struct {T, \preccurlyeq_2}$ is a totally ordered set then so is $\struct {S, \preccurlyeq_1}$.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Theorem $14.4$
Category:Order Isomorphisms
Category:Total Orderings
Order Isomorphism on Well-Ordered Set preserves Well-Ordering

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\phi: \struct {S_1, \preccurlyeq_1} \to \struct {S_2, \preccurlyeq_2}$ be an order isomorphism.
Then $\struct {S_1, \preccurlyeq_1}$ is a well-ordered set $\struct {S_2, \preccurlyeq_2}$ is also a well-ordered set.
== Proof ==
Let $\struct {S_1, \preccurlyeq_1}$ be a well-ordered set.
Then by definition $\preccurlyeq_1$ is a well-ordering.
By Well-Ordering is Total Ordering, $\preccurlyeq_1$ is a total ordering.
From Order Isomorphism on Totally Ordered Set preserves Total Ordering, it follows that $\struct {S_2, \preccurlyeq_2}$ is a totally ordered set.
All that remains is to show that $\preccurlyeq$ is a well-founded relation.
Let $T_1 \subseteq S_1$.
As $\struct {S_1, \preccurlyeq_1}$ is a well-ordered set:
:$\exists m_1 \in T_1: \forall t \in T_1: t = m_1 \lor \neg \paren {t \preccurlyeq_1 m_1}$
Now consider the image $m_2$ of $m_1$ in $S_2$:
:$m_2 = \map \phi {m_1}$
 $\struct {S_2, \preccurlyeq_2}$ is not a well-ordered set.
Let there exist $T_2 \subseteq S_2$ such that:
:$\exists x \in T_2: x \ne m_2, x \preccurlyeq_2 m_2$
By Inverse of Order Isomorphism is Order Isomorphism, if $\phi$ is an order isomorphism then so is $\phi^{-1}$.
Hence:
:$\map {\phi^{-1} } x \ne \map {\phi^{-1} } {m_2}, \map {\phi^{-1} } x \preccurlyeq_2 \map {\phi^{-1} } {m_2}$
But this contradicts the fact that $\struct {S_1, \preccurlyeq_1}$ is well-ordered.
Hence by Proof by Contradiction $\struct {S_2, \preccurlyeq_2}$ must be a well-ordered set.
The same technique is used to show that if $\struct {S_2, \preccurlyeq_2}$ is a well-ordered set then so is $\struct {S_1, \preccurlyeq_1}$.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 14$: Orderings: Theorem $14.4$
* : $\S 6.32$
Category:Order Isomorphisms
Category:Well-Orderings
Order Modulo n of Power of Integer

== Theorem ==
Let $a$ have multiplicative order $c$ modulo $n$.
Then for any $k \ge 1$, $a^k$ has multiplicative order $\dfrac c {\gcd \set {c, k}}$ modulo $n$.
=== Corollary ===
== Proof ==
Let $a$ have multiplicative order $c$ modulo $n$.
Consider $a^k$ and let $d = \gcd \set {c, k}$.
Let $c = d c'$ and $k = d k'$ where $\gcd \set {c', k'} = 1$ from Integers Divided by GCD are Coprime.
We want to show that the multiplicative order $a^k$ modulo $n$ is $c'$.
Let the order $a^k$ modulo $n$ be $r$.
Then:
So, by Integer to Power of Multiple of Order, $c'$ is a multiple of $r$, that is, $r \divides c'$.
On the other hand, $a^{k r} = \paren {a^k}^r \equiv 1 \pmod n$, and so $k r$ is a multiple of $c$.
Substituting for $k$ and $c$, we see that $d k' r$ is a multiple of $d c'$ which shows $c'$ divides $k' r$.
But from Euclid's Lemma (which applies because $\gcd \set {c', k'} = 1$), we have that $c'$ divides $r$, or $c' \divides r$.
So, as $c' \divides r$ and $r \divides c'$, from Divisor Relation on Positive Integers is Partial Ordering, it follows that $c' = r$.
Category:Number Theory
Order Modulo n of Power of Integer/Corollary

== Theorem ==
Let $a$ be a primitive root of $n$.
Then:
:$a^k$ is also a primitive root of $n$
:
:$k \perp \map \phi n$
where $\phi$ is the Euler phi function.
Furthermore, if $n$ has a primitive root, it has exactly $\map \phi {\map \phi n}$ of them.
== Proof ==
Let $a$ be a primitive root of $n$.
Then $R = \set {a, a^2, \ldots, a^{\map \phi n}}$ is a reduced residue system for $n$.
Hence all primitive roots are contained in $R$.
By Order Modulo n of Power of Integer, the multiplicative order $a^k$ modulo $n$ is $\dfrac {\map \phi n} {\gcd \set {\map \phi n, k} }$.
Hence $a^k$ will be a primitive root of $n$ exactly when $\gcd \set {\map \phi n, k} = 1$.
That is, when $\map \phi n \perp k$.
So the primitive roots are the integers $a^k$, where $k \in \set {1, 2, \ldots, \map \phi n}$.
By definition of $\phi$, there are $\map \phi {\map \phi n}$ such $k$.
Hence there are $\map \phi {\map \phi n}$ primitive roots of $n$.
Category:Number Theory
Order Statistic/Examples/Greatest Observation

== Example of Order Statistics ==
Let $S$ be a sample of ordinal data with a total of $n$ observations.
Let $x_{\paren i}$ denote the $i$th order statistic of $S$.
Then $x_{\paren n}$ is the observation which has the greatest value of $S$.
== Sources ==
* 
* 
Category:Examples of Order Statistics
Order Statistic/Examples/Median

== Example of Order Statistics ==
Let $S$ be a sample of ordinal data consisting of $2 n + 1$ observations.
Let $x_{\paren i}$ denote the $i$th order statistic of $S$.
The median of $S$ is $x_{\paren {n + 1} }$.
== Sources ==
* 
* 
Category:Examples of Order Statistics
Category:Medians
Order Sum of Ordered Sets is Ordered

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Then the order sum $\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$ of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ is also an ordered set.
== Proof ==
Let $\struct {S, \preccurlyeq} := \struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$.
By definition:
::$\forall \tuple {a, b}, \tuple {c, d} \in S: \tuple {a, b} \preccurlyeq \tuple {c, d} \iff \begin {cases} b = 0 \text { and } d = 1 \\ b = d = 0 \text { and } a \preccurlyeq_1 c \\ b = d = 1 \text { and } a \preccurlyeq_2 c \end {cases}$
We check in turn each of the criteria for an ordering:
=== Reflexivity ===
We have by definition of set union:
:$\forall \tuple {a, n} \in S_1 \sqcup S_2: a \in S_1 \lor a \in S_1$
and so either $a \preccurlyeq_1 a$ or $a \preccurlyeq_2 a$.
Hence by definition of $\oplus$:
:$\forall \tuple {a, n} \in S: \tuple {a, n} \preccurlyeq \tuple {a, n}$
So $\preccurlyeq$ is reflexive.
=== Transitivity ===
We proceed on a case-by-case basis.
Let $\tuple {a, n_a}, \tuple {b, n_b}, \tuple {c, n_c} \in S$.
Let $\tuple {a, n_a} \preccurlyeq \tuple {b, n_b}$ and $\tuple {b, n_b} \preccurlyeq \tuple {c, n_c}$.
Suppose $a, b, c \in S_1$.
Then:
Suppose $a, b, c \in S_2$.
Then:
Suppose $a, b \in S_1$ and $c \in S_2$.
Then:
Then we have that:
Suppose $a \in S_1$ and $b, c \in S_2$.
Then:
Then we have that:
There are four other cases to consider:
:$a, c \in S_1, b \in S_2$
:$b, c \in S_1, a \in S_2$
:$c \in S_1, a, b \in S_2$
:$b \in S_1, a, c \in S_2$.
None of these can happen as otherwise one of $\lnot \paren {\tuple {a, n_a} \preccurlyeq \tuple {b, n_b} }$ or $\lnot \paren {\tuple {b, n_b} \preccurlyeq \tuple {c, n_c} }$ would be the case.
Thus in all cases we have that:
:$\tuple {a, n_a} \preccurlyeq \tuple {b, n_b} \text { and } \tuple {b, n_b} \preccurlyeq \tuple {c, n_c} \implies \tuple {a, n_a} \preccurlyeq \tuple {c, n_c}$
So we have shown that $\preccurlyeq$ is transitive.
=== Antisymmetry ===
Suppose $\tuple {a, n_a} \preccurlyeq \tuple {b, n_b}$ and $\tuple {b, n_b} \preccurlyeq \tuple {a, n_a}$.
It cannot be the case that $a \in S_1$ and $b \in S_2$ because then $\lnot \paren {\tuple {b, n_b} \preccurlyeq \tuple {a, n_a} }$.
It cannot be the case that $a \in S_2$ and $b \in S_1$ because then $\lnot \paren {\tuple {a, n_a} \preccurlyeq \tuple {b, n_b} }$
So either $a, b \in S_1$ or $a, b \in S_2$.
If $a, b \in S_1$ then $a = b$ by antisymmetry of $\preccurlyeq_1$.
If $a, b \in S_2$ then $a = b$ by antisymmetry of $\preccurlyeq_2$.
Thus in all cases it can be seen that:
:$\tuple {a, n_a} \preccurlyeq \tuple {b, n_b} \text { and } \tuple {b, n_b} \preccurlyeq \tuple {a, n_a} \implies \tuple {a, n_a} = \tuple {b, n_b}$
So $\preccurlyeq$ is antisymmetric.
So we have shown that $\preccurlyeq$ is reflexive, transitive and antisymmetric.
Thus by definition, $\preccurlyeq$ is an ordering and so $\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$ is an ordered set.
Category:Order Sums
Order Sum of Totally Ordered Sets is Totally Ordered

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be totally ordered sets.
Then the order sum $\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$ of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ is also a totally ordered set.
== Proof ==
Let $\struct {S, \preccurlyeq} := \struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$.
From Order Sum of Ordered Sets is Ordered, $\struct {S, \preccurlyeq}$ is an ordered set.
It remains to be shown that $\tuple {a, b}$ and $\tuple {c, d}$ are comparable for all $\tuple {a, b}, \tuple {c, d} \in S$.
Let $\tuple {a, b}, \tuple {c, d} \in S$ be arbitrary.
By definition:
::$\forall \tuple {a, b}, \tuple {c, d} \in S: \tuple {a, b} \preccurlyeq \tuple {c, d} \iff \begin {cases} b = 0 \text { and } d = 1 \\ b = d = 0 \text { and } a \preccurlyeq_1 c \\ b = d = 1 \text { and } a \preccurlyeq_2 c \end {cases}$
Let $a, c \in S_1$.
Then as $\preccurlyeq_1$ is a total ordering, $a$ and $c$ are comparable.
Hence by definition of $\oplus$ it follows that $\tuple {a, b}$ and $\tuple {c, d}$ are comparable.
Let $a, c \in S_2$.
Then as $\preccurlyeq_2$ is a total ordering, $a$ and $c$ are comparable.
Hence by definition of $\oplus$ it follows that $\tuple {a, b}$ and $\tuple {c, d}$ are comparable.
Finally, let $a \in S_1$ and $c \in S_2$.
Then $\tuple {a, 0} \in S$ and $\tuple {c, 1} \in S$.
Hence by definition of $\oplus$ it follows that $\tuple {a, b} \preccurlyeq \tuple {c, d}$ and so are comparable.
In all cases, $\tuple {a, b}$ and $\tuple {c, d}$ are comparable.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $26 \ \text {(b)}$
Category:Order Sums
Category:Total Orderings
Order Sum of Well-Founded Orderings is Well-Founded Ordering

== Theorem ==
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\preccurlyeq_1$ and $\preccurlyeq_2$ be well-founded.
Then the order sum $\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$ of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ is also well-founded.
== Proof ==
Let $\struct {S, \preccurlyeq} := \struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$.
Let $T \subseteq S$ such that $T \ne \O$.
Let $T = T_1 \sqcup T_2$ where $T_1 \subseteq S_1$ and $T_2 \subseteq S_2$.
Let $T_1 \ne \O$.
Then:
:$\exists x \in T_1: \forall y \in T_1: y \preccurlyeq x \implies y = x$
That is, $T_1$ has a minimal element $x$ of $T_1$.
Thus we have:
:$\forall y \in T_1: \tuple {y, 0} \preccurlyeq \tuple {x, 0} \implies \tuple {y, 0} = \tuple {x, 0}$
by definition of order sum.
Also by definition of order sum:
:$\forall \tuple {z, 1} \in T: \tuple {x, 0} \preccurlyeq \tuple {z, 1}$
and so vacuously:
:$\forall \tuple {z, 1} \in T: \tuple {z, 1} \preccurlyeq \tuple {x, 0} \implies \tuple {z, 1} = {x, 0}$
and so $\tuple {x, 0}$ is seen to be a minimal element of $T$.
So if $T_1 \ne \O$ it follows that $T$ has a minimal element.
Let $T_1 = \O$.
Then $T$ consists completely of elements of the form $\tuple {t, 1}$ where $t \in T_2$.
So, let $x \in T_2$ be a minimal element $T_2$.
Then:
:$\forall y \in T_2: y \preccurlyeq x \implies y = x$
Thus we have:
:$\forall y \in T_2: \tuple {y, 1} \preccurlyeq \tuple {x, 1} \implies \tuple {y, 1} = \tuple {x, 1}$
by definition of order sum.
So $\tuple {x, 1}$ is seen to be a minimal element of $T$.
So if $T_1 = \O$ it follows that $T$ has a minimal element.
In both cases it is seen that an arbitrary non-empty subset of $T$ has a minimal element.
Hence the result by definition of well-founded.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $26 \ \text {(a)}$
Category:Order Sums
Category:Well-Founded Relations
Order Topology equals Dual Order Topology

== Theorem ==
Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\tau$ be the $\preceq$-order topology on $S$.
Let $\tau'$ be the $\succeq$-order topology on $S$, where $\succeq$ is the dual ordering of $\preceq$.
Then $\tau' = \tau$.
== Proof ==
Let $U$ be an open ray in $\struct {S, \preceq}$.
By Open Ray is Dual to Open Ray, $U$ is an open ray in $\struct {S, \preceq}$.
Since the open rays in a totally ordered set form a sub-basis for the topology on that set, $\tau'$ is finer than $\tau$.
By the same argument, $\tau$ is finer than $\tau'$.
Thus by definition of set equality:
:$\tau' = \tau$
Category:Order Topology
Order Topology is Hausdorff

== Theorem ==
Let $\struct {X, \preceq, \tau}$ be a linearly ordered space.
Then $\struct {X, \tau}$ is a Hausdorff space.
== Proof ==
Let $x, y \in X$ with $x \ne y$.
Since $\le$ is a total ordering, either $x \prec y$ or $y \prec x$.
, assume that $x \prec y$.
If there is a $z \in X$ such that $x \prec z \prec y$, then $z^\prec$ and $z^\succ$ separate $x$ and $y$.
Otherwise, by Upper Closure is Strict Upper Closure of Immediate Predecessor, $y^\prec$ and $x^\succ$ separate $x$ and $y$.
Since any two distinct points can be separated by neighborhoods, $\struct {X, \tau}$ is a Hausdorff space.
Category:Order Topology
Order Topology is Normal

== Theorem ==
Let $\struct {S, \preceq}$ be a toset.
Let $\tau$ be the order topology on $S$.
Then $\struct {S, \tau}$ is normal.
== Proof ==
From Linearly Ordered Space is Completely Normal, $\struct {S, \tau}$ is a completely normal space.
The result follows from Completely Normal Space is Normal Space.
Category:Order Topology
Category:Normal Spaces
Order Topology on Convex Subset is Subspace Topology

== Theorem ==
Let $\struct {S, \preceq,\tau}$ be a linearly ordered space.
Let $A \subseteq S$ be a convex set in $S$.
Let $\upsilon$ be the order topology on $A$.
Let $\tau'$ be the $\tau$-relative subspace topology on $A$.
Then $\upsilon = \tau'$.
== Proof ==
By the definition of the order topology, the sets of open rays in $\struct {S, \preceq}$ and $\struct {A, \preceq}$ form sub-bases for $\tau$ and $\upsilon$, respectively.
By Sub-Basis for Topological Subspace, we need only show that the set of open rays in $\struct {S, \preceq}$ induces a subbase for $\upsilon$.
Specifically, we will show that each open ray in $A$ is the intersection of $A$ with an open ray in $S$, and we will show that the intersection of any open ray in $S$ with $A$ is either an open ray in $A$, the empty set, or $A$.
From Strict Lower Closure is Dual to Strict Upper Closure and duality principle, we need to show this only for the upward-pointing rays.
For each $p \in S$, let $p^{\succ S}$ be the strict upper closure of $p$ in $S$.
For each $p \in A$, let $p^{\succ A}$ be the strict upper closure of $p$ in $A$.
Let $p \in A$.
Then by Strict Upper Closure in Restricted Ordering:
:$p^{\succ A} = A \cap p^{\succ S}$
Let $q \in S$.
If $q \in A$, then $A \cap q^{\succ S} = q^{\succ A}$, so $A \cap q^{\succ S}$ is an open ray in $A$.
Suppose instead that $q \notin A$.
If $A \cap q^{\succ S} = \O$, the proof is complete.
Otherwise, $A \cap q^{\succ S}$ must have some element $x$.
 there is a $y \in A \setminus \paren {A \cap q^{\succ S} } = A \cap q^{\preceq S}$.
Then since $q \notin A$, it follows that $y \prec q$.
Thus $y \prec q \prec x$, $y, x \in A$, and $q \notin A$, contradicting the fact that $A$ is convex.
Thus $A \cap q^{\succ S} = A$.
Category:Order Topology
Category:Topological Subspaces