avewright/proofwiki-math huggingface dataset:
Theorem: Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods/Necessary Condition

Let $\struct{S, \tau}$ be a $\struct{S, \tau}$ is a sober space.
For each $x \in S$, let:
:$\map \UU x$ denote the system of open neighborhoods of $x$ 
Then:
:for each completely prime filter $\FF$ in the complete lattice $\struct{\tau, \subseteq}$:
::$\exists ! x \in S : \FF = \map \UU x$

Proof:
Let $\FF$ be a completely prime filter of $\struct{\tau, \subseteq}$.
Let $W = \bigcup \set{U \in \tau : U \notin \FF}$.
By the contrapositive statement of the definition of completely prime filter:
:$W \notin \FF$
From Completely Prime Filter Induces Meet-Irreducible Open Set:
:$W$ is a meet-irreducible open set
By definition of sober space:
:$\exists ! x \in S : W = S \setminus \set x^-$
We have:
{{begin-eqn}}
{{eqn | q = \forall U \in \tau
      | l = U \notin \FF
      | o = \leadsto
      | r = U \subseteq W
      | c = Set is Subset of Union
}}
{{eqn | o = \leadsto
      | r = U \subseteq S \setminus \set x^-
      | c = As $W = S \setminus x^-$
}}
{{eqn | o = \leadstoandfrom
      | r = U \notin \map \UU x
      | c = Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
}}
{{end-eqn}}
We also have
{{begin-eqn}}
{{eqn | q = \forall U \in \tau
      | l = U \notin \map \UU x
      | o = \leadsto
      | r = U \subseteq S \setminus \set x^-
      | c = Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
}}
{{eqn | o = \leadsto
      | r = U \subseteq W
      | c = As $W = S \setminus x^-$
}}
{{eqn | o = \leadsto
      | r = U \notin \FF
      | c = {{Ordered-set-filter-axiom|3}} and $W \notin \FF$
}}
{{end-eqn}}
Hence:
:$\forall U \in \tau : U \notin \FF \iff U \notin \map \UU x$
From Biconditional Equivalent to Biconditional of Negations:
:$\forall U \in \tau : U \in \FF \iff U \in \map \UU x$
By definition of set equality:
:$\FF = \map \UU x$
From System of Open Neighborhoods are Equal Iff Singleton Closures are Equal:
:$x$ is unique
The result follows.
Theorem: Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods/Sufficient Condition

Let $\struct{S, \tau}$ be a topological space.
For each $x \in S$, let:
:$\map \UU x$ denote the system of open neighborhoods of $x$ 
For each completely prime filter $\FF$ in the complete lattice $\struct{\tau, \subseteq}$, let: 
:$\exists ! x \in S : \FF = \map \UU x$
Then $\struct{S, \tau}$ is a sober space.

Proof:
For each completely prime filter $\FF$ in the complete lattice $\struct{\tau, \subseteq}$, let: 
:$\exists ! x \in S : \FF = \map \UU x$
Let $W \in \tau$ be a meet-irreducible open set.
Let $\FF = \set{U \in \tau : U \nsubseteq W}$.
From Meet-Irreducible Open Set Induces Completely Prime Filter:
:$\FF$ is a completely prime filter
We have {{hypothesis}}:
:$\exists ! x \in S : \FF = \map \UU x$
We have:
{{begin-eqn}}
{{eqn | l = S \setminus \set x^-
      | o = \in
      | r = \tau \setminus \map \UU x
      | c = Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
}}
{{eqn | ll = \leadsto
      | l = S \setminus \set x^-
      | o = \in
      | r = \tau \setminus \FF
      | c = as $\map \UU x = \FF$
}}
{{eqn | ll = \leadsto
      | l = S \setminus \set x^-
      | o = \subseteq
      | r = W
      | c = Definition of $\FF$
}}
{{end-eqn}}
We also have:
{{begin-eqn}}
{{eqn | l = W
      | o = \notin
      | r = \FF
      | c = Definition of $\FF$
}}
{{eqn | ll = \leadsto
      | l = W
      | o = \notin
      | r = \map \UU x
      | c = as $\map \UU x = \FF$
}}
{{eqn | ll = \leadsto
      | l = W
      | o = \in
      | r = \tau \setminus \map \UU x
      | c = {{Defof|Set Difference}}
}}
{{eqn | ll = \leadsto
      | l = W
      | o = \subseteq
      | r = S \setminus \set x^-
      | c = Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
}}
{{end-eqn}}
By definition of set equality:
:$W = S \setminus \set x^-$
From System of Open Neighborhoods are Equal Iff Singleton Closures are Equal:
:$x$ is unique
The result follows.
Theorem: Prime whose Divisor Sum is Square is 3

