avewright/proofwiki-math huggingface dataset:
Theorem: Variance of Logistic Distribution

Let $X$ be a continuous random variable which satisfies the logistic distribution:
:$X \sim \map {\operatorname {Logistic} } {\mu, s}$
The variance of $X$ is given by:
:$\var X = \dfrac {s^2 \pi^2} 3$

Proof:
By Moment Generating Function of Logistic Distribution, the moment generating function of $X$ is given by: 
:$\ds \map {M_X} t = \map \exp {\mu t} \int_{\to 0}^{\to 1}  \paren {\dfrac {1 - u} u}^{-s t} \rd u$
for $\size t  < \dfrac 1 s$. 
From Variance as Expectation of Square minus Square of Expectation: 
:$\ds \var X = \expect {X^2} - \paren {\expect X}^2$
From Expectation of Logistic Distribution, we have:
:$\expect X = \mu$
From Moment Generating Function of Logistic Distribution: Second Moment: 
:$\ds \map { {M_X}' '} t = \map \exp {\mu t} \paren {\mu^2 \int_{\to 0}^{\to 1} \paren {\dfrac {1 - u} u}^{-s t} \rd u - 2 s \mu \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \paren {\dfrac {1 - u} u}^{-s t} \rd u + s^2 \int_{\to 0}^{\to 1} \map {\ln^2} {\dfrac {1 - u} u} \paren {\dfrac {1 - u} u}^{-s t} \rd u}$
Hence setting $t = 0$:
{{begin-eqn}}
{{eqn | l = \map { {M_X}''} 0
      | r = \mu^2 \int_{\to 0}^{\to 1} \rd u - 2 s \mu \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \rd u + s^2 \int_{\to 0}^{\to 1} \map {\ln^2} {\dfrac {1 - u} u} \rd u
}}
{{eqn | r = \mu^2 - 2 s \mu \paren {0 } + s^2 \paren {\dfrac {\pi^2} 3}
      | c = Definite Integral of Constant, {{Lemma|Expectation of Logistic Distribution|3|proof = yes}}, and {{Lemma|Variance of Logistic Distribution|4}}
}}
{{eqn | r = \mu^2 + \dfrac {s^2 \pi^2} 3
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn | l = \var X
      | r = \mu^2 + \dfrac {s^2 \pi^2} 3 - \mu^2
}}
{{eqn | r = \dfrac {s^2 \pi^2} 3
}}
{{end-eqn}}
{{qed}}
Theorem: P-adic Numbers form Completion of Rational Numbers with P-adic Norm

Let $p$ be a prime number.
Let $\norm {\,\cdot\,}^\Q_p$ be the $p$-adic norm on the rationals $\Q$.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Then $\struct {\Q_p, \norm {\,\cdot\,}_p}$ is a completion of $\struct {\Q, \norm {\,\cdot\,}^\Q_p}$

Proof:
Let $\norm {\,\cdot\,}^\Q_p$ be the $p$-adic norm on the rationals $\Q$.
From $p$-adic Norm on Rational Numbers is Non-Archimedean Norm:
:$\struct{\Q, \norm {\,\cdot\,}^\Q_p}$ is a valued field with non-Archimedean norm $\norm {\,\cdot\,}_p$ 
By {{Defof|Field of P-adic Numbers|Field of $p$-adic Numbers}}:
:$\Q_p$ is the quotient ring $\CC \, \big / \NN$
where:
:$\CC$ is the commutative ring of Cauchy sequences over $\struct {\Q, \norm {\,\cdot\,}^\Q_p}$.
and
:$\NN$ is the set of null sequences in $\struct {\Q, \norm {\,\cdot\,}^\Q_p}$.
By {{Defof|P-adic Norm on P-adic Numbers|$p$-adic Norm on $p$-adic Numbers}}:
:$\norm {\, \cdot \,}_p:\Q_p \to \R_{\ge 0}$ is defined by:
::$\ds \forall \eqclass{x_n}{} \in \Q_p: \norm {\eqclass{x_n}{} }_p = \lim_{n \mathop \to \infty} \norm{x_n}^\Q_p$
:where $\eqclass{x_n}{}$ denotes the left coset of $\sequence{x_n}$ in $\Q_p$
From Completion of Normed Division Ring:
:$\struct {\Q_p, \norm {\,\cdot\,}_p}$ is the completion of $\struct {\Q, \norm {\,\cdot\,}^\Q_p}$.
{{qed}}
Category:P-adic Number Theory
h1u3loo711ngtiob29qr74v3xh2usm4
Theorem: Kurtosis in terms of Non-Central Moments

