avewright/proofwiki-math huggingface dataset:
Theorem: Quotient of Integers is Primitive Recursive

Let $\operatorname{quot}_\Z : \N^2 \to \N$ be defined as:
:$\map {\operatorname{quot}_\Z} {a_\Z, b_\Z} = \begin{cases}
q_\Z & : b \ne 0 \\
0 & : b = 0
\end{cases}$
where:
:$k_\Z$ denotes the code number for the integer $k$
:$q$ is the quotient of $a$ on division by $b$
Then $\operatorname{quot}_\Z$ is primitive recursive.

Proof:
By definition:
:$a = q b + r$
where $0 \le r < \size b$.
We will first show that $\operatorname{quot}_{\Z,\N} : \N^2 \to \N$ defined as:
:$\map {\operatorname{quot}_{\Z,\N}} {a_\Z, b} = \begin{cases}
q_\Z & : b \ne 0 \\
0 & : b = 0
\end{cases}$
with the difference being that $b \in \N$ instead of $\Z$.
If $a \ge 0$, we have $\operatorname{quot} : \N^2 \to \N$ from Quotient is Primitive Recursive.
If $a < 0$, we have:
{{begin-eqn}}
{{eqn | l = a
      | r = q b + r
}}
{{eqn | l = -a
      | r = -q b - r
}}
{{eqn | r = -\paren {q + 1} b - r + b
}}
{{eqn | l = -\paren {a + 1}
      | r = -\paren {q + 1} b + \paren {b - r - 1}
}}
{{end-eqn}}
As $0 \le r < b$, we have $0 \le b - r - 1 < b$.
Thus, $-\paren {q + 1}$ is the quotient of $-\paren {a + 1}$ on division by $b$, by definition.
Additionally, since $a < 0$, we have $-\paren {a + 1} = -a - 1 \ge 0$.
Therefore, we can use the Quotient is Primitive Recursive form again.
If $q' = - \paren {q + 1}$, then we have:
:$q = -q' + -1$
Putting it all together:
:$\map {\operatorname{quot}_{\Z,\N}} {a_\Z, b} = \begin{cases}
\paren {\map {\operatorname{quot}} {\size a, b}}_\Z & : b \ne 0 \land \neg \paren {a < 0} \\
\paren {-1 + -\map {\operatorname{quot}} {\map {\operatorname{pred}} {\size a}, b}}_\Z & : b \ne 0 \land a < 0 \\
0 & : b = 0
\end{cases}$
which is primitive recursive by:
* Definition by Cases is Primitive Recursive
* Quotient is Primitive Recursive
* Predecessor Function is Primitive Recursive
* Addition of Integers is Primitive Recursive
* Absolute Value of Integer is Primitive Recursive
* Code Number for Non-Negative Integer is Primitive Recursive
* Code Number for Non-Positive Integer is Primitive Recursive
* Constant Function is Primitive Recursive
* Set Operations on Primitive Recursive Relations
* Ordering Relations are Primitive Recursive
* Equality Relation is Primitive Recursive
* Set of Strictly Negative Integers is Primitive Recursive
Finally, we can define $\operatorname{quot}_\Z$.
Observe that:
:$a = q b + r \iff a = \paren {-q} \paren {-b} + r$
Thus:
:$q$ is the quotient of $a$ on division by $b$ {{iff}} $-q$ is the quotient of $a$ on division by $-b$
Therefore, we can reduce to the case above:
:$\map {\operatorname{quot}_\Z} {a_\Z, b_\Z} = \map {\sgn_\Z} b \times_\Z \map {\operatorname{quot}_{\Z,\N}} {a_\Z, \size b}$
which is primitive recursive by:
* Multiplication of Integers is Primitive Recursive
* Signum Function on Integers is Primitive Recursive
* Absolute Value of Integer is Primitive Recursive
{{qed}}
Category:Primitive Recursive Functions
r1zuys3mrk38rvhf8d0x6axu4o1yzo2
Theorem: Restriction of Restriction is Restriction