There is exactly $1$ prime number whose divisor sum is a square number, and that is $3$:
:$\map {\sigma_1} 3 = 4$

Proof:
That $\map {\sigma_1} 3 = 4$ is shown at {{DSFLink|3}}.
It remains to be shown there are no more.
Let $n \in \N$ such that $\map {\sigma_1} n$ is square.
:$\map {\sigma_1} n = m^2$
Suppose $n$ is prime.
From Divisor Sum of Prime Number:
:$\map {\sigma_1} n = n + 1$
So we have:
{{begin-eqn}}
{{eqn | l = n + 1
      | r = m^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | r = m^2 - 1
      | c = 
}}
{{eqn | r = \paren {m + 1} \paren {m - 1}
      | c = Difference of Two Squares
}}
{{end-eqn}}
But $\paren {m + 1} \paren {m - 1}$ is prime {{iff}} $m - 1 = 1$, that is, $m = 2$.
That is the case covered by $\map {\sigma_1} 3 = 4$.
Hence the result.
{{qed}}
Category:Divisor Sum Function
Category:3
nazx9o3fkx2k753er6cc5t09mj17b01
Theorem: Linear Combination of Riemann-Stieltjes Integrals/Integrand

Let $f, g, \alpha$ be real functions that are bounded on $\closedint a b$.
Let $c_1, c_2 \in \R$.
Suppose that $f$ and $g$ are Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$ and:
:$\ds \int_a^b f \rd \alpha = A$
:$\ds \int_a^b g \rd \alpha = B$
Then, the real function $h : \closedint a b \to \R$ defined as:
:$\map h x = c_1 \map f x + c_2 \map g x$
is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$ and:
:$\ds \int_a^b h \rd \alpha = c_1 A + c_2 B$

