avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
From the $1$st logarithm form:
$\quad \ds \int \frac {\d x} {x^2 - a^2} = \begin {cases} \dfrac 1 {2 a} \map \ln {\dfrac {a - x} {a + x} } + C & : \size x < a \\
& \\
\dfrac 1 {2 a} \map \ln {\dfrac {x - a} {x + a} } + C & : \size x > a \\
& \\
\text {undefined} & : \size x = a \end {cases}$
From Primitive of Reciprocal of a squared minus x squared: Logarithm Form: Lemma:
:$\map \ln {\dfrac {x - a} {x + a} }$ is defined {{iff}} $\size x > a$
:$\map \ln {\dfrac {a - x} {a + x} }$ is defined {{iff}} $\size x < a$
Let $\size x > a$.
Then $\map \ln {\dfrac {x - a} {x + a} }$ is defined.
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {x - a} {x + a}
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - a} {x + a}
      | r = \size {\dfrac {x - a} {x + a} }
      | c = 
}}
{{end-eqn}}
So the result holds for $\size x > a$.
Let $\size x < a$.
Then $\map \ln {\dfrac {a - x} {a + x} }$ is defined.
We have:
We have that:
{{begin-eqn}}
{{eqn | l = \dfrac {a - x} {a + x}
      | r = -\dfrac {x - a} {x + a}
      | c = 
}}
{{eqn | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {a - x} {a + x}
      | r = \size {\dfrac {x - a} {x + a} }
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
Let:
:$a \tan \theta = x$
for $\theta \in \openint {-\dfrac \pi 2} {\dfrac \pi 2}$.
From Shape of Tangent Function, this substitution is valid for all real $x$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = a \tan \theta 
      | c = from above
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d \theta}
      | r = a \sec^2 \theta
      | c = Derivative of Tangent Function
}}
{{eqn | ll= \leadsto
      | l = \int \frac 1 {x^2 + a^2} \rd x
      | r = \int \frac {a \ \sec^2 \theta} {a^2 \tan^2 \theta + a^2} \rd \theta
      | c = Integration by Substitution
}}
{{eqn | r = \frac a {a^2} \int \frac {\sec^2 \theta} {\tan^2 \theta + 1} rd \theta
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac 1 a \int \frac {\sec^2 \theta} {\sec^2 \theta} \rd \theta
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac 1 a \int \rd \theta
}}
{{eqn | r = \frac 1 a \theta + C
      | c = Integral of Constant
}}
{{end-eqn}}
As $\theta$ was stipulated to be in the open interval $\openint {-\dfrac \pi 2} {\dfrac \pi 2}$:
:$\tan \theta = \dfrac x a \iff \theta = \arctan \dfrac x a$
Thus:
:$\ds \int \frac 1 {x^2 + a^2} \rd x = \frac 1 a \arctan \frac x a + C$
{{qed|lemma}}
When $a = 0$, both $\dfrac x a$ and $\dfrac 1 a$ are undefined.
However, consider the limit of the above primitive as $a \to 0$:
{{begin-eqn}}
{{eqn | l = \lim_{a \mathop \to 0} \frac 1 a \arctan {\frac x a}
      | r = \lim_{a \mathop \to 0} \frac {\arctan {\frac x a} } a
}}
{{eqn | ll= \leadsto
      | r = \lim_{a \mathop \to 0} \frac {-x a^{-2} } {1 + \frac {x^2} {a^2} }
      | c = L'Hôpital's Rule, Derivative of Arctangent Function
}}
{{eqn | r = \lim_{a \mathop \to 0} \frac {a^{-2} } {a^{-2} } \frac {-x} {x^2 + a^2}
}}
{{eqn | r = -\frac 1 x
}}
{{end-eqn}}
This corresponds with the result:
:$\ds \int \frac 1 {x^2} \rd x = \frac {-1} x + C$
which follows from Primitive of Power.
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
We have that $x^2 + a^2$ is in the form $a x^2 + b x + c$, where $b^2 - 4 a c < 0$.
Thus from Primitive of $\dfrac 1 {a x^2 + b x + c}$ for $b^2 - 4 a c > 0$:
:$\ds \int \frac {\d x} {a x^2 + b x + c} = \frac 2 {\sqrt {4 a c - b^2} } \map \arctan {\frac {2 a x + b} {\sqrt {4 a c - b^2} } } + C$
setting $a := 1, b := 0, c := a^2$:
{{begin-eqn}}
{{eqn | l = \int \frac 1 {x^2 + a^2} \rd x
      | r = \dfrac 2 {\sqrt {4 a^2 - 0} } \map \arctan {\dfrac {2 x + 0} {\sqrt {4 a^2} } } + C
      | c = Primitive of $\dfrac 1 {a x^2 + b x + c}$
}}
{{eqn | r = \frac 1 a \arctan {\frac x a} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {x^2 + a^2}
      | r = \frac 1 a \int \frac {\d t} {t^2 + 1}
      | c = Substitution of $x \to a t$
}}
{{eqn | r = \frac 1 a \int \frac {\d t} {\paren {1 + i t} \paren {1 - i t} }
      | c = factoring
}}
{{eqn | r = \frac 1 {2 a} \paren {\int \frac {\d t} {1 + i t} + \int \frac {\d t} {1 - i t} }
      | c = {{Defof|Partial Fractions Expansion}}
}}
{{eqn | r = \frac 1 {2 a} \paren {i \map \ln {1 - i t} - i \map \ln {1 + i t} } + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \frac i {2 a} \map \ln {\frac {1 - i t} {1 + i t} } + C
      | c = Sum of Logarithms
}}
{{eqn | r = \frac 1 a \arctan \frac x a + C
      | c = Arctangent Logarithmic Formulation and substituting back $t \to \dfrac x a$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal

:$\ds \int \frac {\d x} x = \ln \size x + C$
for $x \ne 0$.

Proof:
Suppose $x > 0$.
Then:
:$\ln \size x = \ln x$
The result follows from Derivative of Natural Logarithm Function and the definition of primitive.
Suppose $x < 0$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \ln \size x
      | r = \dfrac \d {\d x} \map \ln {-x}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \frac 1 {-x} \cdot -1
      | c = Chain Rule for Derivatives and Derivative of Natural Logarithm Function, as $-x > 0$
}}
{{eqn | r = \frac 1 x
}}
{{end-eqn}}
and the result again follows from the definition of the primitive.
{{qed}}
Theorem: Powers of Commuting Elements of Semigroup Commute