Let $\RR$ be a relation on $S \times T$.
Let $X \subseteq S$, $Y \subseteq T$.
Let $W \subseteq X$, $V \subseteq Y$.
Then:
:$\paren{\RR {\restriction_{X \times Y} } } {\restriction_{W \times V} } = \RR {\restriction_{W \times V} }$
That is, the restriction of $\RR {\restriction_{X \times Y} }$ to $W \times V$ is the restriction of $\RR$ to $W \times V$

Proof:
From Cartesian Product of Subsets:
:$W \times V \subseteq X \times Y$
We have:
{{begin-eqn}}
{{eqn | l = \paren{\RR {\restriction_{X \times Y} } } {\restriction_{W \times V} }
      | r = \RR {\restriction_{X \times Y} } \cap W \times V
      | c = {{Defof|Restriction of Relation}}
}}
{{eqn | r = \paren {\RR \cap X \times Y} \cap W \times V
      | c = {{Defof|Restriction of Relation}}
}}
{{eqn | r = \RR \cap \paren{X \times Y \cap W \times V}
      | c = Intersection is Associative
}}
{{eqn | r = \RR \cap W \times V
      | c = Intersection with Subset is Subset
}}
{{eqn | r = \RR {\restriction_{W \times V} }
      | c = {{Defof|Restriction of Relation}}
}}
{{end-eqn}}
{{qed}}
Category:Restrictions
o0qnzaeow2vzfvrs9xnvzkm2bzs1zgr
Theorem: Characterization of Generalized Hilbert Sequence Space/Necessary Condition

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $H^\alpha = \struct{A, d_2}$ be the generalized Hilbert sequence space of weight $\alpha$ where:
:$A$ denotes the set of all real-valued functions $x : I \to \R$ such that:
::$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
::$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $H = \struct{\ell^2, d_{\ell^2}}$ denote the Hilbert sequence space, where:
:$\ell^2$ denotes the real $2$-sequence space, that is, the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{n \mathop = 0}^\infty x_n^2$ is convergent
Let $x_1, x_2, \ldots, x_m \in A$.
Then:
there exists an enumeration $\set{j_0, j_1, j_2, \ldots}$ of a countably infinite subset of $I$ such that $\forall k \in \closedint 1 m$:
::$(1)\quad\set{i \in I : \paren{x_k}_i \ne 0} \subseteq \set{j_0, j_1, j_2, \ldots}$
::$(2)\quad\sequence{\paren{x_k}_{j_n}} \in \ell^2$   
In which case:
:$\forall k \in \closedint 1 m : \ds \sum_{i \mathop \in I} \paren{\paren{x_k}_i}^2 = \sum_{n \mathop = 0}^\infty \paren{\paren{x_k}_{j_n}}^2$

