avewright/proofwiki-math huggingface dataset:
Theorem: Well-Founded Relation is not necessarily Ordering

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a well-founded relation on $S$.
Then it is not necessarily the case that $\RR$ is also either an ordering or a strict ordering.

Proof:
Proof by Counterexample:
Let $P$ be the set of all polynomials over $\R$ in one variable with real coefficients.
Let $\DD$ be a relation on $P$ defined as:
:$\forall p_0, p_1 \in P: \tuple {p_0, p_1} \in \DD$ {{iff}} $p_0$ is the derivative of $p_1$.
From Differentiation of Polynomials induces Well-Founded Relation, we have that $\DD$ is a well-founded relation on $P$.
Let $P_a$ be the polynomial defined as:
:$P_a = x^3$
Then the derivative of $P_a$ {{WRT|Differentiation}} $x$ is:
:$P_a' = \dfrac \d {\d x} x^3 = 3 x^2$
Then the derivative of $P_a$ {{WRT|Differentiation}} $x$ is:
:$P_a'' = \dfrac \d {\d x} 3 x^2 = 6 x$
So we have that:
:$\tuple {P_a', P_a} \in \DD$
and:
:$\tuple {P_a'', P_a'} \in \DD$
but it is not the case that $\tuple {P_a'', P_a} \in \DD$.
That is, $\DD$ is not transitive.
It follows that $\DD$ is neither an ordering nor a strict ordering.
{{qed}}
Theorem: Well-Founded Relation has no Relational Loops

Let $\RR$ be a well-founded relation on $S$.
Let $x_1, x_2, \ldots, x_n \in S$.
Then:
:$\neg \paren {\paren {x_1 \mathrel \RR x_2} \land \paren {x_3 \mathrel \RR x_4} \land \cdots \land \paren {x_n \mathrel \RR x_1} }$
That is, there are no relational loops within $S$.

Proof:
Since $x_1, x_2, \ldots, x_n \in S$, there exists a non-empty subset $T$ of $S$ such that:
:$T = \set {x_1, x_2, \ldots, x_n}$
By the definition of a well-founded relation:
:$(1): \quad \exists z \in T: \forall y \in T \setminus z: \neg y \mathrel \RR z$
{{AimForCont}} $\paren {x_1 \mathrel \RR x_2} \land \paren {x_2 \mathrel \RR x_3} \land \cdots \land \paren {x_n \mathrel \RR x_1}$.
We have that the elements of $T$ are $x_1, x_2, \ldots, x_n$.
Hence:
:$\forall y \in T: \exists z \in T \setminus z: y \mathrel \RR z$
This then contradicts $(1)$.
Hence:
:$\neg \paren {\paren {x_1 \mathrel \RR x_2} \land \paren {x_3 \mathrel \RR x_4} \land \cdots \land \paren {x_n \mathrel \RR x_1} }$
and so it follows that a well-founded relation has no relational loops.
{{qed}}
Theorem: Infinite Sequence Property of Strictly Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Then $\RR$ is a strictly well-founded relation {{iff}} there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$

Proof:
=== Reverse Implication ===
{{:Infinite Sequence Property of Strictly Well-Founded Relation/Reverse Implication/Proof 1}}{{qed|lemma}}
Theorem: Infinite Sequence Property of Strictly Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Then $\RR$ is a strictly well-founded relation {{iff}} there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$

Proof:
Suppose $\RR$ is not a strictly well-founded relation.
So by definition there exists a non-empty subset $T$ of $S$ which has no strictly minimal element.
Let $a \in T$.
Since $a$ is not strictly minimal in $T$, we can find $b \in T: b \mathrel \RR a$.
This holds for all $a \in T$.
Hence the restriction $\RR \restriction_{T \times T}$ of $\RR$ to $T \times T$ is a right-total endorelation on $T$.
So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
then $\RR$ is a strictly well-founded relation.
Theorem: Infinite Sequence Property of Strictly Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Then $\RR$ is a strictly well-founded relation {{iff}} there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$

Proof:
Suppose $\RR$ is not a strictly well-founded relation.
Hence there exists $T \subseteq S$ such that $T$ has no strictly minimal element under $\RR$.
Let $a_0 \in T$.
We have that $a_0$ is not strictly minimal in $T$.
So:
:$\exists a_1 \in T: a_1 \mathrel \RR a_0$
Similarly, $a_1$ is not strictly minimal in $T$.
So:
:$\exists a_2 \in T: a_2 \mathrel \RR a_1$
Let $a_{k + 1}$ be an arbitrary element for which $a_{k + 1} \mathrel \RR a_k$.
In order to allow this to be possible in the infinite case, it is necessary to invoke the Axiom of Dependent Choice as follows:
Let $a_k \in T$.
Then as $a_k$ is not strictly minimal in $T$:
:$\exists a_{k + 1} \in T: a_{k + 1} \mathrel \RR a_k$
Hence by definition $\RR$ is a right-total relation.
So, by the Axiom of Dependent Choice, it follows that:
:$\forall n \in \N: \exists a_n \in T: a_{n + 1} \mathrel \RR a_n$
Thus we have been able to construct an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$.
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
then $\RR$ is a strictly well-founded relation.
Theorem: Infinite Sequence Property of Strictly Well-Founded Relation/Reverse Implication

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be such that there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
Then $\RR$ is a strictly well-founded relation.

Proof:
Suppose $\RR$ is not a strictly well-founded relation.
So by definition there exists a non-empty subset $T$ of $S$ which has no strictly minimal element.
Let $a \in T$.
Since $a$ is not strictly minimal in $T$, we can find $b \in T: b \mathrel \RR a$.
This holds for all $a \in T$.
Hence the restriction $\RR \restriction_{T \times T}$ of $\RR$ to $T \times T$ is a right-total endorelation on $T$.
So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
then $\RR$ is a strictly well-founded relation.
Theorem: Infinite Sequence Property of Strictly Well-Founded Relation/Reverse Implication

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be such that there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
Then $\RR$ is a strictly well-founded relation.

Proof:
Suppose $\RR$ is not a strictly well-founded relation.
Hence there exists $T \subseteq S$ such that $T$ has no strictly minimal element under $\RR$.
Let $a_0 \in T$.
We have that $a_0$ is not strictly minimal in $T$.
So:
:$\exists a_1 \in T: a_1 \mathrel \RR a_0$
Similarly, $a_1$ is not strictly minimal in $T$.
So:
:$\exists a_2 \in T: a_2 \mathrel \RR a_1$
Let $a_{k + 1}$ be an arbitrary element for which $a_{k + 1} \mathrel \RR a_k$.
In order to allow this to be possible in the infinite case, it is necessary to invoke the Axiom of Dependent Choice as follows:
Let $a_k \in T$.
Then as $a_k$ is not strictly minimal in $T$:
:$\exists a_{k + 1} \in T: a_{k + 1} \mathrel \RR a_k$
Hence by definition $\RR$ is a right-total relation.
So, by the Axiom of Dependent Choice, it follows that:
:$\forall n \in \N: \exists a_n \in T: a_{n + 1} \mathrel \RR a_n$
Thus we have been able to construct an infinite sequence $\sequence {a_n}$ in $T$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$.
It follows by the Rule of Transposition that if there is no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
then $\RR$ is a strictly well-founded relation.
Theorem: Infinite Sequence Property of Strictly Well-Founded Relation/Forward Implication

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a strictly well-founded relation.
Then there exists no infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$

Proof:
Let $\RR$ be a strictly well-founded relation.
{{AimForCont}} there exists an infinite sequence $\sequence {a_n}$ in $S$ such that:
:$\forall n \in \N: a_{n + 1} \mathrel \RR a_n$
Let $T = \set {a_0, a_1, a_2, \ldots}$.
Let $a_k \in T$ be a strictly minimal element of $T$.
That is:
:$\forall y \in T: y \not \mathrel \RR a_k$
But we have that:
:$a_{k + 1} \mathrel \RR a_k$
So $a_k$ is not a strictly minimal element.
It follows by Proof by Contradiction that such an infinite sequence cannot exist.
Theorem: Restriction of Well-Founded Relation is Well-Founded

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a well-founded relation on $S$.
Let $T$ be a subset or subclass of $S$.
Let $\RR'$ be the restriction of $\RR$ to $T$.
Then $\preceq'$ is a well-founded relation on $T$.

Proof:
Let $A$ be a non-empty subset of $T$.
By Subset Relation is Transitive, $A$ is a non-empty subset of $S$.
Since $\RR$ is a well-founded relation on $S$, $A$ has a minimal element $m$ under $\RR$.
Let $x \in A$.
Let $x \mathrel {\RR'} m$.
By the definition of restriction:
:$x \mathrel \RR m$
Thus by the definition of minimal element:
:$x = m$
As $x$ is an arbitrary element of $A$, this holds for all $x \in A$.
Hence by definition $m$ is a minimal element of $A$ under $\RR'$.
As $A$ is an arbitrary non-empty subset of $T$, this holds for all non-empty subsets of $T$.
Hence $\RR'$ is a well-founded relation on $T$.
{{qed}}
Category:Well-Founded Relations
gbjqedaemwa7m7vpcwdpnvcc743pkvc
Theorem: Divisor Relation on Positive Integers is Well-Founded Ordering

The divisor relation on $\Z_{>0}$ is a well-founded ordering.

Proof:
Let $\struct {\Z_{>0}, \divides}$ denote the relational structure formed from the strictly positive integers $\Z_{>0}$ under the divisor relation $\divides$.
From Divisor Relation on Positive Integers is Partial Ordering, $\struct {\Z_{>0}, \divides}$ is a partially ordered set.
It remains to be shown that $\divides$ is well-founded.
By definition, we need to show:
:For any non-empty set $T \subseteq \Z_{>0}$, there is an element $z \in T$ such that for all $y \in T \setminus \set z$, $y \nmid z$.
We choose $z = \min T$ as per the usual ordering on $\Z_{>0}$.
Then for any $y \in T \setminus \set z$, we have $y > z$.
By the contrapositive of {{Corollary|Absolute Value of Integer is not less than Divisors}}, we have $y \nmid z$.
Hence the result.
{{qed}}
Theorem: Union of Indexed Family of Sets Equal to Union of Disjoint Sets/General Result

Let $I$ be a set which can be well-ordered by a well-ordering $\preccurlyeq$.
Let $\family {E_\alpha}_{\alpha \mathop \in I}$ be a countable indexed family of sets indexed by $I$ where at least two $E_\alpha$ are distinct.
Then there exists a countable indexed family of disjoint sets $\family {F_\alpha}_{\alpha \mathop \in I}$ defined by:
:$\ds F_\beta = E_\beta \setminus \paren {\bigcup_{\alpha \mathop \prec \beta} E_\alpha}$
satisfying:
:$\ds \bigsqcup_{\alpha \mathop \in I} F_n = \bigcup_{\alpha \mathop \in I} E_n$
where:
:$\bigsqcup$ denotes disjoint union.
:$\alpha \prec \beta$ denotes that $\alpha \preccurlyeq \beta$ and $\alpha \ne \beta$.

Proof:
Denote:
{{begin-eqn}}
{{eqn | l = E
      | r = \bigcup_{\beta \mathop \in I} E_\beta
}}
{{eqn | l = F
      | r = \bigcup_{\beta \mathop \in I} F_\beta
}}
{{end-eqn}}
where:
:$\ds F_\beta = E_\beta \setminus \paren {\bigcup_{\alpha \mathop \prec \beta} E_\alpha}$
We first show that $E = F$.
That $x \in E \implies x \in F$ follows from the construction of $F$ from subsets of $E$.
Thus $E \subseteq F$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcup_{\beta \mathop \in I} F_\beta
}}
{{eqn | ll= \leadsto
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = F_\beta
}}
{{eqn | ll= \leadsto
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = E_\beta
}}
{{eqn | lo= \land
      | l = x
      | o = \notin
      | r = \paren {\bigcup_{\gamma \mathop \prec \beta} E_\gamma}
}}
{{eqn | ll= \leadsto
      | q = \exists \beta \in I
      | l = x
      | o = \in
      | r = E_\beta
      | c = Rule of Simplification
}}
{{end-eqn}}
so $F \subseteq E$.
Thus $E = F$ by definition of set equality.
To show that the sets in $F$ are (pairwise) disjoint, consider an arbitrary $x \in F$. 
Then $x \in F_\beta$ for some $F_\beta$.
By the Well-Ordering Principle, there is a smallest such $\beta$ with respect to $\preccurlyeq$.
Then:
:$\forall \gamma \prec \beta: x \notin F_\gamma$
Choose any distinct $\eta, \zeta \in I$. 
We have:
If $\eta \prec \zeta$, then:
{{begin-eqn}}
{{eqn | l = x \in F_\eta
      | o = \implies
      | r = x \in E_\eta
}}
{{eqn | l = x \in F_\zeta
      | o = \implies
      | r = x \notin E_\zeta
}}
{{end-eqn}}
If $\zeta < \eta$, then:
{{begin-eqn}}
{{eqn | l = x \in F_\zeta
      | o = \implies
      | r = x \in E_\zeta
}}
{{eqn | l = x \in F_\eta
      | o = \implies
      | r = x \notin E_\eta
}}
{{end-eqn}}
So the sets $F_\eta, F_\zeta$ are disjoint. 
Thus $F$ is the disjoint union of sets equal to $E$:
:$\ds \bigcup_{\alpha \mathop \in I} E_\alpha = \bigsqcup_{\alpha \mathop \in I} F_\alpha$
{{qed}}
Theorem: Subset of Well-Founded Relation is Well-Founded

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a well-founded relation on $S$.
Let $\QQ$ be a subset of $\RR$.
Then $\QQ$ is also a well-founded relation on $S$.

Proof:
{{AimForCont}} $\struct {S, \QQ}$ is not a well-founded set.
By Infinite Sequence Property of Well-Founded Relation there exists an infinite sequence $\sequence {x_n}$ in $S$ such that:
:$\forall n \in \N: \tuple {x_{n + 1}, x_n} \in \QQ \text { and } x_{n + 1} \ne x_n$
But then because $\QQ \subseteq \RR$, it follows that:
:$\forall n \in \N: \tuple {x_{n + 1}, x_n} \in \QQ \implies \tuple {x_{n + 1}, x_n} \in \RR$
and it follows that:
:$\forall n \in \N: \tuple {x_{n + 1}, x_n} \in \RR \text { and } x_{n + 1} \ne x_n$
Hence by Infinite Sequence Property of Well-Founded Relation it follows that $\RR$ is not a well-founded relation on $S$.
The result follows by Proof by Contradiction.
{{Qed}}
Theorem: Rank Function Property of Well-Founded Relation

Let $\struct {S, \RR}$ be a relational structure.
Let $\struct {T, \prec}$ be a strictly well-ordered set.
Let there exist a rank function $\operatorname {rk}: S \to T$, that is:
:$\forall x, y \in S: \paren {x \ne y \text { and } \tuple {x, y} \in \RR} \implies \map {\operatorname {rk} } x \prec \map {\operatorname {rk} } y$
Then $\RR$ is a well-founded relation.

Proof:
{{AimForCont}} $\RR$ is not a well-founded relation.
From Infinite Sequence Property of Well-Founded Relation, there exists an infinite sequence $\sequence {a_n}$ of elements of $S$ such that:
:$\forall n \in \N: \paren {a_{n + 1} \mathrel \RR a_n} \text { and } \paren {a_{n + 1} \ne a_n}$
Let $A = \operatorname {rk} \sqbrk {\sequence {a_n} }$ denote the image of $\sequence {a_n}$ under $\operatorname {rk}$.
From Image is Subset of Codomain:
:$A \subseteq T$
Let $m \in A$ be the smallest element of $A$.
Such a smallest element exists by the fact that $T$ is well-ordered by $\prec$.
Let $a_k \in S$ such that $\map {\operatorname {rk} } {a_k} = m$.
Then $a_{k + 1} \mathrel \RR a_k$ {{hypothesis}}.
But then:
:$\map {\operatorname {rk} } {a_{k + 1} } \prec m$
by definition of $\operatorname {rk}$.
Both $\map {\operatorname {rk} } {a_{k + 1} } \in A$ and $m \in A$.
But $m$ is the smallest element of $A$ under $\prec$.
This contradicts $\map {\operatorname {rk} } {a_{k + 1} } \prec m$.
Hence by Proof by Contradiction our initial assumption that $\RR$ is not a well-founded relation was false.
Hence the result.
{{qed}}
Theorem: Set of Distributional Derivatives of Dirac Delta Distribution is Linearly Independent

Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Then for any $n \in \N$ the set of distributional derivatives $\set {\delta, \delta' \ldots, \delta^{\paren n} }$ is linearly independent in $\map {\DD'} \R$.

Proof:
{{AimForCont}} there exist scalars $c_0, c_1, \ldots, c_n \in \R$ such that:
:$\ds \sum_{i \mathop = 0}^n c_i \delta^{\paren i} = \mathbf 0$
where $\mathbf 0 : \map \DD \R \to 0$ is the zero distribution.
Let $\phi \in \map \DD \R$ be a test function.
Let $\lambda \in \R_{\mathop > 0}$
Let $\map {\phi_\lambda} x := \map \phi {\lambda x}$.
We have that $\phi_\lambda$ is a test function.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | r = \map {\mathbf 0} {\phi_\lambda}
}}
{{eqn | r = \map {\paren{\sum_{i \mathop = 0}^n c_i \delta^{\paren i} } } {\phi_\lambda}
}}
{{eqn | r = \sum_{i \mathop = 0}^n c_i \map {\delta^i} {\phi_\lambda}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \paren {-1}^i c_i \lambda^i \map {\phi^{\paren i} } 0
      | c = {{Defof|Distributional Derivative}}
}}
{{end-eqn}}
This has to hold for any $\lambda > 0$.
Hence $\paren \star$:
:$c_0 \map \phi 0 = \ldots = c_n \map {\phi^{\paren n} } 0 = 0$
We have that:
:$\forall \phi \in \map \DD \R : \forall x \in \R : \forall n \in \N : x^n \phi \in \map \DD \R$
By Leibniz's Rule in One Variable:
:$\ds \map {\paren {x^n \phi}^{\paren n} } 0 = \paren {-1}^n \binom n n n! \map \phi 0 \ne 0$
Using $x^n \phi$ as our test function in $\paren \star$ yields:
:$c_0 = \ldots = c_n = 0$
and we have a contradiction.
{{qed}}
Theorem: Derivatives of Moment Generating Function of Logistic Distribution