:$\forall m, n \in \N_{>0}: \paren {\circ^m a} \circ \paren {\circ^n b} = \paren {\circ^n b} \circ \paren {\circ^m a}$

Proof:
The proof proceeds by the Principle of Mathematical Induction:
Let $\map P n$ be the proposition:
:$\paren {\circ^n a} \circ b = b \circ \paren {\circ^n a}$
Theorem: All Elements of Right Operation are Right Zeroes

Let $\struct {S, \to}$ be an algebraic structure in which the operation $\to$ is the right operation.
Then no matter what $S$ is, $\struct {S, \to}$ is a semigroup all of whose elements are right zeroes.
Thus it can be seen that any right zero in a semigroup is not necessarily unique.

Proof:
It is established in Structure under Right Operation is Semigroup that $\struct {S, \to}$ is a semigroup.
From the definition of right operation:
:$\forall x, y \in S: x \to y = y$
from which it can immediately be seen that all elements of $S$ are indeed right zeroes.
{{qed}}
From More than One Right Zero then No Left Zero, it also follows that there is no left zero.
Theorem: All Elements of Left Operation are Left Zeroes

Let $\struct {S, \leftarrow}$ be an algebraic structure in which the operation $\leftarrow$ is the left operation.
Then no matter what $S$ is, $\struct {S, \leftarrow}$ is a semigroup all of whose elements are left zeroes.
Thus it can be seen that any left zero in a semigroup is not necessarily unique.

Proof:
It is established in Structure under Left Operation is Semigroup that $\struct {S, \leftarrow}$ is a semigroup.
From the definition of left operation:
:$\forall x, y \in S: x \leftarrow y = x$
from which it can immediately be seen that all elements of $S$ are indeed left zeroes.
{{qed}}
From More than One Right Zero then No Left Zero, it also follows that there is no right zero.
Theorem: More than One Right Zero then No Left Zero