Proof:
By definition of $A$:
:$\forall k \in \closedint 1 m : \set{i \in I : \paren{x_k}_i \ne 0}$ is countable
From Infinite Set has Countably Infinite Subset, let:
:$I' \subseteq I$ be countably infinite
Let:
:$J = I' \cup \ds \bigcup_{k \mathop = 1}^m \set{i \in I : \paren{x_k}_i \ne 0}$
From Countable Union of Countable Sets is Countable:
:$J$ is countable
From the contrapositive statement of Subset of Finite Set is Finite:
:$J$ is countably infinite
From Countably Infinite Set has Enumeration, let:
:$\set{j_0, j_1, j_2, \ldots}$ be an enumeration of $J$
From Set is Subset of Union:
:$\forall k \in \closedint 1 m : \set{i \in I : \paren{x_k}_i \ne 0} \subseteq \set{j_0, j_1, j_2, \ldots}$
By definition of $A$:
:$\forall k \in \closedint 1 m : \ds \sum_{i \mathop \in I} \paren{x_k}_i^2$ converges
We have:
{{begin-eqn}}
{{eqn | q = \forall k \in \closedint 1 m
      | l = \ds \sum_{i \mathop \in I} \paren{x_k}_i^2
      | r = \sum_{i \mathop \in I} \size{\paren{x_k}_i^2}
      | c = Square of Real Number is Non-Negative and {{Defof|Absolute Value}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \size{\paren{\paren{x_k}_{j_n} }^2}
      | c = Generalized Sum with Countable Non-zero Summands
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren{\paren{x_k}_{j_n} }^2
      | c = Square of Real Number is Non-Negative and {{Defof|Absolute Value}}
}}
{{end-eqn}}
Hence:
:$\forall k \in \closedint 1 m : \sequence{\paren{x_k}_{j_n}} \in \ell^2$
Theorem: Characterization of Generalized Hilbert Sequence Space/Sufficient Condition

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $H^\alpha = \struct{A, d_2}$ be the generalized Hilbert sequence space of weight $\alpha$ where:
:$A$ denotes the set of all real-valued functions $x : I \to \R$ such that:
::$(1)\quad \set{i \in I: x_i \ne 0}$ is countable
::$(2)\quad$ the generalized sum $\ds \sum_{i \mathop \in I} x_i^2$ is a convergent net.
Let $H = \struct{\ell^2, d_{\ell^2}}$ denote the Hilbert sequence space, where:
:$\ell^2$ denotes the real $2$-sequence space, that is, the set of all real sequences $\sequence {x_i}$ such that the series $\ds \sum_{n \mathop = 0}^\infty x_n^2$ is convergent
Let $x_1, x_2, \ldots, x_m : I \to \R$ be real-valued functions.
Let there exist an enumeration $\set{j_0, j_1, j_2, \ldots}$ of a countably infinite subset of $I$ such that $\forall k \in \closedint 1 m$:
::$(1)\quad\set{i \in I : \paren{x_k}_i \ne 0} \subseteq \set{j_0, j_1, j_2, \ldots}$
::$(2)\quad\sequence{\paren{x_k}_{j_n}} \in \ell^2$   
Then:
:$x_1, x_2, \ldots, x_m \in A$ 
In which case:
:$\forall k \in \closedint 1 m : \ds \sum_{i \mathop \in I} \paren{\paren{x_k}_i}^2 = \sum_{n \mathop = 0}^\infty \paren{\paren{x_k}_{j_n}}^2$

Proof:
By definition of $\ell^2$:
:$\forall k \in \closedint 1 m : \ds \sum_{n \mathop = 0}^\infty \paren{\paren{x_k}_{j_n}}^2 < \infty$
We have:
{{begin-eqn}}
{{eqn | q = \forall k \in \closedint 1 m
      | l = \sum_{n \mathop = 0}^\infty \paren{\paren{x_k}_{j_n} }^2
      | r = \sum_{n \mathop = 0}^\infty \size{\paren{\paren{x_k}_{j_n} }^2}
      | c = Square of Real Number is Non-Negative and {{Defof|Absolute Value}}
}}
{{eqn | r = \sum_{i \mathop \in I} \size{\paren{x_k}_i^2}
      | c = Generalized Sum with Countable Non-zero Summands
}}
{{eqn | r = \sum_{i \mathop \in I} \paren{x_k}_i^2
      | c = Generalized Sum with Countable Non-zero Summands
}}
{{end-eqn}}
Theorem: Angle Bisector Theorem/Exterior Angle

Let $\triangle ABC$ be a triangle.
Let $AB$ be produced past $A$ to $D$.
Let the external angle $CAD$ be bisected by $AE$ where $BE$ is $BC$ produced.
:400px
Then:
:$BE : EC = AB : AC$

Proof:
400px
Construct $CF$ parallel to the angle bisector $AE$.
By Parallelism implies Equal Corresponding Angles:
:$\angle AFC = \angle DAE$
By Parallelism implies Equal Alternate Angles:
:$\angle ACF = \angle CAE$
Given that $\angle DAC$ is bisected:
:$\angle DAE = \angle CAE$
By {{EuclidCommonNotionLink|1}}:
:$\angle AFC = \angle ACF$
By Triangle with Two Equal Angles is Isosceles:
:$\triangle AFC$ is isosceles
By the definition of isosceles triangle:
:$AF = AC$
By Parallelism implies Equal Corresponding Angles:
:$\angle BAE = \angle BFC$
$\angle ABC$ is shared.
By Triangles with Two Equal Angles are Similar:
:$\triangle BFC \sim \triangle BAE$
By the definition of similar triangles:
:$AB : BE = AF : CE$
Substituting for $AF$:
:$AB : BE = AC : CE$
Rearrange to give:
:$AB : AC = BE : EC$
{{qed}}
Theorem: Angular Momentum of Particle moving with Constant Circular Motion

Let $P$ be a particle of mass $m$ moving:
:with constant speed $v$
:in a circle of radius $r$ about a point $O$.
Then the angular momentum has magnitude $m v r$.

Proof:
The angular momentum $\mathbf L$ of a $P$ with respect to a point is given by the formula: 
:$\mathbf L = \mathbf r \times \mathbf p$
where
:$\mathbf r$ is the position of $P$
:$\mathbf p$ is the linear momentum of $P$
We have that $P$ is moving in a circle of radius $r = \size {\mathbf r}$.
Define a coordinate system such that the origin is at the center of the circle and the $x y$-plane contains the circle.
Let $\theta$ be the angle between the positive $x$-axis and $\mathbf r$ measured in a counterclockwise direction.
Therefore, $\mathbf r$ can be represented as: 
:$\mathbf r = r \cos \theta \mathbf i + r \sin \theta \mathbf j$
The velocity $\mathbf v$ of $P$ can be expressed as:
{{begin-eqn}}
{{eqn | l = \mathbf v
      | r = \dfrac {\d \mathbf r} {\d t}
}}
{{eqn | r = \dfrac \d {\d t} (r \cos \theta \mathbf i + r \sin \theta \mathbf j)
}}
{{eqn | r = r \frac {\d \theta} {\d t} \paren {-\sin \theta \mathbf i + \cos \theta \mathbf j}
}}
{{end-eqn}}
Let the angular speed be:
:$\omega = \dfrac {\d \theta} {\d t}$ 
So:
:$\mathbf v = r \omega \paren {-\sin \theta \mathbf i + \cos \theta \mathbf j}$
Now substituting into the angular momentum equation: 
{{begin-eqn}}
{{eqn | l = \mathbf L
      | r = \mathbf r \times \mathbf p
}}
{{eqn | r = \paren {r \cos \theta \mathbf i + r \sin \theta \mathbf j} \times \paren {m r \omega \paren {-\sin \theta \mathbf i + \cos \theta \mathbf j} }
      | c = $\mathbf p = m \mathbf v$
}}
{{eqn | r = m r^2 \omega \paren {\cos \theta \mathbf i \times \cos \theta \mathbf j} + m r^2 \omega \paren {\sin \theta \mathbf j \times \paren {-\sin \theta \mathbf i} }
      | c = Vector Cross Product Operator is Bilinear and Cross Product of Parallel Vectors
}}
{{eqn | r = m r^2 \omega \paren {\cos^2 \theta + \sin^2 \theta} \mathbf k
      | c = Cross Product of Elements of Standard Ordered Basis
}}
{{eqn | r = m r^2 \omega \mathbf k
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
From Angular Speed of Particle in Circular Motion at Constant Speed: 
:$\omega = \dfrac v r$
Substituting $\omega$ into the angular momentum equation gives: 
:$\mathbf L = m r^2 \paren {\dfrac v r} \mathbf k = m v r \mathbf k$
Thus, the magnitude of the angular momentum $\mathbf L$ is:
:$L = m v r$
{{qed}}
Theorem: Composition of Sequentially Computable Real-Valued Functions is Sequentially Computable

Let $D \subseteq \R^n$ and $E \subseteq \R^m$ be subsets of real cartesian space.
Let $f : D \to \R$ be sequentially computable.
Let $g_1, g_2, \dotsc, g_n : E \to \R$ be sequentially computable.
Suppose that, for every $\bsx \in E$:
:$\tuple {\map {g_1} \bsx, \map {g_2} \bsx, \dotsc, \map {g_n} \bsx} \in D$
Then $h : E \to \R$ defined as:
:$\map h {x_1, \dotsc, x_m} = \map f {\map {g_1} {x_1, \dotsc, x_m}, \dotsc, \map {g_n} {x_1, \dotsc, x_m}}$
is sequentially computable.

Proof:
Let $\tuple {\sequence {x_{1,k}}_k, \dotsc, \sequence {x_{m,k}}_k}$ be an $m$-tuple of computable real sequences in $E$.
By definition of sequentially computable:
:$\sequence {\map {g_i} {x_{1,k}, \dotsc, x_{m,k}}}_k$ is sequentially computable
for every $1 \le i \le n$
Additionally, for every $k$:
:$\tuple {\map {g_1} {x_{1,k}, \dotsc, x_{m,k}}, \dotsc, \map {g_n} {x_{1,k}, \dotsc, x_{m,k}}} \in D$
by assumption.
Therefore:
:$\tuple {\sequence {\map {g_1} {x_{1,k}, \dotsc, x_{m,k}}}_k, \dotsc, \sequence {\map {g_n} {x_{1,k}, \dotsc, x_{m,k}}}_k}$
is an $n$-tuple of computable real sequences in $D$.
Hence, by definition of sequentially computable:
:$\sequence {\map f {\map {g_1} {x_{1,k}, \dotsc, x_{m,k}}, \dotsc, \map {g_n} {x_{1,k}, \dotsc, x_{m,k}}}}_k$
is computable.
But, for every $k \in \N$:
:$\map f {\map {g_1} {x_{1,k}, \dotsc, x_{m,k}}, \dotsc, \map {g_n} {x_{1,k}, \dotsc, x_{m,k}}} = \map h {x_{1,k}, \dotsc, x_{m,k}}$
Therefore:
:$\sequence {\map h {x_{1,k}, \dotsc, x_{m,k}}}_k$
is computable.
As $\tuple {\sequence {x_{1,k}}_k, \dotsc, \sequence {x_{m,k}}_k}$ was arbitrary, it follows that $h$ is sequentially computable by definition.
{{qed}}
Category:Computability Theory
b4exzmz9ieluhneo4xotb7fu3r6gw4t
Theorem: Composition of Computable Real-Valued Functions is Computable

Let $D \subseteq \R^n$ and $E \subseteq \R^m$ be subsets of real cartesian space.
Let $f : D \to \R$ be computable.
Let $g_1, g_2, \dotsc, g_n : E \to \R$ be computable.
Suppose that, for every $\bsx \in E$:
:$\tuple {\map {g_1} \bsx, \map {g_2} \bsx, \dotsc, \map {g_n} \bsx} \in D$
Then $h : E \to \R$ defined as:
:$\map h {x_1, \dotsc, x_m} = \map f {\map {g_1} {x_1, \dotsc, x_m}, \dotsc, \map {g_n} {x_1, \dotsc, x_m}}$
is computable.

Proof:
Follows immediately from:
* Composition of Sequentially Computable Real-Valued Functions is Sequentially Computable
* Composition of Computably Uniformly Continuous Real-Valued Functions is Computably Uniformly Continuous
{{qed}}
Category:Computability Theory
bhipvqt9fyp3vmilaala6eqa0y7ifej
Theorem: Bounded Generalized Sum is Absolutely Convergent

Let $V$ be a Banach space.
Let $\family {v_i}_{i \mathop \in I}$ be an indexed family of elements of $V$.
Let $\FF$ denote the set of finite subsets of $I$.
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} v_i$ is absolutely net convergent
{{iff}}
:there exists $M \in \R_{\mathop \ge 0}$ such that for all $F \in \FF$:
::the summation $\ds \sum_{i \mathop \in F} \norm{v_i} \le M$

Proof:
=== Necessary Condition ===
Let the generalized sum $\ds \sum_{i \mathop \in I} v_i$ be absolutely net convergent.
Let: 
:$M = \ds \sum_{i \mathop \in I} \norm{v_i}$
{{AimForCont}}
:$\exists F_0 \in \FF : \sum_{i \mathop \in F_0} \norm{v_i} > M$
Let:
:$(1) \quad \epsilon \in \R_{\mathop > 0} : \epsilon < \paren{\ds \sum_{i \mathop \in F_0} \norm{v_i} } - M$
By definition of absolutely net convergence:
:$(2) \quad \exists F \in \FF : \forall E \in \FF : E \supseteq F \implies \ds \size{\sum_{i \mathop \in E} \norm{v_i} - M} < \epsilon$
Let:
:$E = F \cup F_0$
From Set is Subset of Union:
:$E \supseteq F$
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop \in E} \norm{v_i}
      | o = < 
      | r = M + \epsilon
      | c = from $(2)$
}}
{{eqn | o = < 
      | r = \sum_{i \mathop \in F_0} \norm{v_i}
      | c = from $(1)$
}}
{{eqn | o = \le 
      | r = \sum_{i \mathop \in F_0} \norm{v_i} + \sum_{i \mathop \in E \setminus F_0} \norm{v_i}
      | c = {{NormAxiomVector|1}}
}}
{{eqn | r = \sum_{i \mathop \in E} \norm{v_i}
      | c = Summation over Union of Disjoint Finite Index Sets
}}
{{end-eqn}}
We have a contradiction, so it follows that:
:$\forall F \in \FF : \ds \sum_{i \mathop \in F} \norm{v_i} \le M$
{{qed|lemma}}
Theorem: Velocity of Point on Rotating Body