The $n$th derivative of $M_X$ is given by:
:$\ds {M_X}^{\paren n} = \map \exp {\mu t} \sum_{k \mathop = 0}^n \paren {-1}^k \dbinom n k \mu^{n - k} s^k \int_{\to 0}^{\to 1} \map {\ln^k} {\dfrac {1 - u} u} \paren {\dfrac {1 - u} u}^{-s t} \rd u$

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds {M_X}^{\paren n} = \map \exp {\mu t} \sum_{k \mathop = 0}^n \paren {-1}^k \dbinom n k \mu^{n - k} s^k \int_{\to 0}^{\to 1} \map {\ln^k} {\dfrac {1 - u} u} \paren {\dfrac {1 - u} u}^{-s t} \rd u$
Theorem: Representative of P-adic Number is Representative of Equivalence Class

Let $p$ be any prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $x \in \Q_p$.
Then for any sequence $\sequence{y_n}$ of the rational numbers $\Q$:
:$\sequence{y_n}$ is a representative of the $p$-adic number $x$ {{iff}} $\sequence{y_n}$ is a representative of the equivalence class $x$.

Proof:
By definition of the $p$-adic numbers:
:$\Q_p$ is quotient ring
By definition of a quotient ring:
:$\Q_p$ is a coset space
By definition of a coset space:
:Every $p$-adic number $x$ is an equivalence class
By definitions of a representative of a $p$-adic number and a representative of an equivalence class:
:for any sequence $\sequence{y_n}$ of the rational numbers $\Q$: 
::$\sequence{y_n}$ is a representative of the $p$-adic number $x$ {{iff}} $\sequence{y_n}$ is a representative of the equivalence class $x$.
{{qed}}
Category:P-adic Number Theory
07jswsrgcria5em2lxegt44brhkjnf4
Theorem: Distributional Partial Derivatives Commute