Let $\struct {S, \circ}$ be an algebraic structure.
If $\struct {S, \circ}$ has more than one left zero, then it has no right zero.
Likewise, if $\struct {S, \circ}$ has more than one right zero, then it has no left zero.

Proof:
Let $\struct {S, \circ}$ be an algebraic structure with more than one left zero.
Take any two of these, and call them $z_{L_1}$ and $z_{L_2}$, where $z_{L_1} \ne z_{L_2}$.
Suppose $\struct {S, \circ}$ has a right zero.
Call it $z_R$.
Then, by the behaviour of $z_R$, $z_{L_1}$ and $z_{L_2}$:
:$z_{L_1} = z_{L_1} \circ z_R = z_R$
:$z_{L_2} = z_{L_2} \circ z_R = z_R$
So $z_{L_1} = z_R = z_{L_2}$, which contradicts the supposition that $z_{L_1}$ and $z_{L_2}$ are different.
Therefore, in an algebraic structure with more than one left zero, there can be no right zero.
{{qed}}
The same argument can be applied to an algebraic structure with more than one right zero.
Category:Zero Elements
48vfjejkwqkxzeq6sxzvhdtg9doj2qd
Theorem: Left and Right Zero are the Same

Let $\struct {S, \circ}$ be an algebraic structure.
Let $z_L \in S$ be a left zero, and $z_R \in S$ be a right zero.
Then $z_L = z_R$, that is, both the left and right zero are the same, and are therefore a zero $z$.
Furthermore, $z$ is the ''only'' left and right zero for $\circ$.

Proof:
Let $\struct {S, \circ}$ be an algebraic structure such that:
:$\exists z_L \in S: \forall x \in S: z_L \circ x = z_L$
:$\exists z_R \in S: \forall x \in S: x \circ z_R = z_R$
Then $z_L = z_L \circ z_R = z_R$ by both the above, hence the result.
The uniqueness of the left and right zero is a direct result of Zero Element is Unique.
{{Qed}}
Theorem: Primitive of Cotangent Function

