avewright/proofwiki-math huggingface dataset:
Theorem: Summation of Products of n Numbers taken m at a time with Repetitions/Examples/Order 3

:$\ds \sum_{i \mathop = a}^b \sum_{j \mathop = a}^i \sum_{k \mathop = a}^j x_i x_j x_k = \dfrac { {S_1}^3} 6 + \dfrac {S_1 S_2} 2 + \dfrac {S_3} 3$
where:
:$\ds S_r := \sum_{k \mathop = a}^b {x_k}^r$

Proof:
We have that:
:$\ds \sum_{i \mathop = a}^b \sum_{j \mathop = a}^i \sum_{k \mathop = a}^j x_i x_j x_k = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le j_3 \mathop \le b} x_{j_1} x_{j_2} x_{j_3}$
From Summation of Products of n Numbers taken m at a time with Repetitions:
:$\ds \sum_{a \mathop \le j_1 \mathop \le \cdots \mathop \le j_m \mathop \le b} x_{j_1} \cdots x_{j_m} = \sum_{\substack {k_1, k_2, \ldots, k_m \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + \cdots \mathop + m k_m \mathop = m} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac { {S_2}^{k_2} } {2^{k_2} k_2 !} \cdots \dfrac { {S_m}^{k_m} } {m^{k_m} k_m !}$
where:
:$S_r = \ds \sum_{k \mathop = a}^b {x_k}^r$ for $r \in \Z_{\ge 0}$.
Setting $m = 3$:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le j_3 \mathop \le b} x_{j_1} x_{j_2} x_{j_3}
      | r = \sum_{\substack {k_1, k_2, k_3 \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + 3 k_3 \mathop = 3} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac { {S_2}^{k_2} } {2^{k_2} k_2 !} \dfrac { {S_3}^{k_3} } {3^{k_3} k_3 !}
      | c = 
}}
{{end-eqn}}
We need to find all sets of $k_1, k_2, k_3 \in \Z_{\ge 0}$ such that:
:$k_1 + 2 k_2 + 3 k_3 = 3$
Thus $\tuple {k_1, k_2, k_3}$ can be:
:$\tuple {3, 0, 0}$
:$\tuple {1, 1, 0}$
:$\tuple {0, 0, 1}$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le j_3 \mathop \le b} x_{j_1} x_{j_2} x_{j_3}
      | r = \dfrac { {S_1}^3 {S_2}^0 {S_3}^0} {\paren {1^3 \times 3!} \paren {2^0 \times 0!} \paren {3^0 \times 0!} } + \dfrac { {S_1}^1 {S_2}^1 {S_3}^0} {\paren {1^1 \times 1!} \paren {2^1 \times 1!} \paren {3^0 \times 0!} } + \dfrac { {S_1}^0 {S_2}^0 {S_3}^1} {\paren {1^0 \times 0!} \paren {2^0 \times 0!} \paren {3^1 \times 1!} }
      | c = 
}}
{{eqn | r = \dfrac { {S_1}^3} 6 + \dfrac {S_1 S_2} 2 + \dfrac {S_3} 3
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Summation of Product of Differences

:$\ds \sum_{1 \mathop \le i \mathop < j \mathop \le n} \paren {u_j - u_k} \paren {v_j - v_k} = n \sum_{j \mathop = 1}^n u_j v_j - \sum_{j \mathop = 1}^n u_j \sum_{j \mathop = 1}^n v_j$

Proof:
Take the Binet-Cauchy Identity:
:$\ds \paren {\sum_{i \mathop = 1}^n a_i c_i} \paren {\sum_{j \mathop = 1}^n b_j d_j} = \paren {\sum_{i \mathop = 1}^n a_i d_i} \paren {\sum_{j \mathop = 1}^n b_j c_j} + \sum_{1 \mathop \le i \mathop < j \mathop \le n} \paren {a_i b_j - a_j b_i} \paren {c_i d_j - c_j d_i}$
Make the following assignments:
{{begin-eqn}}
{{eqn | q = 1 \le i \le n
      | l = a_i
      | o = :=
      | r = u_i
}}
{{eqn | q = 1 \le i \le n
      | l = c_i
      | o = :=
      | r = v_i
}}
{{eqn | q = 1 \le j \le n
      | l = b_j
      | o = :=
      | r = 1
}}
{{eqn | q = 1 \le j \le n
      | l = d_j
      | o = :=
      | r = 1
}}
{{end-eqn}}
Then we have:
:$\ds \paren {\sum_{i \mathop = 1}^n u_i v_i} \paren {\sum_{j \mathop = 1}^n 1 \times 1} = \paren {\sum_{i \mathop = 1}^n u_i \times 1} \paren {\sum_{j \mathop = 1}^n 1 \times v_j} + \sum_{1 \mathop \le i \mathop < j \mathop \le n} \paren {u_i \times 1 - u_j \times 1} \paren {v_i \times 1 - v_j \times 1}$
and the result follows.
{{qed}}
Theorem: Product of Summations

:$\ds \prod_{j \mathop = 1}^n \sum_{i \mathop = 1}^m a_{i j} = \sum_{1 \mathop \le i_1 \mathop , \mathop \ldots \mathop , i_n \mathop \le m} a_{i_1 1} \cdots a_{i_n n}$

Proof:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop = 1}^n \sum_{i \mathop = 1}^m a_{i j}
      | r = \sum_{i \mathop = 1}^m a_{i 1} \sum_{i \mathop = 1}^m a_{i 2} \cdots  \sum_{i \mathop = 1}^m a_{i n}
      | c = {{Defof|Continued Product}}
}}
{{eqn | r = \sum_{i_1 \mathop = 1}^m a_{i_1 1} \sum_{i_2 \mathop = 1}^m a_{i_2 2} \cdots  \sum_{i_n \mathop = 1}^m a_{i_n n}
      | c = 
}}
{{eqn | r = \sum_{i_1 \mathop = 1}^m \sum_{i_2 \mathop = 1}^m \cdots \sum_{i_n \mathop = 1}^m a_{i_1 1} a_{i_2 2} \cdots a_{i_n n}
      | c = General Distributivity Theorem
}}
{{eqn | r = \sum_{1 \mathop \le i_1 \mathop , \mathop \ldots \mathop , i_n \mathop \le m} a_{i_1 1} \cdots a_{i_n n}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Summation of Powers over Product of Differences

:$\ds \sum_{j \mathop = 1}^n \begin{pmatrix} {\dfrac { {x_j}^r} {\ds \prod_{\substack {1 \mathop \le k \mathop \le n \\ k \mathop \ne j} } \paren {x_j - x_k} } } \end{pmatrix} = \begin{cases} 0 & : 0 \le r < n - 1 \\ 1 & : r = n - 1 \\ \ds \sum_{j \mathop = 1}^n x_j & : r = n \end{cases}$

Proof:
By Cauchy's Residue Theorem:
:$\ds \sum_{j \mathop = 1}^n \begin {pmatrix} {\dfrac { {x_j}^r} {\ds \prod_{\substack {1 \mathop \le k \mathop \le n \\ k \mathop \ne j} } \paren {x_j - x_k} } } \end {pmatrix} = \dfrac 1 {2 \pi i} \int \limits_{\size z \mathop = R} \dfrac {z^r \rd z} {\paren {z - z_1} \cdots \paren {z - z_n} }$
where $R > \size {z_1}, \ldots, \size {z_n}$.
The Laurent series of the integrand converges uniformly on $\size z = R$:
{{begin-eqn}}
{{eqn | o = 
      | r = z^{r - n} \paren {\dfrac 1 {1 - x_1 / z} } \cdots \paren {\dfrac 1 {1 - x_n / z} }
      | c = 
}}
{{eqn | r = z^{r - n} + \paren {x_1 + \cdots x_n} z^{r - n - 1} + \paren {x_1^2 + x_1 x_2 + \cdots} z^{r - n - 2} + \cdots
      | c = 
}}
{{end-eqn}}
On integrating term my term, everything vanishes except the coefficient of $z^{-1}$.
Thus:
:$\ds \sum_{\substack {j_1 \mathop + \mathop \cdots \mathop + j_n \mathop = r \mathop - n \mathop + 1 \\ j_1, \mathop \ldots j_n \mathop \ge 0} } {x_1}^{j_1} {x_2}^{j_2} \cdots {x_n}^{j_n}$
{{qed}}
Theorem: Summation by k of Product by r of x plus k minus r over Product by r less k of k minus r

:$\ds \sum_{k \mathop = 1}^n \paren {\dfrac {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne m} } \paren {x + k - r} } {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne k} } \paren {k - r} } } = 1$
where $1 \le m \le n$ and $x$ is arbitrary.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \paren {\dfrac {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne m} } \paren {x + k - r} } {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne k} } \paren {k - r} } }
      | r = \sum_{k \mathop = 1}^n \paren {\dfrac {k^{n - 1} + \map P k} {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne k} } \paren {k - r} } }
      | c = where $\map P k$ is a polynomial of degree $n - 2$
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {\dfrac {k^{n - 1} } {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne k} } \paren {k - r} } } + \sum_{k \mathop = 1}^n \paren {\dfrac {\map P k} {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne k} } \paren {k - r} } }
      | c = 
}}
{{eqn | r = 1 + 0
      | c = Summation of Powers over Product of Differences
}}
{{end-eqn}}
{{qed}}
Theorem: Summation by k of Product by r of x plus k minus r over Product by r less k of k minus r/Example