Let $T \in \map {\DD'} {\R^d}$ be a Schwartz distribution.
Then in the distributional sense:
:$\dfrac {\partial^2 T} {\partial x_i \partial x_j} = \dfrac {\partial^2 T} {\partial x_j \partial x_i}$
where:
:$i, j \in \N : 1 \le i, j \le d$

Proof:
Let $\phi \in \map \DD {\R^d}$ be a test function.
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\partial^2 T} {\partial x_i \partial x_j} } \phi
      | r = -\map {\dfrac {\partial T} {\partial x_j} } {\dfrac {\partial \phi} {\partial x_i} }
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = \map T {\dfrac {\partial^2 \phi} {\partial x_j \partial x_i} }
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = \map T {\dfrac {\partial^2 \phi} {\partial x_i \partial x_j} }
      | c = Clairaut's Theorem, {{Defof|Test Function}}
}}
{{eqn | r = - \map {\dfrac {\partial T} {\partial x_i} } {\dfrac {\partial \phi} {\partial x_j} }
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = \map {\dfrac {\partial^2 T} {\partial x_j \partial x_i} } \phi
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Real Arctangent Function is Order Embedding into Reals

The real arctangent function $\arctan: \R \to \R$ is an order embedding on the set of real numbers under the usual ordering.

Proof:
{{ProofWanted|straightforward but tedious. We should have Real Arctangent Function is Increasing for a start but we don't yet.}}
Theorem: Inclusion Mapping is Order Embedding

Let $\struct {S, \preccurlyeq_S}$ and $\struct {T, \preccurlyeq_T}$ be ordered sets such that $S \subseteq T$.
Let ${\preccurlyeq_S} = {\preccurlyeq_T} {\restriction_S}$ be the restriction of $\preccurlyeq_T$ to $S$.
Let $i_S: S \to T$ denote the inclusion mapping from $S$ to $T$:
:$\forall s \in S: \map {i_S} s = s$
Then $i_S$ is an order embedding.

Proof:
We have that Inclusion Mapping is Restriction of Identity.
Then we have that Identity Mapping is Order Isomorphism.
The result follows.
{{qed}}
Theorem: Non-Injective Mapping may be Strictly Order-Preserving and Order-Reversing

Let $\struct {S, \prec_1}$ and $\struct {T, \prec_2}$ be strictly ordered sets.
Let $\phi: S \to T$ be a mapping.
Let $\pi: S \to T$ be a mapping with the property that:
:$\forall x, y \in S: x \prec_1 y \iff \map \pi x \prec_2 \map \pi y$
Then it is not necessarily the case that $\pi$ is an injection.

Proof:
Proof by Counterexample:
Let $S = \set {\O, \set a, \set b, \set {a, b} }$ and $T = \set {1, 2, 3}$.
Let $\prec_1$ be the proper subset relation:
:$\forall x, y \in S: x \prec_1 y \iff x \subsetneq y$
Let $\prec_2$ be the usual strict ordering on the integers $1, 2, 3$:
:$\forall x, y \in T: x \prec_2 y \iff x < y$
Let $\pi = \set {\tuple {\O, 1}, \tuple {\set a, 2}, \tuple {\set b, 2}, \tuple {\set {a, b}, 3} }$.
By inspection it is seen that $\pi: S \to T$ is a mapping which is specifically not an injection, as $\map \pi {\set a} = \map \pi {\set b}$.
Equally by inspection it can be seen that:
:$\forall x, y \in S: x \prec_1 y \iff \map \pi x \prec_2 \map \pi y$
{{qed}}
Theorem: Strictly Order-Preserving and Order-Reversing Mapping on Strictly Totally Ordered Set is Injection

Let $\struct {S, \prec_1}$ and $\struct {T, \prec_2}$ be strictly totally ordered sets.
Let $\phi: S \to T$ be a mapping.
Let $\pi: S \to T$ be a mapping with the property that:
:$\forall x, y \in S: x \prec_1 y \iff \map \pi x \prec_2 \map \pi y$
Then $\pi$ is an injection.

Proof:
{{AimForCont}} $\pi$ is not an injection.
Hence:
:$\exists x, y \in S: \map \pi x = \map \pi y$
As $S$ is strictly totally ordered:
:$x \prec_1 y$ or $y \prec_1 x$
{{WLOG}}, let $x \prec_1 y$.
Then we have:
:$\map \pi x = \map \pi y$
But {{hypothesis}}:
:$\map \pi x \prec_2 \map \pi y$
Because $\prec_2$ is a strict ordering, it follows that:
:$\map \pi x \ne \map \pi y$
It follows by Proof by Contradiction that it cannot be the case that $\pi$ is not an injection.
Hence the result.
{{qed}}