Let $B$ be a body undergoing rotational motion around an axis $A$.
Let the angular velocity of $B$ about $A$ be $\bsomega$.
Let $O$ be an arbitrary point on $A$.
Let $P$ be a point in $B$ whose position vector {{WRT}} $O$ is $\mathbf r$.
Then the velocity $\mathbf v$ of $P$ is given by:
:$\mathbf v = \bsomega \times \mathbf r$

Proof:
{{begin-eqn}}
{{eqn | l = \bsomega \times \mathbf r
      | r = \paren {\frac {\mathbf r \times \mathbf v} {\size {\mathbf r}^2} } \times \mathbf r
      | c = {{Defof|Angular Velocity}}
}}
{{eqn | r = \frac 1 {\size {\mathbf r}^2} \paren {\paren {\mathbf r \cdot \mathbf r} \mathbf v - \paren {\mathbf v \cdot \mathbf r} \mathbf r}
      | c = Lagrange's Formula/Corollary
}}
{{eqn | r = \frac {\mathbf r \cdot \mathbf r} {\size {\mathbf r}^2} \mathbf v - \frac {\mathbf v \cdot \mathbf r} {\size {\mathbf r}^2} \mathbf r
}}
{{eqn | r = \mathbf v - \frac {\mathbf v \cdot \mathbf r} {\size {\mathbf r}^2} \mathbf r
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \mathbf v
      | c = $\mathbf v \perp \mathbf r$ in rotational motion and Dot Product of Perpendicular Vectors
}}
{{end-eqn}}
{{qed}}
Theorem: Nagata-Smirnov Metrization Theorem/Lemma 1