:$\dfrac {x \paren {x - 2} \paren {x - 3} } {\paren {-1} \paren {-2} \paren {-3} } + \dfrac {\paren {x + 1} \paren {x - 1} \paren {x - 2} } {\paren 1 \paren {-1} \paren {-2} } + \dfrac {\paren {x + 2} x \paren {x - 1} } {\paren 2 \paren 1 \paren {-1} } + \dfrac {\paren {x + 3} \paren {x + 1} x} {\paren 3 \paren 2 \paren 1 } = 1$

Proof:
This is an example of Summation by k of Product by r of x plus k minus r over Product by r less k of k minus r:
:$\ds \sum_{k \mathop = 1}^n \paren {\dfrac {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne m} } \paren {x + k - r} } {\ds \prod_{\substack {1 \mathop \le r \mathop \le n \\ r \mathop \ne k} } \paren {k - r} } } = 1$
where $n = 4$ and $m = 2$.
{{qed}}
Theorem: Sum of Elements in Inverse of Combinatorial Matrix

Let $C_n$ be the combinatorial matrix of order $n$ given by:
:$C_n = \begin{bmatrix}
x + y & y & \cdots & y \\
y & x + y & \cdots & y \\
\vdots & \vdots & \ddots & \vdots \\
y & y & \cdots & x + y
\end{bmatrix}$
Let $C_n^{-1}$ be its inverse, from Inverse of Combinatorial Matrix:
:$b_{i j} = \dfrac {-y + \delta_{i j} \paren {x + n y} } {x \paren {x + n y} }$
where $\delta_{i j}$ is the Kronecker delta.
The sum of all the elements of $C_n^{-1}$ is:
:$\ds \sum_{1 \mathop \le i, \ j \mathop \le n} b_{i j} = \dfrac n {x + n y}$