Let $X$ be a random variable with expectation $\mu$ and standard deviation $\sigma$.
Then the kurtosis $\alpha_4$ of $X$ is given by: 
:$\ds \alpha_4 = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4}$

Proof:
{{begin-eqn}}
{{eqn | l = \alpha_4
      | r = \expect {\paren {\dfrac {X - \mu} \sigma}^4}
      | c = {{Defof|Kurtosis}}
}}
{{eqn | r = \dfrac {\expect {X^4 - 4 X^3 \mu + 6 X^2 \mu^2 - 4 X \mu^3 + \mu^4} } {\sigma^4}
      | c = Fourth Power of Difference
}}
{{eqn | r = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 4 \mu^3 \expect X + \mu^4} {\sigma^4}
      | c = Expectation is Linear
}}
{{eqn | r = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4}
      | c = $\mu = \expect X$
}}
{{end-eqn}}
{{qed}}
Category:Kurtosis
2qtecgtk8f3zl15jcm9qaxjy7a1n3bk
Theorem: Mutual Order Embedding does not imply Order Isomorphism

Let $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ be ordered sets.
Let it be possible for:
:$\struct {S_1, \preceq_1}$ to be embedded in $\struct {S_2, \preceq_2}$
:$\struct {S_2, \preceq_2}$ to be embedded in $\struct {S_1, \preceq_1}$.
Then it is not necessarily the case that $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ are isomorphic.