:$\forall x \in S$ and $n \in \N$:
::the generalized sum $\ds \sum_{B \mathop \in \BB_n} \map {f_{\tuple {B, n} }^2} x$ converges

Proof:
Let $s \in S$ and $m \in \N$.
By definition of locally finite set of subsets:
:$\exists U \in \tau : s \in U : \set {B \in \BB_m : B \cap U \ne \O}$ is finite
Hence:
:$\set {B \in \BB_m : s \in B}$ is finite
It follows that:
:$\set {\tuple {B, m} \in I : \map {f_{\tuple {B, m} } } s \ne 0}$ is finite
From Generalized Sum with Finite Non-zero Summands:
:the generalized sum $\ds \sum_{B \mathop \in \BB_m} \map {f_{\tuple {B, m} }^2} s$ converges
The result follows.
{{qed}}
Category:Nagata-Smirnov Metrization Theorem
8a2py32n8n4lpo1v8nb3yqgeomf5ki9
Theorem: Nagata-Smirnov Metrization Theorem/Lemma 2

:for all $n \in \N$ and $x \in S$:
::the generalized sum $\ds \sum_{\tuple{B, k} \mathop \in I_n} \sqbrk{\dfrac 1 {\paren{\sqrt 2}^k} \dfrac {\map {f_{\tuple{B, k}}} x} {\sqrt {1 + \map {g_k} x}}}^2$ converges 
and:
:$\ds \sum_{\tuple{B, k} \mathop \in I_n} \sqbrk{\dfrac 1 {\paren{\sqrt 2}^k} \dfrac {\map {f_{\tuple{B, k}}} x} {\sqrt {1 + \map {g_k} x}}}^2 \le \sum_{m \mathop = n}^\infty \dfrac 1 {2^k}$