:$\ds \int \cot x \rd x = \ln \size {\sin x} + C$
where $\sin x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \cot x \rd x
      | r = \int \frac {\cos x} {\sin x} \rd x
      | c = {{Defof|Real Cotangent Function}}
}}
{{eqn | r = \int \frac {\paren {\sin x}'} {\sin x} \rd x
      | c = Derivative of Sine Function
}}
{{eqn | r = \ln \size {\sin x} + C
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
{{qed}}
Theorem: Inner Limit in Hausdorff Space by Open Neighborhoods

Let $\sequence {C_n}_{n \mathop \in \N}$ be a sequence of sets in a Hausdorff topological space $\struct {\XX, \tau}$.
Let $x \in \XX$.
Let $\map \mho x := \set {V \in \tau:\ x \in V}$ denote the set of open neighborhoods of $x$.
Let $\NN_\infty$ denote the set of cofinite subsets of $\N$:
:$\NN_\infty := \set {N \subset \N: \N \setminus N \text{ is finite} }$
Then the inner limit of $\sequence {C_n}_{n \mathop \in \N}$ is:
:$\ds \liminf_n C_n = \set {x \in \XX: \forall V \in \map \mho x: \exists N \in \NN_\infty: \forall n \in N: C_n \cap V \ne \O}$
or equivalently:
:$\ds \liminf_n C_n = \set {x \in \XX: \forall V \in \map \mho x: \exists N_0 \in \N: \forall n \ge N_0: C_n \cap V \ne \O}$

Proof:
If $x \in \liminf_n C_n$ then there exist a sequence $\sequence {x_k}_{n \mathop \in \N}$ such that $x_k \to x$ while:
:$x_k \in C_{n_k}$ 
and 
:$\sequence {n_k}_{k \mathop \in \N} \subseteq \N$ is a strictly increasing sequence of indices.
For any $V \in \map \mho x$ there exists $N_0 \in\N$ such that for all $i \ge N_0$: 
:$x_i \in V$
and:
:$x_i \in C_{n_i}$
Thus:
:$C_{n_i} \cap V \ne \O$
Therefore $x \in \set {x \in \XX: \forall V \in \map \mho x: \exists N_0 \in \N: \forall n \ge N_0: C_n \cap V \ne \O}$.
{{qed|lemma}}
Let $x \in \set {x \in \XX: \forall V \in \map \mho x: \exists N \in \NN_\infty: \forall n \in N: C_n \cap V \ne \O}$.
Thus:
:$\forall V \in \map \mho x: \exists N \in \NN_\infty: \forall n \in N: C_n \cap V \ne \O$
Then there exists a strictly increasing sequence:
:$\sequence {n_k}_{k \mathop \in \N} \subseteq \N$
such that for every $V \in \map \mho x$:
:$\exists x_k \in C_{n_k} \cap V$.
Hence $x_k \to x$ in the topology $\tau$.
{{qed}}
{{explain|A general increase in clarity needed.}}
Theorem: Lagrange Polynomial Approximation

Let $f: D \to \R$ be $n + 1$ times differentiable in an interval $I \subseteq \R$.
Let $x_0, \dotsc, x_n \in I$ be pairwise distinct points.
Let $P$ be the Lagrange Interpolation Formula of degree at most $n$ such that:
:$\forall i \in \set {0, \dotsc, n}: \map P {x_i} = \map f {x_i}$
Let $\map R x = \map f x - \map P x$.
Then, for every $x \in I$, there exists $\xi$ in the interval spanned by $x$ and $x_i$, $i = 0, \dotsc, n$, such that:
:$\map R x = \dfrac {\paren {x - x_0} \paren {x - x_1} \dotsm \paren {x - x_n} \map {f^{\paren {n + 1} } } \xi} {\paren {n + 1}!}$

Proof:
This proof is similar to the proof of Taylor's theorem with the remainder in the Lagrange form, and is also based on Rolle's Theorem.
Observe that:
:$\map R {x_i} = 0$ for $i = 0, \dotsc, n$
and that:
:$R^{\paren {n + 1} } = f^{\paren {n + 1} }$
{{WLOG}}, assume that $x$ is different from all $x_i$ for $i = 0, \dotsc, n$.
Let the function $g$ be defined by:
:$\map g t = \map R t - \dfrac {\paren {t - x_0} \paren {t - x_1} \dotsm \paren {t - x_n} \map R x} {\paren {x - x_0} \paren {x - x_1} \dotsm \paren {x - x_n} }$
Then $\map g {x_i} = 0$ for $i = 0, \dotsc, n$, and $\map g x = 0$.
Denote by $J$ the interval spanned by $x$ and $x_i$, $i = 0, \dotsc, n$.
Thus $g$ has at least $n + 2$ zeros in $J$.
{{Proofread}}
The Extended Rolle's Theorem is applied in $J$ successively to $g$, $g'$, $g' '$ and so on until $g^{\paren {n + 1} }$, which thus has at least one zero $\xi$ located between the two known zeros of $g^{\paren n}$ in $J$.
Then:
:$0 = \map {g^{\paren {n + 1} } } \xi = \map {f^{\paren {n + 1} } } \xi - \dfrac {\paren {n + 1}! \map R x} {\paren {x - x_0} \paren {x - x_1} \dotsm \paren {x - x_n} }$
and the formula for $\map R x$ follows.
{{qed}}
Theorem: Stabilizer of Subspace stabilizes Orthogonal Complement

Let $H$ be a finite-dimensional real or complex Hilbert space (that is, inner product space).
Let $t: H \to H$ be a normal operator on $H$.
Let $t$ stabilize a subspace $V$.
Then $t$ also stabilizes its orthogonal complement $V^\perp$.

Proof:
Let $p: H \to V$ be the orthogonal projection of $H$ onto $V$.
Then the orthogonal projection of $H$ onto $V^\perp$ is $\mathbf 1 - p$, where $\mathbf 1$ is the identity map of $H$.
The fact that $t$ stabilizes $V$ can be expressed as:
:$\paren {\mathbf 1 - p} t p = 0$
or:
:$p t p = t p$
The goal is to show that:
:$p t \paren {\mathbf 1 - p} = 0$
We have that $\tuple {a, b} \mapsto \map \tr {a b^*}$ is an inner product on the space of endomorphisms of $H$.
Here, $b^*$ denotes the adjoint operator of $b$.
Thus it will suffice to show that $\map \tr {x x^*} = 0$ for $x = p t \paren {\mathbf 1 - p}$.
This follows from a direct computation, using properties of the trace and orthogonal projections:
{{begin-eqn}}
{{eqn | l = x x^*
      | r = p t \paren {\mathbf 1 - p}^2 t^* p
      | c = 
}}
{{eqn | r = p t \paren {\mathbf 1 - p} t^* p
      | c = 
}}
{{eqn | r = p t t^* p - p t p t^* p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \tr {x x^*}
      | r = \map \tr {p t t^* p} - \map \tr {p t p t^* p}
      | c = 
}}
{{eqn | r = \map \tr {p^2 t t^*} - \map \tr {p^2 t p t^*}
      | c = 
}}
{{eqn | r = \map \tr {p t t^*} - \map \tr {\paren {p t p} t^*}
      | c = 
}}
{{eqn | r = \map \tr {p t t^*} - \map \tr {t p t^*}
      | c = 
}}
{{eqn | r = \map \tr {p t t^*} - \map \tr {p t^* t}
      | c = 
}}
{{eqn | r = \map \tr {p \paren {t t^* - t^*t} }
      | c = 
}}
{{eqn | r = \map \tr 0
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Hilbert Spaces
p17r6a1t00sw8693wociakiflkftxb5
Theorem: Primitive of Secant Function/Secant plus Tangent Form

:$\ds \int \sec x \rd x = \ln \size {\sec x + \tan x} + C$
where $\sec x + \tan x \ne 0$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \tan x + \sec x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac \d {\d x} \tan x + \frac \d {\d x} \sec x 
      | c = Linear Combination of Derivatives
}}
{{eqn | r = \sec^2 x + \frac \d {\d x} \sec x 
      | c = Derivative of Tangent Function
}}
{{eqn | r = \sec^2 x + \sec x \tan x 
      | c = Derivative of Secant Function
}}
{{eqn | r = \sec x \paren {\sec x + \tan x}
      | c = factorising
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sec x \rd x
      | r = \int \frac {\sec x \paren {\sec x + \tan x} } {\sec x + \tan x} \rd x
      | c = multiplying top and bottom by $\sec x + \tan x$
}}
{{eqn | r = \ln \size {\sec x + \tan x} + C
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Secant Function/Secant plus Tangent Form

:$\ds \int \sec x \rd x = \ln \size {\sec x + \tan x} + C$
where $\sec x + \tan x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \sec x \rd x 
      | r = \int \frac 1 {\cos x} \rd x
      | c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
We make the Weierstrass Substitution:
{{begin-eqn}}
{{eqn | l = u
      | r = \tan \frac x 2
}}
{{eqn | ll= \leadsto
      | l = \cos x
      | r = \frac {1 - u^2} {1 + u^2}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = \frac 2 {u^2 + 1}
}}
{{eqn | ll= \leadsto
      | l = \int \frac 1 {\cos x} \rd x
      | r = \int \frac {1 + u^2} {1 - u^2} \frac 2 {u^2 + 1} \rd u
}}
{{eqn | r = 2 \int \frac 1 {1 - u^2} \rd u
}}
{{eqn | r =  \ln \size {\frac {1 + u} {1 - u} } + C
      | c = Primitive of $\dfrac 1 {a^2 - u^2}$: Logarithm Form
}}
{{eqn | r = \ln \size {\frac {1 + \tan \frac x 2} {1 - \tan \frac x 2} } + C
}}
{{eqn | r = \ln \size {\sec x + \tan x} + C
      | c = One Plus Tangent Half Angle over One Minus Tangent Half Angle
}}
{{end-eqn}}
{{qed}}
Theorem: Subset of Natural Numbers is Cofinal iff Infinite

Consider the ordered set $\struct {\N, \le}$, where $\le$ is the usual ordering on the natural numbers.
Let $S \subseteq \N$.
Then $S$ is cofinal {{iff}} it is infinite.

Proof:
From Rule of Transposition, we may replace the ''only if'' statement by its contrapositive.
Therefore, the following suffices:
Theorem: Inner Limit in Hausdorff Space by Set Closures

Let $\struct {\XX, \tau}$ be a Hausdorff space.
Let $\sequence {C_n}_{n \mathop \in \N}$ be a sequence of sets in $\XX$.
Then:
:$\ds \liminf_n C_n = \bigcap_{N \mathop \in \NN_\infty^\#} \map \cl {\bigcup_{n \mathop \in N} C_n}$
where:
:$\cl$ denotes set closure
:$\NN_\infty^\#$ denotes the set of cofinal subsets of $\N$.

Proof:
$(1)$: Let:
:$\ds x \in \liminf_n \ C_n$
Let:
:$\Sigma \in \NN_\infty^\#$
Let $W$ be an open neighborhood of $x$. 
Then there exists $N_0 \in \N$ such that for all $n \ge N_0$ such that $n \in \Sigma$:
:$W \cap C_n \ne \O$
Thus:
:$\ds x \in \map \cl {\bigcup_{n \mathop \in \Sigma} C_n}$
$(2)$: Let:
:$\ds x \notin \liminf_n C_n$
Then there exists an open neighborhood of $x$.
Let $\map \mho x := \set {V \in \tau: x \in V}$ denote the set of open neighborhoods of $x$.
Let $W \in \map \mho x$ such that:
:$\Sigma_0 := \set {n \in \N: W \cap C_n = \O}$
is cofinal.
Then:
:$\ds x \notin \map \cl {\bigcup_{n \mathop \in \Sigma_0} C_n}$
This completes the proof.
{{qed}}
Theorem: At Most Two Horizontal Asymptotes

The graph of a real function has at most two horizontal asymptotes.

Proof:
Follows directly from the definition of a horizontal asymptote.
{{qed}}
Theorem: Ordinal is Transitive

Every ordinal is a transitive set.

Proof:
Let $\alpha$ be an ordinal by Definition 1:
{{:Definition:Ordinal/Definition 1}}
Thus $\alpha$ is {{apriori}} transitive.
{{qed}}
Theorem: Ordinal is Transitive

Every ordinal is a transitive set.

Proof:
Let $\alpha$ be an ordinal by Definition 2:
{{:Definition:Ordinal/Definition 2}}
Thus $\alpha$ is {{apriori}} transitive.
{{qed}}
Theorem: Ordinal is Transitive

Every ordinal is a transitive set.

Proof:
Let $\alpha$ be an ordinal by Definition 3.
{{:Definition:Ordinal/Definition 3}}
That is, $\alpha$ is a transitive set.
{{explain|Determine exactly what is being proved here}}
{{qed}}
Theorem: Ordinal is Transitive

Every ordinal is a transitive set.

Proof:
Let $\alpha$ be an ordinal by Definition 4.
{{:Definition:Ordinal/Definition 4}}
The proof proceeds by the Principle of Superinduction.
From Empty Class is Transitive we start with the fact that $0$ is transitive.
{{qed|lemma}}
Let $x$ be transitive.
From Successor Set of Transitive Set is Transitive:
:$x^+$ is transitive.
{{qed|lemma}}
We have that Class is Transitive iff Union is Subclass.
Hence the union of a chain of transitive sets is transitive.
{{qed|lemma}}
Hence the result by the Principle of Superinduction.
{{qed}}
Theorem: Strictly Well-Founded Relation has no Relational Loops

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

Proof:
Since $x_1, x_2, \ldots, x_n \in A$, there exists a $y$ such that $y = \set {x_1, x_2, \ldots, x_n}$.
Then $y$ is a non-empty subset of $A$.
So, by the definition of a strictly well-founded relation:
:$\exists w \in y: \forall z \in y: \neg w \prec z$
Now, suppose $x_1 \prec x_2 \land x_2 \prec x_3 \cdots \land x_n \prec x_1$.
But since the elements of $y$ are $x_1, x_2, \ldots, x_n$, then this contradicts the previous statement, since:
:$\forall w \in y: \exists z \in y: w \prec z$
Thus a founded relation has no relational loops.
{{explain|is a "founded relation" the same as a "foundational relation", that is a (strictly) well-founded relation? If so, use the same terminology throughout the entire page; if not, provide a definition for the former.}}
{{qed}}
Theorem: Epsilon Relation is Strictly Well-Founded

Let $\Epsilon$ denote the epsilon relation.
Then $\Epsilon$ is a strictly well-founded relation on every class $A$.

Proof:
{{NotZFC}}
By the {{Axiom-link|Foundation}}:
:$\forall S: \paren {\exists x: x \in S \implies \exists y \in S: \forall x \in S: \neg x \in y}$
That is, by Nonempty Class has Members:
:$\forall S: \paren {S \ne \O \implies \exists y \in S: \forall x \in S: \neg x \in y}$ 
This holds for all sets $S$ whose construction is based on the Zermelo-Fraenkel axioms.
We can weaken the antecedent of the above statement with this statement:
:$\forall S: \paren {\paren {S \ne \O \land S \subseteq A} \implies \exists y \in S: \forall x \in S: \neg x \in y}$
Note that this step does not require that $A$ be a set: it can be any class, even a proper class.
By definition, it follows that $\Epsilon$ is a strictly well-founded relation on every class $A$.
Category:Well-Founded Relations
Category:Axiom of Foundation
Category:Class Theory
b6914338b7lggajamzjs3h574802aqh
Theorem: Inner Limit in Normed Spaces by Open Balls

Let $\sequence {C_n}_{n \mathop \in \N}$ be a sequence of sets in a normed vector space $\struct {\XX, \norm {\, \cdot \,} }$.
Then the inner limit of $\sequence {C_n}_{n \mathop \in \N}$ is:
:$\ds \liminf_n C_n = \set {x: \forall \epsilon > 0: \exists N \in \NN_\infty: \forall n \in N: x \in C_n + B_\epsilon}$
where $B_\epsilon$ denotes the open $\epsilon$-ball of the space.
{{explain|What are $N$ and $\NN_\infty$ in this context? Also, what point is at the center of $B$? And what does $C_n + \epsilon B$ mean? For the latter one suspects $\cup$, but this needs to be checked. This page might need to be rewritten from a new perspective, as the original author was touchy about symbols used and departed {{ProofWiki}} in a rage when his notation was changed.}}

Proof:
The proof is an immediate result of Inner Limit in Hausdorff Space by Open Neighborhoods since the arbitrary open sets can be here replaced by open balls.
{{qed}}
Theorem: Inner Limit is Closed Set

Let $\struct {S, \tau}$ be a Hausdorff topological space.
Let $\sequence {C_n}_{n \mathop \in \N}$ be a sequence of sets in $S$.
Then the inner limit $\liminf_n C_n$ is a closed set.

Proof:
According to Inner Limit in Hausdorff Space by Set Closures, the inner limit is given by an arbitrary intersection of closed sets which is closed in the topology $\tau$.
{{qed}}
Category:Limits of Sequence of Sets
olfc9bqbfl4j70ofagsfnhu9jetdors
Theorem: Local Basis of Topological Vector Space

Let $\struct {\XX, \tau}$ be a topological vector space.
Let $0_\XX$ denote the zero vector of $\XX$.
Then there exists a local basis $\BB$ of $0_\XX$ with the following properties:
:$(1): \quad \forall W \in \BB: \exists V \in \BB$ such that $V + V \subseteq W$ (where the addition $V + V$ is meant in the sense of the Minkowski sum)
:$(2): \quad$ Every $W \in \BB$ is star-shaped (balanced)
:$(3): \quad$ Every $W \in \BB$ is absorbent.
:$(4): \quad \ds \bigcap_\BB W = \set {0_\XX}$.

Proof:
The proof will be carried out in various steps.
We will construct a collection of star-shaped neighborhoods of $0_\XX$.
Then we will show that it is indeed a local basis with the required properties.
Firstly we define the following set:
:$\BB_0 := \set {W \in \tau: 0 \in W, W \text{ is star-shaped} }$