Proof:
Let $\epsilon > 0$ be arbitrary.
By definition of the Riemann-Stieltjes integral, let $P'_\epsilon, P' '_\epsilon$ be subdivisions of $\closedint a b$ such that:
:For every $P$ finer than $P'_\epsilon$, $\size {\map S {P, f, \alpha} - A} < \dfrac \epsilon {\size {c_1} + \size {c_2} + 1}$
:For every $P$ finer than $P' '_\epsilon$, $\size {\map S {P, g, \alpha} - B} < \dfrac \epsilon {\size {c_1} + \size {c_2} + 1}$
Define $P_\epsilon = P'_\epsilon \cup P' '_\epsilon$ to be a subdivision that is finer than both $P'_\epsilon$ and $P' '_\epsilon$.
Let $P = {x_0, \dotsc, x_n} \supseteq P_\epsilon$ be an arbitrary subdivision that is finer than $P_\epsilon$.
Clearly, $P$ is also finer than $P'_\epsilon$ and $P' '_\epsilon$.
Finally, fix the $t_1, \dotsc, t_k$ for the following Riemann-Stieltjes sum.
We have:
{{begin-eqn}}
{{eqn | l = \map S {P, h, \alpha}
      | r = \sum_{k \mathop = 1}^n \map h {t_k} \paren {\map \alpha {x_k} - \map \alpha {x_{k - 1} } }
      | c = {{Defof|Riemann-Stieltjes Sum}}
}}
{{eqn | r = c_1 \sum_{k \mathop = 1}^n \map f {t_k} \paren {\map \alpha {x_k} - \map \alpha {x_{k - 1} } } + c_2 \sum_{k = 1}^n \map g {t_k} \paren {\map \alpha {x_k} - \map \alpha {x_{k - 1} } }
      | c = Linear Combination of Indexed Summations
}}
{{eqn | r = c_1 \map S {P, f, \alpha} + c_2 \map S {P, g, \alpha}
      | c = {{Defof|Riemann-Stieltjes Sum}}
}}
{{end-eqn}}
And so:
{{begin-eqn}}
{{eqn | l = \size {\map S {P, h, \alpha} - \paren {c_1 A + c_2 B} }
      | r = \size {\paren {c_1 \map S {P, f, \alpha} + c_2 \map S {P, g, \alpha} } - \paren {c_1 A + c_2 B} }
}}
{{eqn | r = \size {c_1 \paren {\map S {P, f, \alpha} - A} + c_2 \paren {\map S {P, g, \alpha} - B} }
}}
{{eqn | o = \le
      | r = \size {c_1} \size {\map S {P, f, \alpha} - A} + \size {c_2} \size {\map S {P, g, \alpha} - B}
      | c = Triangle Inequality for Real Numbers and Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le
      | r = \size {c_1} \frac \epsilon {\size {c_1} + \size {c_2} + 1} + \size {c_2} \frac \epsilon {\size {c_1} + \size {c_2} + 1}
      | c = Definitions of $P'_\epsilon$ and $P' '_\epsilon$
}}
{{eqn | r = \frac {\size {c_1} + \size {c_1} } {\size {c_1} + \size {c_2} + 1} \epsilon
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
As $\epsilon > 0$ was arbitrary, by the definition of the Riemann-Stieltjes integral:
:$\ds \int_a^b h \rd \alpha = c_1 A + c_2 B$
{{qed}}
Theorem: Riemann-Stieltjes Integral of Constant Integrand

Let $\alpha$ be a real function that is bounded on $\closedint a b$.
Let $f : \closedint a b \to \R$ be defined as:
:$\map f x = c$
for some $c \in \R$.
Then, $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$, and:
:$\ds \int_a^b f \rd \alpha = c \map \alpha b - c \map \alpha a$

Proof:
Let $\epsilon > 0$
Define $P_\epsilon = \set {a, b}$.
Let $P = \set {x_0, \dotsc, x_n}$ be a subdivision of $\closedint a b$ that is finer than $P_\epsilon$.
Then:
{{begin-eqn}}
{{eqn | l = \map S {P, f, \alpha}
      | r = \sum_{k \mathop = 1}^n \map f {t_k} \paren {\map \alpha {x_k} - \map \alpha {x_{k - 1} } }
      | c = {{Defof|Riemann-Stieltjes Sum}}
}}
{{eqn | r = \sum_{k \mathop = 1}^n \paren {c \map \alpha {x_k} - c \map \alpha {x_{k - 1} } }
      | c = Definition of $f$
}}
{{eqn | r = c \map \alpha {x_n} - c \map \alpha {x_0}
      | c = Telescoping Series
}}
{{eqn | r = c \map \alpha b - c \map \alpha a
      | c = {{Defof|Finite Subdivision}}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \size {\map S {P, f, \alpha} - \paren {c \map \alpha b - c \map \alpha a} }
      | r = \size {\paren {c \map \alpha b - c \map \alpha a} - \paren {c \map \alpha b - c \map \alpha a} }
      | c = Above
}}
{{eqn | r = 0
}}
{{eqn | o = <
      | r = \epsilon
      | c = Definition of $\epsilon$
}}
{{end-eqn}}
Therefore, by definition of the Riemann-Stieltjes integral:
:$\ds \int_a^b f \rd \alpha = c \map \alpha b - c \map \alpha a$
{{qed}}
Theorem: Sum of Riemann-Stieltjes Integrals on Adjacent Intervals

Let $a, b, c \in \R$.
Let $f, \alpha$ be real functions that are bounded on some closed interval containing $a, b, c$.
Suppose that two of the following three Riemann-Stieltjes integrals exist, with the limits of integration interpreted in the general sense:
:$\ds \int_a^b f \rd \alpha$
:$\ds \int_b^c f \rd \alpha$
:$\ds \int_c^a f \rd \alpha$
Then, the third exists as well, and:
:$\ds \int_a^b f \rd \alpha + \int_b^c f \rd \alpha + \int_c^a f \rd \alpha = 0$

Proof:
We have the following special cases:
Theorem: Riemann-Stieltjes Integral by Norm of Subdivision

Let $f, \alpha$ be real functions that are bounded on $\closedint a b$.
Suppose there exists some $A \in \R$ where, for every $\epsilon > 0$, there exists some $\delta_\epsilon > 0$ such that:
:For every finite subdivision $P$ of $\closedint a b$, if the norm $\norm P < \delta_\epsilon$, then:
::For every Riemann-Stieltjes sum $\map S {P, f, \alpha}$:
:::$\size {\map S {P, f, \alpha} - A} < \epsilon$
Then, $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$ and:
:$\ds \int_a^b f \rd \alpha = A$

Proof:
Let $\epsilon > 0$ be arbitrary.
By hypothesis, let $\delta_\epsilon > 0$ be such that, for every subdivision $P$ with $\norm P < \delta_\epsilon$:
:$\size {\map S {P, f, \alpha} - A} < \epsilon$
By Existence of Subdivision with Small Norm, let $P_\epsilon$ be a subdivision of $\closedint a b$ such that:
:$\norm {P_\epsilon} < \delta_\epsilon$
Let $P$ be a subdivision that is finer than $P_\epsilon$.
Then:
{{begin-eqn}}
{{eqn | l = \norm P
      | o = \le
      | r = \norm {P_\epsilon}
      | c = Norm of Refinement is no Greater than Norm of Subdivision
}}
{{eqn | o = <
      | r = \delta_\epsilon
      | c = Definition of $P_\epsilon$
}}
{{end-eqn}}
Thus, by hypothesis:
:$\size {\map S {P, f, \alpha} - A} < \epsilon$
But, since $P$ finer than $P_\epsilon$ and $\epsilon > 0$ were arbitrary:
:$\ds \int_a^b f \rd \alpha = A$
by definition of the Riemann-Stieltjes integral.
{{qed}}
Theorem: Riemann-Stieltjes Integral by Norm of Subdivision/Riemann Integral

Let $f$ be a real function that is bounded on $\closedint a b$.
Suppose $f$ is Riemann integrable on $\closedint a b$.
Let $\iota$ be the identity mapping on $\closedint a b$.
Then, $f$ is Riemann-Stieltjes integrable with respect to $\iota$ on $\closedint a b$ and:
:$\ds \int_a^b f \rd \iota = \int_a^b \map f x \rd x$
where the integral on the right is understood to denote the Riemann integral.

Proof:
Let $\epsilon > 0$ be arbitrary.
By definition of the Riemann integral, there exists some $\delta_\epsilon$ such that:
:For every finite subdivision $\Delta = \set {x_0, \dotsc, x_n}$ of $\closedint a b$, and every $C = \paren {c_i}_{1 \mathop \le i \mathop \le n}$ such that $c_i \in \closedint {x_{i - 1}} {x_i}$:
::If the norm $\norm \Delta < \delta_\epsilon$, then $\ds \size {\map S {f; \Delta, C} - \int_a^b \map f x \rd x} < \epsilon$
:where $\map S {f; \Delta, C}$ denotes a Riemann sum of $f$ for the subdivision $\Delta$.
Let $P = \set {x_0, \dotsc, x_n}$ be a finite subdivision of $\closedint a b$ such that $\norm P < \delta_\epsilon$.
Then:
{{begin-eqn}}
{{eqn | l = \map S {P, f, \iota}
      | r = \sum_{k \mathop = 1}^n \map f {t_k} \paren {\map \iota {x_k} - \map \iota {x_{k - 1} } }
      | c = {{Defof|Riemann-Stieltjes Sum}}, denoted by $\map S {P, f, \iota}$
}}
{{eqn | r = \sum_{k \mathop = 1}^n \map f {t_k} \paren {x_k - x_{k - 1} }
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | r = \map S {f; P, C}
      | c = {{Defof|Riemann Sum}}, with $C = \paren {t_1, \dotsc, t_n}$
}}
{{eqn | ll = \leadsto
      | l = \size {\map S {P, f, \iota} - \int_a^b \map f x \rd x}
      | r = \size {\map S {f; P, C} - \int_a^b \map f x \rd x}
}}
{{eqn | o = <
      | r = \epsilon
      | c = $\norm P < \delta_\epsilon$
}}
{{end-eqn}}
As $P$ with $\norm P < \delta_\epsilon$ and $\epsilon > 0$ were arbitrary, the result follows from Riemann-Stieltjes Integral by Norm of Subdivision.
{{qed}}
Category:Definite Integrals
Category:Riemann-Stieltjes Integral
qguuvcncoe8fet0vrjsn4910n4892sr
Theorem: Norm of Refinement is no Greater than Norm of Subdivision

Let $P$ be a finite subdivision of $\closedint a b$.
Let $P'$ be a refinement of $P$.
Then:
:$\norm {P'} \le \norm P$
where $\norm P$ denotes the norm of $P$.

Proof:
Let $P = \set {x_0, x_1, \dotsc, x_{n - 1}, x_n}$.
Let $P' = \set {y_0, y_1, \dotsc, y_{m - 1}, y_m}$.
By definition of refinement:
:$P \subseteq P'$
Therefore, every $x_i \in P'$.
Thus, every $i \in \set {0, 1, \dotsc, n - 1, n}$, define $k_i \in \set {0, 1, \dotsc, m - 1, m}$ such that:
:$y_{k_i} = x_i$
Now, for each $j \in \set {1, 2, \dotsc, m - 1, m}$, let $i_j$ be the smallest $i$ such that $k_i \ge j$.
Since $k_{i_j} \ge j$, it follows that $y_j \le y_{k_{i_j}}$.
Therefore, by definition of $k_i$:
:$y_j \le x_{i_j}$
{{AimForCont}} $k_{i_j - 1} > j - 1$.
Then, $k_{i_j - 1} \ge j$, contradicting the fact that $i_j$ is the smallest $i$ satisfying the property.
Therefore, by Proof by Contradiction, $k_{i_j - 1} \le j - 1$.
Hence, $x_{i_j - 1} = y_{k_{i_j - 1}} \le y_{j - 1}$.
Let $Z = \norm {P'}$ be the norm of $P'$.
By definition, there is some $j \in \set {1, 2, \dotsc, m - 1, m}$ such that:
:$y_j - y_{j - 1} = Z$
But from:
:$x_{i_j - 1} \le y_{j - 1} \le y_j \le x_{i_j}$
it follows that:
:$x_{i_j} - x_{i_j - 1} \ge y_j - y_{j - 1} = Z$
Therefore, by definition of the norm of $P$:
:$\norm P \ge Z = \norm {P'}$
{{qed}}
Category:Subdivisions (Real Analysis)
p9vq5ckksz2xle50qubgjnbvrprq5je
Theorem: Existence of Subdivision with Small Norm

Let $\closedint a b$ be a closed real interval.
Let $\epsilon > 0$ be a positive real number.
Then, there exists a finite subdivision $P$ of $\closedint a b$ such that:
:$\norm P < \epsilon$
where $\norm P$ denotes the norm of $P$.

Proof:
By the Axiom of Archimedes, choose $N \in \N$ such that:
:$N > \dfrac {b - a} \epsilon > 0$
For each $k \in \set {0, 1, \dotsc, N - 1, N}$, define:
:$x_k = a + \dfrac k N \paren {b - a}$
We have:
{{begin-eqn}}
{{eqn | l = x_0
      | r = a + \frac 0 N \paren {b - a}
      | c = Definition of $x_k$
}}
{{eqn | r = a
}}
{{eqn | l = x_N
      | r = a + \frac N N \paren {b - a}
      | c = Definition of $x_k$
}}
{{eqn | r = b
}}
{{eqn | l = x_k - x_{k - 1}
      | r = \paren {a + \frac k N \paren {b - a} } - \paren {a + \frac {k - 1} N \paren {b - a} }
      | c = Definition of $x_k$
}}
{{eqn | n = 1
      | r = \frac {b - a} N
}}
{{eqn | o = >
      | r = 0
}}
{{eqn | ll = \leadsto
      | l = x_{k - 1}
      | o = <
      | r = x_k
}}
{{end-eqn}}
Let $P = \set {x_0, x_1, \dotsc, x_{N - 1}, x_N}$.
From:
:$x_0 = a$
:$x_N = b$
:$\forall k \in \set {1, \dotsc, N}: x_{k - 1} < x_k$
it follows that $P$ is a finite subdivision of $\closedint a b$.
Now:
{{begin-eqn}}
{{eqn | l = \norm P
      | r = \max \set {x_k - x_{k - 1} : k \in \set {1, \dotsc, N} }
      | c = {{Defof|Norm of Subdivision}}
}}
{{eqn | r = \max \set {\frac {b - a} N}
      | c = $\paren 1$ holds for all $k$
}}
{{eqn | r = \frac {b - a} N
}}
{{eqn | o = <
      | r = \frac {b - a} {b - a} \epsilon
      | c = Definition of $N$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}{{qed}}
Category:Subdivisions (Real Analysis)
skhnezux326patfw4jjtfx25vuhg9p8
Theorem: Integers under Addition form Group

The set of integers under addition $\struct {\Z, +}$ forms a group.

Proof:
From Integers under Addition form Abelian Group, $\struct {\Z, +}$ forms an abelian group.
An abelian group is {{afortiori}} a group.
Hence the result.
{{qed}}
Theorem: Integration by Substitution/Riemann-Stieltjes Integral

Let $g$ be a real function that is continuous and strictly monotone on $\closedint a b$.
Let $\Bbb I = g \closedint a b$ be the image of $g$ under $\closedint a b$.
Let $f, \alpha$ be real functions that are bounded on $\Bbb I$.
Further suppose that $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\Bbb I$.
Let $h, \beta : \Bbb I \to \R$ be defined as:
:$\map h x = \map f {\map g x}$
:$\map \beta x = \map \alpha {\map g x}$
Then, $h$ is Riemann-Stieltjes integrable with respect to $\beta$ on $\Bbb I$ and:
:$\ds \int_a^b h \rd \beta = \int_{\map g a}^{\map g b} f \rd \alpha$

Proof:
We have the following special cases:
Theorem: Continuous at Point iff Left-Continuous and Right-Continuous

Let $A \subseteq \R$ be an open set of real numbers.
Let $f : A \to \R$ be a real function.
Let $x_0 \in A$.
Then:
:$f$ is continuous at $x_0$
{{iff}}:
:$f$ is both left-continuous and right-continuous at $x_0$

Proof:
=== Necessary Condition ===
Suppose $f$ is continuous at $x_0$.
Then, by definition:
:$\ds \lim_{x \mathop \to x_0} \map f x = \map f {x_0}$
By Limit iff Limits from Left and Right:
:$\ds \lim_{x \mathop \to x_0^-} \map f x = \map f {x_0}$
:$\ds \lim_{x \mathop \to x_0^+} \map f x = \map f {x_0}$
Therefore, by definition, $f$ is both left-continuous and right-continuous at $x_0$.
{{qed|lemma}}
Theorem: Integers under Subtraction form Magma

The set of integers $\Z$ under the operation of subtraction forms a magma.

Proof:
Recall the definition of magma:
:$\struct {S, \circ}$ is a magma {{iff}} $\forall a, b \in S: a \circ b \in S$:
That is, a magma is closed under its operation.
Recall that the operation of subtraction is defined as:
:$\forall a, b \in \Z: a - b := a + \paren {-b}$
Recall that the Integers under Addition form Group.
Hence:
:$\forall b \in \Z: -b \in \Z$
and:
:$\forall a, b \in \Z: a + \paren {-b} \in \Z$
That is:
:$\forall a, b \in \Z: a - b \in \Z$
Hence the result by definition of magma.
{{qed}}
Theorem: Natural Numbers under Subtraction do not form Magma

The set of natural numbers $\N$ under the operation of subtraction does not form a magma.

Proof:
Proof by Counterexample:
Recall the definition of magma:
:$\struct {S, \circ}$ is a magma {{iff}} $\forall a, b \in S: a \circ b \in S$:
That is, a magma is closed under its operation.
Recall that the operation of natural number subtraction of $n - m$ is defined as:
:$n - m = p$
where $p \in \N$ such that $n = m + p$.
But this is defined only when $n \ge m$.
Consider $4 - 7$.
Then there exists no $p \in N$ such that $4 = 7 + p$.
Thus $4 - 7$ is not defined on $\N$.
Thus the algebraic structure $\struct {\N, -}$ is not closed.
Hence the algebraic structure $\struct {\N, -}$ is not a magma by definition.
{{qed}}
Theorem: Order of Hadamard Matrix

Let $\mathbf A$ be a Hadamard matrix.
Then the order of $\mathbf A$ must either be $2$ or an integer multiple of $4$.

Proof:
Let $\mathbf A$ be of order $n$.
{{ProofWanted}}
Theorem: Riemann-Stieltjes Integral with Step Integrator

Let $a < c < b$ be real numbers.
Let $f$ be a real function that is bounded on $\closedint a b$.
Let $\alpha$ be a real function on $\closedint a b$ such that:
:$\forall x \in \hointr a c: \map \alpha x = \map \alpha a$
:$\forall x \in \hointl c b: \map \alpha x = \map \alpha b$
Suppose that:
:Either $f$ is left-continuous at $c$, or $\map \alpha c = \map \alpha a$
:Either $f$ is right-continuous at $c$, or $\map \alpha c = \map \alpha b$
Then, $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$ and:
:$\ds \int_a^b f \rd \alpha = \map f c \paren {\map \alpha b - \map \alpha a}$

Proof:
Let $\epsilon > 0$ be arbitrary.
The construction of $P_\epsilon$ will depend on which of $f$ and $\alpha$ are continuous on which sides at $c$.
Theorem: Hankel Matrix is Symmetric

Let $\mathbf H$ be a Hankel matrix.
Then $\mathbf H$ is a symmetric matrix.

Proof:
Recall the definition of symmetric matrix:
$\mathbf A$ is '''symmetric''' {{iff}}:
:$\mathbf A = \mathbf A^\intercal$
where $\mathbf A^\intercal$ is the transpose of $\mathbf A$.
By definition of transpose of $\mathbf A$:
:$\mathbf A^\intercal_{i j}: = \mathbf A_{j i}$
Recall the definition of Hankel matrix:
{{:Definition:Hankel Matrix}}
That is, by definition of antidiagonal:
:$\forall i, j \in \closedint 1 n: \mathbf A_{i j}: = \mathbf A_{j i}$
Hence $\mathbf A^\intercal = \mathbf A$ and the result follows.
{{qed}}
Theorem: Differential Equation governing Simple Harmonic Motion

Let $B$ be a body undergoing simple harmonic motion in a straight line.
Then its motion can be described using the equation:
:$\dfrac {\d^2 x} {\d x^2} = -\omega^2 x$

Proof:
Consider the equation governing simple harmonic motion:
:$(1): \quad x = A \map \cos {\omega t + \phi}$
Differentiating $2$ times {{WRT|Differentiation}} $t$:
{{begin-eqn}}
{{eqn | n = 2
      | l = \dfrac {\d x} {\d t}
      | r = -\omega A \map \sin {\omega t + \phi}
      | c = Derivative of Cosine Function
}}
{{eqn | n = 3
      | l = \dfrac {\d^2 x} {\d t^2}
      | r = -\omega^2 A \map \cos {\omega t + \phi}
      | c = Derivative of Sine Function
}}
{{eqn | r = -\omega^2 x
      | c = 
}}
{{end-eqn}}
We have arrived at a ordinary differential equation of order $2$:
:$\dfrac {\d^2 x} {\d t^2} = -\omega^2 x$
{{qed}}
Theorem: Meet-Irreducible Open Set Induces Completely Prime Filter

Let $\struct{S, \tau}$ be a topological space.
Let:
:$W \in \tau : W \ne S : W$ is meet-irreducible
Let:
:$\FF = \set{U \in \tau : U \nsubseteq W}$.
Then:
:$\FF$ is a completely prime filter in the complete lattice $\struct{\tau, \subseteq}$

Proof:
=== $\FF$ satisfies {{Ordered-set-filter-axiom|1}} ===
We have {{hypothesis}}:
:$W \ne S$
From {{Open-set-axiom|3}}:
:$S \in \tau$
By definition of $\FF$:
:$S \in \FF$
By definition of empty set:
:$\FF \ne \O$
It follows that $\FF$ satisfies {{Ordered-set-filter-axiom|1}}.
{{qed|lemma}}
Theorem: Completely Prime Filter Induces Meet-Irreducible Open Set

Let $\struct{S, \tau}$ be a topological space.
Let $\FF$ be a completely prime filter in the complete lattice $\struct{\tau, \subseteq}$.
Let $W = \bigcup \set{U \in \tau : U \notin \FF}$.
Then:
:$W$ is a meet-irreducible open set

Proof:
By definition of completely prime filter:
:$\FF$ is a proper subset of $\tau$
Hence:
:$\set{U \in \tau : U \notin \FF} \ne \O$
By {{Open-set-axiom|1}}:
:$W \in \tau$
From Filter Contains Greatest Element:
:$S \in \FF$
By definition of completely prime filter:
:$W \notin \FF$
and so:
:$W \ne S$
Let $U_1, U_2 \in \tau$:
:$U_1 \cap U_2 \subseteq W$
By the contrapositive statement of {{Meet-semilattice-filter-axiom|1}}:
:$U_1 \cap U_2 \notin \FF$
as $W \notin \FF$
By the contrapositive statement of {{Meet-semilattice-filter-axiom|2}}:
:either $U_1 \notin \FF$ or $U_2 \notin \FF$
Hence:
:either $U_1 \subseteq W$ or $U_2 \subseteq W$
From Characterization of Meet-Irreducible Open Set, $W$ is a meet-irreducible open set.
{{qed}}