Proof:
Let $n \in \N$.
Let $x \in S$.
Let $\FF$ denote the set of finite subsets of $I_n$.
Let $F \in \FF$.
Hence:
:$\set{k \in \N : \exists B \in \BB_k : \tuple{B, k} \in F}$ is finite.
Let $\set{n_1, n_2, \ldots, n_m} = \set{k \in \N : \exists B \in \BB_k : \tuple{B, k} \in F}$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{\tuple{B, k} \mathop \in F} \sqbrk{\dfrac 1 {\paren{\sqrt 2}^k} \dfrac {\map {f_{\tuple{b, k} } } x} {\sqrt {1 + \map {g_k} x} } }^2
      | r = \sum_{\tuple{B, k} \mathop \in F} \sqbrk{\dfrac {\map {f^2_{\tuple{b, k} } } x} {2^n \paren{1 + \map {g_k} x} } }
      | c = squaring the terms to remove square roots
}}
{{eqn | r = \sum_{k \mathop = 1}^m \sqbrk{\sum_{\tuple{B, n_k} \mathop \in F} \dfrac {\map {f^2_{\tuple{b, n_k} } } x} {2^{n_k} \paren{1 + \map {g_{n_k} } x} } }
      | c = Summation over Union of Disjoint Finite Index Sets
}}
{{eqn | r = \sum_{k \mathop = 1}^m \sqbrk{ \dfrac 1 {2^{n_k} \paren{1 + \map {g_{n_k} } x} }  \ds \sum_{\tuple{B, n_k} \mathop \in F}  \map {f^2_{\tuple{b, n_k} } } x}
      | c = {{Real-number-axiom|D}}
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 1}^m \sqbrk{\dfrac 1 {2^{n_k} \paren{1 + \map {g_{n_k} } x} }  \ds \sum_{B \mathop \in \BB_{n_k} }  \map {f^2_{\tuple{b, n_k} } } x}
      | c = Absolutely Convergent Generalized Sum Converges to Supremum
}}
{{eqn | r = \sum_{k \mathop = 1}^m \dfrac {\map {g_{n_k} } x} {2^{n_k} \paren{1 + \map {g_{n_k} } x} }
      | c = definition of $g_{n_k}$
}}
{{eqn | o = <
      | r = \sum_{k \mathop = 1}^m \dfrac 1 {2^{n_k} }  
      | c = as $\map {g_{n_k} } x < 1 + \map {g_{n_k} } x$
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = n}^\infty \dfrac 1 {2^k}  
}}
{{eqn | o = <
      | r = \infty  
      | c = Sum of Infinite Geometric Sequence
}}
{{end-eqn}}
Since $F$ was arbitrary, it follows that:
:$\forall F \in \FF : \ds \sum_{\tuple{B, k} \mathop \in F} \sqbrk{\dfrac 1 {\paren{\sqrt 2}^k} \dfrac {\map {f_{\tuple{b, k} } } x} {\sqrt {1 + \map {g_k} x} } }^2 \le \sum_{k \mathop = n}^\infty \dfrac 1 {2^k}$
From Bounded Generalized Sum is Absolutely Convergent:
:the generalized sum $\ds \sum_{\tuple{B, k} \mathop \in I_n} \sqbrk{\dfrac 1 {\paren{\sqrt 2}^k} \dfrac {\map {f_{\tuple{B, k}}} x} {\sqrt {1 + \map {g_k} x}}}^2$ converges
and:
:$\ds \sum_{\tuple{B, k} \mathop \in I_n} \sqbrk{\dfrac 1 {\paren{\sqrt 2}^k} \dfrac {\map {f_{\tuple{B, k}}} x} {\sqrt {1 + \map {g_k} x}}}^2 \le \sum_{k \mathop = n}^\infty \dfrac 1 {2^k}$
{{qed}}
Category:Nagata-Smirnov Metrization Theorem
rteqq530rd1g7nvo6528g0nr1on88pw
Theorem: Continuous Image of Everywhere Dense Set is Everywhere Dense