Proof:
Consider the ordered structures:
:$\struct {S_1, \preceq_1} := \struct {\R, \le}$
:$\struct {S_2, \preceq_2} := \struct {\hointl {-\dfrac \pi 2} {\dfrac \pi 2}, \le}$
From Real Arctangent Function is Order Embedding into Reals, $\struct {S_1, \preceq_1}$ can be embedded into $\struct {S_2, \preceq_2}$.
From Inclusion Mapping is Order Embedding,  $\struct {S_1, \preceq_2}$ can be embedded into $\struct {S_2, \preceq_1}$.
{{AimForCont}}  $\struct {\R, \le}$ and $\struct {\hointl {-\dfrac \pi 2} {\dfrac \pi 2}, \le}$ are isomorphic.
From Number of Maximal Elements is Order Property, $\struct {\R, \le}$ and $\struct {\hointl {-\dfrac \pi 2} {\dfrac \pi 2}, \le}$ have the same number of maximal elements.
But we note that:
:$\struct {\R, \le}$ has no maximal elements
:$\struct {\hointl {-\dfrac \pi 2} {\dfrac \pi 2}, \le}$ has one maximal element, that is $\dfrac \pi 2$.
It follows by Proof by Contradiction that $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ are not isomorphic.
{{qed}}
Theorem: Number of Minimal Elements is Order Property

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $\map m S$ be the number of minimal elements of $\struct {S, \preccurlyeq}$.
Then $\map m S$ is an order property.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be isomorphic ordered sets.
Hence let $\phi: S_1 \to S_2$ be an order isomorphism.
By definition of order property, we need to show that the number of minimal elements of $\struct {S_1, \preccurlyeq_1}$ is equal to the number of minimal elements of $\struct {S_2, \preccurlyeq_2}$.
Let $s \in \struct {S_1, \preccurlyeq_1}$ be a minimal element of $\struct {S_1, \preccurlyeq_1}$.
Then:
:$\forall x \in S_1: x \preccurlyeq_1 s \implies x = s$
Let $\map \phi y, \map \phi s \in S_2$ such that $\map \phi y \preccurlyeq_2 \map \phi s$.
Then as $\phi$ is an order isomorphism:
:$y \preccurlyeq_1 s$
and so as $s$ is a minimal element of $\struct {S_1, \preccurlyeq_1}$:
:$y = s$
From Order Embedding is Injection it follows that $\map \phi s$ is a minimal element of $\struct {S_2, \preccurlyeq_2}$.
Similarly, let $\map \phi s \in \struct {S_2, \preccurlyeq_2}$ be a minimal element of $\struct {S_2, \preccurlyeq_2}$.
Then:
:$\forall \map \phi y \in S_2: \map \phi y \preccurlyeq_2 \map \phi s \implies \map \phi y = \map \phi s$
Let $x \in S_1: x \preccurlyeq_1 s$.
Then as $\phi$ is an order isomorphism:
:$\map \phi x \preccurlyeq_2 \map \phi s$
and so as $\map \phi s$ is a minimal element of $\struct {S_2, \preccurlyeq_2}$:
:$\map \phi x = \map \phi s$
That is:
:$x = s$
and it follows that $s$ is a minimal element of $\struct {S_1, \preccurlyeq_1}$.
Hence:
:all minimal elements of $\struct {S_1, \preccurlyeq_1}$ are also minimal elements of $\struct {S_2, \preccurlyeq_2}$
and:
:all minimal elements of $\struct {S_2, \preccurlyeq_2}$ are also minimal elements of $\struct {S_1, \preccurlyeq_1}$
and the result follows.
{{qed}}
Theorem: Number of Maximal Elements is Order Property

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $\map M S$ be the number of maximal elements of $\struct {S, \preccurlyeq}$.
Then $\map M S$ is an order property.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be isomorphic ordered sets.
Hence let $\phi: S_1 \to S_2$ be an order isomorphism.
By definition of order property, we need to show that the number of maximal elements of $\struct {S_1, \preccurlyeq_1}$ is equal to the number of maximal elements of $\struct {S_2, \preccurlyeq_2}$.
Let $s \in \struct {S_1, \preccurlyeq_1}$ be a maximal element of $\struct {S_1, \preccurlyeq_1}$.
Then:
:$\forall x \in S_1: s \preccurlyeq_1 x \implies x = s$
Let $\map \phi y, \map \phi s \in S_2$ such that $\map \phi s \preccurlyeq_2 \map \phi y$.
Then as $\phi$ is an order isomorphism:
:$s \preccurlyeq_1 y$
and so as $s$ is a maximal element of $\struct {S_1, \preccurlyeq_1}$:
:$y = s$
From Order Embedding is Injection it follows that $\map \phi s$ is a maximal element of $\struct {S_2, \preccurlyeq_2}$.
Similarly, let $\map \phi s \in \struct {S_2, \preccurlyeq_2}$ be a maximal element of $\struct {S_2, \preccurlyeq_2}$.
Then:
:$\forall \map \phi y \in S_2: \map \phi s \preccurlyeq_2 \map \phi y \implies \map \phi y = \map \phi s$
Let $x \in S_1: x \preccurlyeq_1 s$.
Then as $\phi$ is an order isomorphism:
:$\map \phi s \preccurlyeq_2 \map \phi x$
and so as $\map \phi s$ is a maximal element of $\struct {S_2, \preccurlyeq_2}$:
:$\map \phi x = \map \phi s$
That is:
:$x = s$
and it follows that $s$ is a maximal element of $\struct {S_1, \preccurlyeq_1}$.
Hence:
:all maximal elements of $\struct {S_1, \preccurlyeq_1}$ are also maximal elements of $\struct {S_2, \preccurlyeq_2}$
and:
:all maximal elements of $\struct {S_2, \preccurlyeq_2}$ are also maximal elements of $\struct {S_1, \preccurlyeq_1}$
and the result follows.
{{qed}}
Theorem: Densely Ordered is Order Property

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be isomorphic ordered sets.
Let $\struct {S_1, \preccurlyeq_1}$ be densely ordered.
Then $\struct {S_2, \preccurlyeq_2}$ is also densely ordered.
That is, the property of being densely ordered is an order property.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be isomorphic ordered sets.
Let $\struct {S_1, \preccurlyeq_1}$ be densely ordered.
Let $a, b \in S_2$ such that $a \prec b$.
Then as $\phi$ is an order isomorphism:
:$\exists p, q \in S_1: a = \map \phi p, b = \map \phi q$
Then by definition of densely ordered:
:$\exists r \in S_1: p \prec r \prec q$
By definition of order isomorphism:
:$\map \phi p \prec \map \phi r \prec \map \phi q$
That is:
:$\exists c \in S_2: a \prec c \prec b$
where $c = \map \phi r$.
The result follows by definition of densely ordered.
{{qed}}
Theorem: Order Isomorphism is Symmetric

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.
{{qed}}
Theorem: Order Isomorphism is Transitive

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.
{{qed}}
Theorem: Collection of All Ordered Sets is not Set