Proof:
All $n^2$ elements of $C_n^{-1}$ have a term $\dfrac {-y} {x \paren {x + n y} }$.
Further to this, the $n$ elements on the main diagonal contribute an extra $\dfrac {x + n y} {x \paren {x + n y} }$ to the total.
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{1 \mathop \le i, \ j \mathop \le n} b_{i j}
      | r = n^2 \dfrac {-y} {x \paren {x + n y} } + n \dfrac {x + n y} {x \paren {x + n y} }
      | c = 
}}
{{eqn | r = \dfrac {-n^2 y + n \paren {x + n y} } {x \paren {x + n y} }
      | c = 
}}
{{eqn | r = \dfrac {-n^2 y + n x + n^2 y} {x \paren {x + n y} }
      | c = 
}}
{{eqn | r = \dfrac {n x} {x \paren {x + n y} }
      | c = 
}}
{{eqn | r = \dfrac n {x + n y}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Elements in Inverse of Vandermonde Matrix

Let $V_n$ be the Vandermonde matrix of order $n$ given by:
:<nowiki>$V_n = \begin{pmatrix}
  x_1 & x_2 & \cdots & x_n \\
  x_1^2 & x_2^2 & \cdots & x_n^2 \\
\vdots & \vdots & \ddots & \vdots \\
  x_1^n & x_2^n & \cdots & x_n^n
\end{pmatrix}$</nowiki>
Let $V_n^{-1}$ be its inverse, from Inverse of Vandermonde Matrix:
:<nowiki>$b_{i j} = \begin {cases}
\paren {-1}^{j - 1} \paren {\dfrac {\ds \sum_{\substack {1 \mathop \le m_1 \mathop < \ldots \mathop < m_{n - j} \mathop \le n \\ m_1, \ldots, m_{n - j} \mathop \ne i} } x_{m_1} \cdots x_{m_{n - j} } } {x_i \ds \prod_{\substack {1 \mathop \le m \mathop \le n \\ m \mathop \ne i} } \paren {x_m - x_i} } } & : 1 \le  j < n \\
\qquad \qquad \qquad \dfrac 1 {x_i \ds \prod_{\substack {1 \mathop \le m \mathop \le n \\ m \mathop \ne i} } \paren {x_i - x_m} } & : j = n
\end{cases}$</nowiki>
The sum of all the elements of $V_n^{-1}$ is:
:$\ds \sum_{1 \mathop \le i, \ j \mathop \le n} b_{i j} = 1 - \prod_{k \mathop = 1}^n \paren {1 - \dfrac 1 {x_k} }$

Proof:
From Sum of Elements of Nonsingular Matrix, the sum of elements in $V_n^{-1}$ is:
:$1 - \map \det {V_n^{-1} } \map \det {V_n - J_n}$
The plan is to expand $\map \det {V_n - J_n}$ and simplify.
The method is efficiently communicated in the $3 \times 3$ case:
{{begin-eqn}}
{{eqn | l = \map \det {V_3 - J_3}
      | r = <nowiki>\map \det {\begin {matrix}
                    x_1 - 1 & x_2 - 1 & x_3 - 1 \\
                    x_1^2 - 1 & x_2^2 - 1 & x_3^2 - 1 \\
                    x_1^3 - 1 & x_2^3 - 1 & x_3^3 - 1 \\
                    \end {matrix} }</nowiki>
      | c = where $J_3$ is the $3 \times 3$ ones matrix
}}
{{eqn | r = <nowiki>\paren {x_1 - 1} \paren {x_2 - 1} \paren {x_3 - 1} \map \det {\begin {matrix}
                     1 & 1 & 1 \\
                     x_1+1 & x_2+1 & x_3+1 \\
                     x_1^2+x+1+1 & x_2^2+x_2+1 & x_3^2+x_3+1 \\
                     \end {matrix} }</nowiki> 
      | c =
Use $a^n - b^n$ factorization.
Effect of Elementary Row Operations on Determinant collects common column factors outside the determinant.
}}
{{eqn | r = <nowiki>\paren {x_1 - 1} \paren {x_2 - 1} \paren {x_3 - 1}
       \map \det {\begin {matrix}
       1 & 1 & 1 \\
       x_1 & x_2 & x_3 \\
       x_1^2 & x_2^2 & x_3^2 \\
       \end {matrix} }</nowiki> 
      | c = Effect of Elementary Row Operations on Determinant simplifies the determinant.
}}
{{end-eqn}}
The proof is completed by '''induction''' using the lemmas below.
Theorem: Hilbert Matrix is Cauchy Matrix

A Hilbert matrix is a special case of a Cauchy matrix.

Proof:
By definition of Hilbert matrix, the element $a_{i j}$ is:
:$a_{i j} = \dfrac 1 {i + j - 1}$
For all $i, j \in \Z$ such that $1 \le i \le n$ and $1 \le j \le n$, let:
:$x_i = i$
:$y_j = j - 1$
Then:
:$a_{i j} = \dfrac 1 {x_i + y_j}$
The result follows by definition of a Cauchy matrix.
{{qed}}
Theorem: Elements of Inverse of Hilbert Matrix are Integers

Let $H_n$ be the Hilbert matrix of order $n$:
:$\begin{bmatrix} a_{i j} \end{bmatrix} = \begin{bmatrix} \dfrac 1 {i + j - 1} \end{bmatrix}$
Consider its inverse $H_n^{-1}$.
All the elements of $H_n^{-1}$ are integers.

Proof:
From Inverse of Hilbert Matrix, $H_n^{-1} = \begin {bmatrix} b \end{bmatrix}_n$ can be specified as:
:$\begin{bmatrix} b_{i j} \end{bmatrix} = \begin{bmatrix} \dfrac {\paren {-1}^{i + j} \paren {i + n - 1}! \paren {j + n - 1}!} {\paren {\paren {i - 1}!}^2 \paren {\paren {j - 1}!}^2 \paren {n - i}! \paren {n - j}! \paren {i + j - 1} } \end{bmatrix}$
Thus:
{{begin-eqn}}
{{eqn | l = b_{i j}
      | r = \frac {\paren {-1}^{i + j} \paren {i + n - 1}! \paren {j + n - 1}!} {\paren {\paren {i - 1}!}^2 \paren {\paren {j - 1}!}^2 \paren {n - i}! \paren {n - j} ! \paren {i + j - 1} }
      | c = 
}}
{{eqn | r = \paren {\frac {\paren {-1}^{i + j} } {i + j - 1} } \paren {\frac {\paren {i + n - 1}!} {\paren {i - 1}! \, n!} } \paren {\frac {\paren {j + n - 1}!} {\paren {j - 1}! \, n!} } \paren {\frac {n! \, i} {i! \, \paren {n - i}!} } \paren {\frac {n! \, j} {j! \, \paren {n - j}! } }
      | c = 
}}
{{eqn | r = \frac {\paren {-1}^{i + j} i j} {i + j - 1} \binom {i + n - 1} n \binom {j + n - 1} n \binom n i \binom n j
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \paren {-1}^{i + j} j \binom {i + n - 1} {i - i} \binom {j + n - 1} {n - 1} \binom {i + j - 2} {n - i} \binom n j
      | c = 
}}
{{end-eqn}}
All of the factors of the above expression are integers, from Binomial Coefficient is Integer.
{{qed}}
Theorem: Sum of Elements in Inverse of Hilbert Matrix

Let $H_n$ be the Hilbert matrix of order $n$:
:$\begin{bmatrix} a_{i j} \end{bmatrix} = \begin{bmatrix} \dfrac 1 {i + j - 1} \end{bmatrix}$
Consider its inverse $H_n^{-1}$.
All the elements of $H_n^{-1}$ are integers.
The sum of all the elements $b_{i j}$ of $H_n^{-1}$ is:
:$\ds \sum_{1 \mathop \le i, \ j \mathop \le n} b_{i j} = n^2$

Proof:
From Hilbert Matrix is Cauchy Matrix, $H_n$ is a special case of a Cauchy matrix:
:$\begin{bmatrix} c_{i j} \end{bmatrix} = \begin{bmatrix} \dfrac 1 {x_i + y_j} \end{bmatrix}$
where:
:$x_i = i$
:$y_j = j - 1$
Then:
{{begin-eqn}}
{{eqn | l = \sum_{1 \mathop \le i, \ j \mathop \le n} b_{i j}
      | r = \sum_{k \mathop = 1}^n x_k + \sum_{k \mathop = 1}^n y_k
      | c = Sum of Elements in Inverse of Cauchy Matrix
}}
{{eqn | r = \sum_{k \mathop = 1}^n k + \sum_{k \mathop = 1}^n \paren {k - 1}
      | c = 
}}
{{eqn | r = 2 \sum_{k \mathop = 1}^n k - n
      | c = 
}}
{{eqn | r = n \paren {n + 1} - n
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = n^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Suprema of two Real Sets

Let $S$ and $T$ be real sets.
Let $S$ and $T$ admit suprema.
Then:
: $\sup S \le \sup T \iff \forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T: s < t + \epsilon$

Proof:
=== Necessary Condition ===
Let $\sup S \le \sup T$.
The aim is to establish that:
:$\forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T: s < t + \epsilon$
Let $\epsilon \in \R_{>0}$.
Let:
:$S' = \set {s \in S : \exists t \in T : s \le t}$
There are two cases for an $s \in S$:
:$s \in S'$, in other words: $\exists t \in T : s \le t$
and:
:$s \in S \setminus S'$, in other words: $\nexists t \in T : s \le t$
First, consider the case that $s \in S'$.
Let $s \in S'$.
Then $t \in T$ exists such that:
{{begin-eqn}}
{{eqn | l = s
      | o = \le
      | r = t
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \le
      | r = t < t + \epsilon
      | c = as $t < t + \epsilon$ is true
}}
{{eqn | ll= \leadsto
      | l = s
      | o = <
      | r = t + \epsilon
      | c = 
}}
{{end-eqn}}
We have found:
: $\forall \epsilon \in \R_{>0}: \forall s \in S': \exists t \in T: s < t + \epsilon$
Next, consider the second case, that $s \in S \setminus S'$.
Let $s \in S \setminus S'$.
Then:
{{begin-eqn}}
{{eqn | q = \nexists t \in T
      | l = s
      | o = \le
      | r = t
}}
{{eqn | ll= \leadsto
      | q = \forall t \in T
      | l = s
      | o = >
      | r = t
      | c = so, $s$ is an upper bound for $T$
}}
{{eqn | ll= \leadsto
      | l = s
      | o = \ge
      | r = \sup T
      | c = as (a) $s$ is an upper bound for $T$ and (b) $\sup T$ is the least upper bound of $T$
}}
{{eqn | ll= \leadsto
      | l = \sup S
      | o = \ge
      | r = s \ge \sup T
      | c = as $\sup S \ge s$ is true since (a) $\sup S$ is an upper bound for $S$ and (b) $s \in S$
}}
{{eqn | ll= \leadsto
      | l = \sup T
      | o = \ge
      | r = \sup S \ge s \ge \sup T
      | c = as $\sup S \le \sup T$ is true
}}
{{eqn | ll= \leadsto
      | l = \sup T
      | o = \ge
      | r = s \ge \sup T
}}
{{eqn | ll= \leadsto
      | l = s
      | r = \sup T
}}
{{end-eqn}}
So, $s = \sup T$ is the only element  of $S \setminus S'$.
A $t \in T$ exists such that:
{{begin-eqn}}
{{eqn | l = \sup T - t
      | o = <
      | r = \epsilon
      | c = by Supremum of Subset of Real Numbers is Arbitrarily Close
}}
{{eqn | ll= \leadsto
      | l = \sup T
      | o = <
      | r = t + \epsilon
}}
{{eqn | ll= \leadsto
      | l = s
      | o = <
      | r = t + \epsilon
      | c = as $s = \sup T$
}}
{{end-eqn}}
We have found:
: $\forall \epsilon \in \R_{>0}: \forall s \in S \setminus S': \exists t \in T: s < t + \epsilon$
We conclude by combining the results for the two cases:
: $\forall \epsilon \in \R_{>0}: \forall s \in S: \exists t \in T: s < t + \epsilon$
{{qed|lemma}}
Theorem: Sequential Continuity is Equivalent to Continuity in the Reals

Let $A \subseteq \R$ be a subset of the real numbers.
Let $c \in A$.
Let $f : A \to \R$ be a real function.
Then $f$ is continuous at $c$ {{iff}}:
:for each sequence $\sequence {x_n}$ in $A$ that converges to $c$, the sequence $\sequence {\map f {x_n} }$ converges to $\map f c$.

Proof:
=== Sufficient Condition ===
{{:Sequential Continuity is Equivalent to Continuity in the Reals/Sufficient Condition}}{{qed|lemma}}
Theorem: Rising Factorial as Quotient of Factorials

:$x^{\overline n} = \dfrac {\paren {x + n - 1}!} {\paren {x - 1}!} = \dfrac {\map \Gamma {x + n} } {\map \Gamma x}$

Proof:
{{begin-eqn}}
{{eqn | l = x^{\overline n}
      | r = \prod_{j \mathop = 0}^{n - 1} \paren {x + j}
      | c = {{Defof|Rising Factorial}}
}}
{{eqn | r = x \paren {x + 1} \paren {x + 2} \dotsm \paren {x + n - 1}
      | c = 
}}
{{eqn | r = \dfrac {\paren {x + n - 1}!} {\paren {x - 1}!}
      | c = {{Defof|Factorial}}
}}
{{eqn | r = \dfrac {\map \Gamma {x + n} } {\map \Gamma x}
      | c = Gamma Function Extends Factorial
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions for Alternating Bilinear Mapping on Ring of Characteristic Not 2

Let $R$ be a commutative ring.
Let $\struct {A_R, \oplus}$ be an algebra over $R$.
Let $R$ have a characteristic not equal to $2$.
Then the following definitions for alternating bilinear mappings are equivalent:
:$\oplus$ is an alternating bilinear mapping {{iff}} for all $a \in A_R$, $a \oplus a = 0$
:$\oplus$ is an alternating bilinear mapping {{iff}} for all $a, b \in A_R$, $a \oplus b + b \oplus a = 0$

Proof:
Let $\oplus$ be a bilinear mapping with the property that:
:$\forall a \in A_R: a \oplus a = 0$
Then for all $u, v \in A_R$:
{{begin-eqn}}
{{eqn | l = 0
      | r = \paren {u + v} \oplus \paren {u + v}
}}
{{eqn | r = u \oplus \paren {u + v} + v \oplus \paren {u + v}
}}
{{eqn | r = u \oplus v + v \oplus u = 0 
}}
{{end-eqn}}
{{qed|lemma}}
Let $\oplus$ be a bilinear mapping with the property that:
:$\forall a, b \in A_R: a \oplus b + b \oplus a = 0$
Let $u \in A_R$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | r = u \oplus u + u \oplus u
}} 
{{eqn | r = 2 \paren {u \oplus u}
}}
{{end-eqn}}
Because the characteristic of $R$ is not $2$:
:$u \oplus u = 0$
{{qed}}
Category:Alternating Bilinear Mappings
4bhj8h7l5ptpq95sivkdybwubzm25po
Theorem: Way Below if Between is Compact Set in Ordered Set of Topology

Let $T = \struct {S, \tau}$ be a topological space.
Let $L = \struct {\tau, \preceq}$ be an ordered set
where $\preceq \mathop = \subseteq\restriction_{\tau \times \tau}$
Let $x, y \in \tau$ such that:
:$\exists H \subseteq S: x \subseteq H \subseteq y \land H$ is compact
Then:
:$x \ll y$

Proof:
Let $D$ be a directed subset of $\tau$ such that:
:$y \preceq \sup D$
By proof of Topology forms Complete Lattice:
:$\ds y \subseteq \bigcup D$
By Subset Relation is Transitive:
:$\ds H \subseteq \bigcup D$
By definition:
:$D$ is open cover of $H$
By definition of compact:
:$H$ has finite subcover $\GG$ of $D$
By Directed iff Finite Subsets have Upper Bounds:
:$\exists d \in D: d$ is upper bound for $\GG$
By definitions of upper bound and of $\preceq$:
:$\forall z \in \GG: z \subseteq d$
By Union is Smallest Superset/Set of Sets:
:$\ds \bigcup \GG \subseteq d$
By definition of cover:
:$\ds H \subseteq \bigcup \GG$
By Subset Relation is Transitive:
:$x \subseteq d$
Thus by definition of $\preceq$:
:$x \preceq d$
Thus by definition of way below relation:
:$x \ll y$
{{qed}}
Theorem: Locally Compact iff Open Neighborhood contains Compact Set

Let $T = \struct {S, \tau}$ be a topological space.
Then:
:$T$ is locally compact
{{iff}}:
:$\forall U \in \tau, x \in U: \exists K \subseteq S: x \in K^\circ \land K \subseteq U \land K$ is compact
where $K^\circ$ denotes the interior of $K$.

Proof:
=== Sufficient Condition ===
Let $T$ be locally compact.
Let $U \in \tau, x \in U$.
Since $T$ is locally compact there exists a neighborhood basis $\BB$ of $x$ consisting of compact sets. 
From Set is Open iff Neighborhood of all its Points, $U$ is a neighborhood of $x$.
By definition of a neighborhood basis:
:$\exists K \in \BB : K \subseteq U$.
By definition of a neighborhood of $x$:
:$\exists V \in \tau : x \in V \subseteq K$
By definition of the interior of a subset then:
:$x \in V \subseteq K^\circ$
Thus
:$\exists K \subseteq S: x \in K^\circ \land K \subseteq U \land K$ is compact
{{qed|lemma}}