Let $A_T = \struct {A, \tau_A}$ and $B_T = \struct {B, \tau_B}$ be topological spaces.
Let $f : A \to B$ be an everywhere continuous surjection.
Let $S \subseteq A$ be everywhere dense in $A_T$.
Then, $f \sqbrk S$ is everywhere dense in $B_T$.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {f \sqbrk S}^-
      | o = \supseteq
      | r = f \sqbrk {S^-}
      | c = Continuity Defined by Closure
}}
{{eqn | r = f \sqbrk A
      | c = {{Defof|Everywhere Dense|index = 1}}
}}
{{eqn | r = B
      | c = {{Defof|Surjection|index = 2}}
}}
{{end-eqn}}
As $\paren {f \sqbrk S}^- \subseteq B$, by set equality:
:$\paren {f \sqbrk S}^- = B$
Therefore, $f \sqbrk S$ is everywhere dense in $B$ by definition.
{{qed}}
Category:Denseness
jibxl5y5uhetu7eer246qei7qrie8r7
Theorem: Cross Product of Antiparallel Vectors is Zero

Let $\mathbf u$ and $\mathbf v$ be antiparallel vectors.
Then:
:$\mathbf u \times \mathbf v = 0$
where $\times$ denotes vector cross product.

Proof:
We have {{hypothesis}} that $\mathbf u$ and $\mathbf v$ are antiparallel.
Hence we can define $\mathbf u$ and $\mathbf v$ as:
{{begin-eqn}}
{{eqn | l = \mathbf u
      | r = x \mathbf i + y \mathbf j + z \mathbf k
}}
{{eqn | l = \mathbf v
      | r = \paren {-x} \mathbf i + \paren {-y} \mathbf j + \paren {-z} \mathbf k
}}
{{end-eqn}}
where $x$, $y$ and $z$ are arbitrary real numbers.
By definition of vector cross product:
:$\mathbf u \times \mathbf v = \begin {vmatrix} \mathbf i & \mathbf j & \mathbf k \\ x & y & z \\ -x & -y & -z \end {vmatrix}$
It is seen that the $3$rd row is a multiple of the $2$nd row.
The result then follows from Determinant with Row Multiplied by Constant.
{{qed}}
Theorem: Dot Product of Antiparallel Vectors is Negative

Let $\mathbf u$ and $\mathbf v$ be non-zero antiparallel vectors.
Then:
:$\mathbf u \cdot \mathbf v < 0$
where $\cdot$ denotes dot product.

Proof:
We have {{hypothesis}} that $\mathbf u$ and $\mathbf v$ are antiparallel.
Hence we can define $\mathbf u$ and $\mathbf v$ as:
{{begin-eqn}}
{{eqn | l = \mathbf u
      | r = x \mathbf i + y \mathbf j + z \mathbf k
}}
{{eqn | l = \mathbf v
      | r = \paren {-x} \mathbf i + \paren {-y} \mathbf j + \paren {-z} \mathbf k
}}
{{end-eqn}}
where $x$, $y$ and $z$ are arbitrary real numbers such that at least one of $x$, $y$ and $z$ is not zero.
By definition of dot product:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf v
      | r = x \paren {-x} + y \paren {-y} + z \paren {-z}
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = -\paren {x^2 + y^2 + z^2}
      | c = 
}}
{{eqn | o = <
      | r = 0
      | c = as $x^2 + y^2 + z^2 > 0$
}}
{{end-eqn}}
{{qed}}