Let $\mathrm {OS}$ denote the collection of all ordered sets.
Then $\mathrm {OS}$ is not a set.

Proof:
Let $C$ be the collection of all singletons:
:$\set {x: \exists y: x = \set y}$
Define a mapping $\map f {\set y} = \RR$ where $\RR$ is a reflexive relation on $\set y$.
By Reflexive Relation on Singleton is Well-Ordering, $\RR$ is an ordering.
Thus:
:$f: C \to \mathrm {OS}$
By Equality of Ordered Pairs:
:$\map f {y_1} = \map f {y_2} \implies y_1 = y_2$
Thus $f$ is an injection.
By definition of cardinality, $C$ is the collection of all sets which are equivalent to $\set \O$.
By Collection of Sets Equivalent to Set Containing Empty Set is Proper Class, $C$ is proper.
Thus, by Injection from Proper Class to Class, $\mathrm {OS}$ is proper.
Theorem: Order Sum of Well-Founded Orderings is Well-Founded Ordering

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.
{{qed}}
Theorem: Order Sum of Totally Ordered Sets is Totally Ordered

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.
{{qed}}
Theorem: Order Sum of Ordered Sets is Ordered

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:
Theorem: Order Isomorphism is Preserved by Order Sum

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ be ordered sets such that:
:$\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {T_1, \preccurlyeq_{1'} }$
:$\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} }$
Then the order sum $\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} } \oplus \struct {T_2, \preccurlyeq_{2'} }$.

Proof:
{{ProofWanted|tedium city or what}}
Theorem: Mixed Partial Derivative of Heaviside Step Function

Let $\tuple {x, y} \stackrel u {\longrightarrow} \map u {x, y}: \R^2 \to \R$ be the Heaviside step function.
Let $u := T_u$ be the Schwartz distribution associated with $u$.
Let $\delta_{\tuple {0, 0} } \in \map {\DD'} {\R^2}$ be the Dirac delta distribution.
Then in the distributional sense:
:$\dfrac {\partial^2 u} {\partial x \partial y} = \delta_{\tuple {0, 0}}$

Proof:
Let $\phi \in \map \DD {\R^2}$ be a test function with support on $\openint 0 a^2 := \openint 0 a \times \openint 0 a$ where $\times$ is the Cartesian product and $a > 0$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\partial^2 u}{\partial x \partial y} } \phi
      | r = - \map {\dfrac {\partial u}{\partial y} } {\dfrac {\partial \phi}{\partial x} }
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = \map u {\dfrac {\partial^2 \phi}{\partial y \partial x} }
      | c = {{Defof|Distributional Partial Derivative}}
}}
{{eqn | r = \iint_{\R^2} u \dfrac {\partial^2 \phi}{\partial y \partial x} \rd x \rd y
      | c = {{Defof|Schwartz Distribution}}
}}
{{eqn | r = \iint_{\R^2} u \dfrac {\partial^2 \phi}{\partial x \partial y} \rd x \rd y
      | c = Clairaut's Theorem, {{Defof|Test Function}}
}}
{{eqn | r = \int_0^a \int_0^a \dfrac {\partial^2 \phi}{\partial x \partial y} \rd x \rd y
      | c = {{Defof|Heaviside Step Function}}, $\phi$ is supported on $\openint 0 a^2$
}}
{{eqn | r = \int_0^a \paren {\map {\dfrac {\partial \phi} {\partial y} } {a, y} - \map {\dfrac {\partial \phi} {\partial y} } {0, y} } \rd y
      | c = Definite Integral of Partial Derivative
}}
{{eqn | r = - \int_0^a \map {\dfrac {\partial \phi} {\partial y} } {0, y} \rd y
      | c = $\phi$ is supported on $\openint 0 a^2$
}}
{{eqn | r = \map \phi {0, 0} - \map \phi {0, a}
}}
{{eqn | r = \map \phi {0, 0}
      | c = $\phi$ is supported on $\openint 0 a^2$
}}
{{eqn | r = \map {\delta_{\tuple {0, 0} } } \phi
      | c = {{Defof|Dirac Delta Distribution}}
}}
{{end-eqn}}
{{qed}}
Theorem: Order Type Addition is Well-Defined Operation

The addition operation on order types is well-defined.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ be ordered sets such that:
:$\struct {S_1, \preccurlyeq_1}$ is isomorphic to $\struct {T_1, \preccurlyeq_{1'} }$
:$\struct {S_2, \preccurlyeq_2}$ is isomorphic to $\struct {T_2, \preccurlyeq_{2'} }$
Let $\alpha := \map \ot {S_1, \preccurlyeq_1}$ and $\beta := \map \ot {S_2, \preccurlyeq_2}$ denote the order types of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ respectively.
Let $\alpha' := \map \ot {T_1, \preccurlyeq_{1'} }$ and $\beta' := \map \ot {T_2, \preccurlyeq_{2'} }$ denote the order types of $\struct {T_1, \preccurlyeq_{1'} }$ and $\struct {T_2, \preccurlyeq_{2'} }$ respectively.
It is required to show that:
:$\alpha + \beta$
is the same as:
:$\alpha' + \beta'$
We have that:
{{begin-eqn}}
{{eqn | l = \alpha + \beta
      | r = \map \ot {\struct {S_1, \preccurlyeq_1} \oplus \struct {S_2, \preccurlyeq_2} }
      | c = 
}}
{{eqn | r = \map \ot {\struct {T_1, \preccurlyeq_{1'} } \oplus \struct {T_2, \preccurlyeq_{2'} } }
      | c = Order Isomorphism is Preserved by Order Sum
}}
{{eqn | r = \alpha' + \beta'
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Dual of Well-Ordering is not necessarily Well-Ordering

Let $\struct {S, \preccurlyeq}$ be a well-ordered set.
Then its dual $\struct {S, \preccurlyeq}$ is not necessarily also a well-ordered set.

Proof:
Consider the ordered structure $\struct {\N, \le}$.
From the Well-Ordering Principle, $\struct {\N, \le}$ is a well-ordered set..
Consider the dual $\struct {\N, \ge}$ of $\struct {\N, \le}$.
Let this be expressed as:
:$\struct {\N, \preccurlyeq} := \struct {\N, \ge}$
so as to enhance the clarification of the nature of the ordering in question.
From Dual of Total Ordering is Total Ordering, $\struct {\N, \preccurlyeq}$ is a totally ordered set.
{{AimForCont}} $\struct {\N, \preccurlyeq}$ is a well-ordered set.
Then there exists a minimal element of $\struct {\N, \preccurlyeq}$:
:$\exists m \in \N: \forall x \in \N: x \preccurlyeq m \implies x = m$
But consider $y = m + 1$.
We have:
:$y \ge m$ but $y \ne m$
That is:
:$y \preccurlyeq m$ but $y \ne m$
and so $m$ cannot be a minimal element of $\struct {\N, \preccurlyeq}$ after all.
It follows that $\struct {\N, \preccurlyeq}$ is not a well-ordered set.
The result follows by Proof by Contradiction
{{qed}}
Theorem: Order Types of Duals of Isomorphic Sets are Equal

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let:
:$\map \ot {S_1, \preccurlyeq_1} = \map \ot {S_2, \preccurlyeq_2}$
where $\ot$ denotes the order type operator.
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}$.
Then:
:$\map \ot {S_1, \succcurlyeq_1} = \map \ot {S_2, \succcurlyeq_2}$

Proof:
{{ProofWanted|when it doesn't look quite so tedious}}
Theorem: Dual of Order Type is Well-Defined Mapping

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.
{{qed}}