avewright/proofwiki-math huggingface dataset:
Theorem: Generalized Hilbert Sequence Space is Metric Space/Metric Space Axiom M4

Let $\alpha$ be an infinite cardinal number.
Let $I$ be an indexed set of cardinality $\alpha$.
Let $A$ be 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 $d_2: A \times A \to \R$ be the real-valued function defined as:
:$\ds \forall x = \family {x_i}, y = \family {y_i} \in A: \map {d_2} {x, y} := \paren {\sum_{i \mathop \in I} \paren {x_i- y_i}^2}^{\frac 1 2}$
Then $d_2$ satisfies {{Metric-space-axiom|4}}.

Proof:
Let $x_1, x_2 \in A : x_1 \ne x_2$.
From Lemma:
:$\exists y_1, y_2 \in \ell^2 :$
::$y_1 \ne y_2$
::$\map {d_2} {x_1, x_2} = \map {d_{\ell^2}} {y_1, y_2}$
We have:
{{begin-eqn}}
{{eqn | l = \map {d_2} {x_1, x_2}
      | r = \map {d_{\ell^2} } {y_1, y_2}
      | c = Lemma
}}
{{eqn | o = >
      | r = 0
      | c = {{Metric-space-axiom|4}} applied to $d_{\ell^2}$
}}
{{end-eqn}}
The result follows.
Theorem: Indices of Complete Bipartite Graph Commute

:$K_{m, n}$ is isomorphic to $K_{n, m}$
for all $m, n \in \N$.

Proof:
Let $K_{m, n}$ be represented by the graph $G = \struct {A \mid B, E}$, where $\card A = m$ and $\card B = n$.
Let $K_{n, m}$ be represented by the graph $G' = \struct {A' \mid B', E'}$, where $\card {A'} = n$ and $\card {B'} = m$
Let:
{{begin-eqn}}
{{eqn | l = A
      | r = \set {a_1, a_2, \ldots, a_m}
}}
{{eqn | l = B
      | r = \set {b_1, b_2, \ldots, b_n}
}}
{{eqn | l = A'
      | r = \set {a_1', a_2', \ldots, a_n'}
}}
{{eqn | l = B'
      | r = \set {b_1', b_2', \ldots, b_n'}
}}
{{end-eqn}}
First we note that:
:$\card {\set {A \mid B} } = \card {\set {A' \mid B'} }$
Let us define the isomorphism $\phi: \set {A \mid B} \to \set {A' \mid B'}$ as follows:
:$\forall v \in G: \map \phi v = \begin {cases} b_k' & : v = a_k \\ a_k' & : v = b_k \end {cases}$
It remains to be confirmed that $\phi$ is indeed an isomorphism.
Let $e = \set {u, v} \in E$.
Then:
:$\set {\map \phi u, \map \phi v} = \begin {cases} \set {b_i', a_j'} & : \set {u, v} = \set {a_i, b_j} \\ \set {a_i', b_j'} & : \set {u, v} = \set {b_i, a_j} \end {cases}$
We have that:
{{begin-eqn}}
{{eqn | q = \forall v' \in A': \exists b_i \in B
      | l = \map \phi {a_i} 
      | r = b_i
      | c = 
}}
{{eqn | q = \forall v' \in B': \exists a_j \in A
      | l = \map \phi {b_j} 
      | r = a_j
      | c = 
}}
{{end-eqn}}
demonstrating that $\phi$ is a surjection.
It follows from Cardinality of Codomain of Surjection that $\phi$ is a bijection.
Finally we note that:
:$\forall v' \in G': \map {\phi^{-1} } {v'} = \begin {cases} b_k & : v' = a_k' \\ a_k & : v' = b_k' \end {cases}$
Hence the result, by definition of isomorphism.
{{qed}}
Category:Complete Bipartite Graphs
8o8drwcmhn4zw1ogi80rjz8bot8t2xn
Theorem: Complete Bipartite Graphs which are Trees

:$K_{0, 0}$ is a tree
:$K_{1, n}$ and $K_{n, 1}$ is a tree for all $n$
and no other complete bipartite graphs are trees.

Proof:
We note from Null Graph is Complete Bipartite Graph and Null Graph is Tree that $K_{0, 0}$ is a complete bipartite graph that is also a tree.
Next we note that the order of $K_{1, n}$ is $n + 1$.
Indeed, there is $1$ vertex in $A$ and $n$ vertices in $B$, for a total of $n + 1$.
Then we note that the size of $K_{1, n}$ is $n$.
Indeed, each vertex in $B$ has exactly $1$ edge to the $1$ vertex in $A$.
By the definition of complete bipartite graph, that accounts for all edges in $G$.
From Finite Connected Simple Graph is Tree iff Size is One Less than Order it follows that $K_{1, n}$ is a tree.
Similarly:
:the order of $K_{n, 1}$ is $n + 1$
:the size of $K_{n, 1}$ is $n$
and again, $K_{n, 1}$ is a tree
Now consider the complete bipartite graph $G = \struct {A \mid B, E} = K_{0, n}$ where $n > 1$.
Let $b_1, b_2 \in B$.
As $K_{0, n}$ is bipartite, $b_1$ and $b_2$ can be adjacent to vertices in $A$ only.
But $A = \O$ and so $b_1$ and $b_2$ are isolated.
Hence $b_1$ and $b_2$ are not connected.
Hence by definition $G$ is not a connected graph
So by definition $K_{0, n}$ is not a tree.
By {{mutatis}} it follows that $K_{m, 0}$ is also not a tree for $m > 1$.
Now consider the complete bipartite graph $K_{m, n}$ where $m, n > 1$.
We recall that $K_{m, n} := G = \struct {A \mid B, E}$ such that every vertex in $A$ is adjacent to every vertex in $B$.
As $m, n > 1$ we have that:
{{begin-eqn}}
{{eqn | l = \exists a_1, a_2
      | o = \in
      | r = A
}}
{{eqn | l = \exists b_1, b_2
      | o = \in
      | r = B
}}
{{end-eqn}}
Hence we can find a cycle in $G$:
:$\tuple {a_1, b_1, a_2, b_2, a_1}$
As a tree is defined as a (connected) graph with no cycles, it follows that such a $K_{m, n}$ is not a tree.
Hence the result.
{{qed}}
Category:Complete Bipartite Graphs
Category:Tree Theory
q5nk96vdn6q4rqka33r42tp32e0at7c
Theorem: Condition for Complete Bipartite Graph to be Edgeless

:$K_{m, n}$ is edgeless {{iff}} either $m = 0$ or $n = 0$.

Proof:
Consider $K_{m, n}$ where both $m > 0$ and $n > 0$.
Then:
:$\exists u \in A, v \in V: \set {u, v} \in E$
and it follows by definition that $K_{m, n}$ is not edgeless.
Consider $K_{m, n}$ where either $m = 0$ or $n = 0$.
Hence one of the partite sets of $G$ is empty.
Hence there are no vertices for the vertices in the other partite set to be adjacent to.
So $K_{m, 0}$ and $K_{0, n}$ are edgeless.
Hence the result.
{{qed}}
Category:Complete Bipartite Graphs
Category:Edgeless Graphs
3gt3pzndxxw88kk04oxzs5k8dqeqn2a
Theorem: Complete Bipartite Graphs which are Regular

:$K_{n, n}$ is $n$-regular for all $n$
:$K_{n, 0}$ and $K_{0, n}$ are $0$-regular for all $n$
and no other complete bipartite graphs are regular.

Proof:
First consider $K_{n, 0}$ and $K_{0, n}$ for $n \in \N$.
From Condition for Complete Bipartite Graph to be Edgeless, every vertex in $K_{n, 0}$ and $K_{0, n}$ has degree $0$.
From Graph is 0-Regular iff Edgeless, $K_{n, 0}$ and $K_{0, n}$ are $0$-regular.
Now consider $K_{m, n}$ where $m, n > 0$.
By definition of complete bipartite graph:
:every vertex in $A$ is adjacent to every vertex in $B$
and so:
:every vertex in $B$ is adjacent to every vertex in $A$.
Hence:
:every vertex in $A$ has degree $m$
:every vertex in $B$ has degree $n$
So when $m, n > 0$, every vertex in $K_{m, n}$ has the same degree {{iff}} $m = n$.
Hence the result.
{{qed}}
Category:Complete Bipartite Graphs
Category:Regular Graphs
25qt25azwrb342mgrnaeogg4woif1m3
Theorem: Null Graph is Tree

The null graph $N_0$ is a tree.

Proof:
By definition, a tree is a connected graph with no cycles.
From Null Graph is Connected, $N_0$ is a connected graph.
The null graph has no edges.
Hence the null graph has no cycles vacuously.
Hence the result.
{{qed}}
Category:Null Graph
Category:Tree Theory
8jigtkxiab6o3m5vr1clnpw9vhrb49t
Theorem: Null Graph is Complete Bipartite Graph

The null graph $N_0$ is the complete bipartite graph $K_{0, 0}$.

Proof:
By definition, the complete bipartite graph $K_{0, 0}$ has no vertices.
Hence the result by definition of null graph.
{{qed}}
Category:Null Graph
Category:Complete Bipartite Graphs
f5awimvrq2u1ymz8as26brg0mpjd8ou
Theorem: Null Graph is Connected

The null graph $N_0$ is a connected graph.

Proof:
By definition, a graph $G$ is '''connected''' {{iff}} every pair of vertices in $G$ is connected.
There are no vertices in $N_0$.
Hence the result holds vacuously.
{{qed}}
Category:Null Graph
Category:Connectedness (Graph Theory)
aol2vr7k45vxn5ugdxzz4ahq5yqz681
Theorem: Complete Bipartite Graphs which are Complete Graphs

:$K_{0, 0}$ is the complete graph $K_0$
:$K_{0, 1}$ and $K_{1, 0}$ are the complete graph $K_1$
:$K_{1, 1}$ is the complete graph $K_2$
and no other complete bipartite graphs are complete.

Proof:
$K_{0, 0}$ is the null graph by Null Graph is Complete Bipartite Graph.
Then by Null Graph is Complete Graph, $K_{0, 0}$ is the complete graph $K_0$.
$K_{0, 1}$ and $K_{1, 0}$ consist of one vertex and no edges.
Then by Complete Graph of Order 1 is Edgeless, $K_{0, 1}$ and $K_{1, 0}$ are both the complete graph $K_1$.
That $K_{1, 1}$ is the complete graph $K_2$ can be determined by inspection:
:100px
{{qed|lemma}}
Suppose either $m > 1$ or $n > 1$.
Then one of the partite sets contains more than $1$ vertex.
By the nature of a bipartite graph, $2$ such vertices are not joined by an edge.
Hence by definition such a $K_{m, n}$ is not a complete graph.
{{qed}}
Category:Complete Bipartite Graphs
Category:Complete Graphs
jda6op7q6c1rstkm0rsnv072rfxl2en
Theorem: Null Graph is Complete Graph

The null graph $N_0$ is the complete graph $K_0$.

Proof:
By definition, the complete graph $K_0$ has no vertices.
Hence the result by definition of null graph.
{{qed}}
Category:Null Graph
Category:Complete Graphs
1qjrnfj3536tq3zcradqlwnzftwbjap
Theorem: Complete Bipartite Graphs which are Path Graphs

:$K_{0, 0}$ is the path graph $P_0$
:$K_{0, 1}$ and $K_{1, 0}$ are the path graph $P_1$
:$K_{1, 1}$ is the path graph $P_2$
:$K_{1, 2}$ and $K_{2, 1}$ are the path graphs $P_3$
and no other complete bipartite graphs are path graphs.

Proof:
$K_{0, 0}$, $K_{0, 1}$ and $K_{1, 0}$ have no edges.
Hence they are path graphs vacuously.
{{qed|lemma}}
That $K_{1, 1}$ is the path graph $P_2$ can be determined by inspection:
:100px
{{qed|lemma}}
Similarly, that $K_{1, 2}$ and $K_{2, 1}$ are the path graph $P_3$ can be determined by inspection:
:200px
{{qed|lemma}}
We have that Path Graph is Tree.
From Complete Bipartite Graphs which are Trees, a path graph must be of the form $K_{1, n}$ or $K_{n, 1}$ for some $n$.
But for $n \ge 3$ there exists one vertex which is of degree greater than $2$.
Hence from Degree of Vertex in Path Graph is Less than 3, $K_{1, n}$ or $K_{n, 1}$ is not a path graph for $n \ge 3$.
Hence the result.
{{qed}}
Category:Complete Bipartite Graphs
Category:Path Graphs
495ps4a0kr9wtrabebhyalp5ma7r6oh
Theorem: Complete Bipartite Graphs which are Cycle Graphs

:$K_{2, 2}$ is the cycle graph $C_4$
and no other complete bipartite graphs are cycle graphs.

Proof:
From Cycle Graph is 2-Regular, a cycle graph is $2$-regular.
From Complete Bipartite Graphs which are Regular, the only $2$-regular complete bipartite graph is $K_{2, 2}$.
Hence the result.
{{qed}}
Category:Complete Bipartite Graphs
Category:Cycle Graphs
21rembf08qx1bdc9wo92rj7333nd9hi
Theorem: Singleton Graph is Unique

The singleton graph $N_1$ is unique (up to isomorphism).

Proof:
$N_1$ can be expressed as:
:$N_1 := \struct {\set v, \O}$
where:
:$\set v$ is the set of vertices
:$\O$ is the set of edges, which is empty by definition.
Suppose there exists another singleton graph $N_1' =  \struct {\set v', \O}$.
Let $\phi: \set v \to \set {v'}$ be the mapping from $N_1$ to $N_1'$ defined as:
:$\map \phi v = v'$
From Mapping from Singleton is Injection, $\phi$ is an injection.
From Mapping to Singleton is Surjection, $\phi$ is an surjection.
Hence $\phi$ is a bijection by definition.
Finally it is noted that:
:for each edge $\set {u, v} \in \map E {N_1}$, there exists an edge $\set {\map \phi u, \map \phi v} \in \map E {N_1'}$
holds vacuously
and:
:for each edge $\set {u, v} \in \map E {N_1'}$, there exists an edge $\set {\map {\phi^{-1} } u, \map {\phi^{-1} } v} \in \map E {N_1}$
also holds vacuously.
Hence $N_1$ is isomorphic to $N_1'$ by definition.
Hence the result.
{{qed}}
Category:Singleton Graph
loy14hoy0dzsf0xy3ljr3z09i7haslg
Theorem: Singleton Graph is Edgeless

The singleton graph $N_1$ is edgeless.

Proof:
Recall the definition of $N_1$:
{{:Definition:Singleton Graph}}
As $N_1$ is simple, the only edges are between distinct vertices.
As $N_1$ has only one vertex, $N_1$ can have no edges.
{{qed}}
Theorem: Singleton Graph is Complete

The singleton graph $N_1$ is complete.

Proof:
Recall the definition of $N_1$:
{{:Definition:Singleton Graph}}
Recall the definition of complete graph:
{{:Definition:Complete Graph}}
As $N_1$ has only one vertex, this follows vacuously.
{{qed}}
Theorem: Singleton Graph is Regular

The singleton graph $N_1$ is regular of degree $0$.

Proof:
Recall the definition of $N_1$:
{{:Definition:Singleton Graph}}
Recall the definition of regular graph:
{{:Definition:Regular Graph}}
As $N_1$ has only one vertex, this follows vacuously.
{{qed}}
Category:Singleton Graph
Category:Regular Graphs
16yimaydpdlp9kinzrqoek1gwe9ud7y
Theorem: Image of Fredholm Operator of Banach Spaces is Closed

Let $\Bbb F \in \set {\R, \C}$. 
Let $\tuple {X, \norm \cdot_X}, \tuple {Y, \norm \cdot_Y}$ be Banach spaces over $\Bbb F$.
Let $T: X \to Y$ be a Fredholm operator.
Let $\Img T$ be the image of $T$ .
Then $\Img T$ is closed.

Proof:
By Kernel of Bounded Linear Transformation is Closed Linear Subspace, $\map \ker T \subseteq X$ is closed.
Thus, by Characterization of Complete Normed Quotient Vector Spaces, $X / \map \ker T$ is a Banach space.
Define the injective linear transformation $\tilde T : X / \map \ker T \to Y$ by:
:$\map {\tilde T} {\eqclass x {\map \ker T} } := \map T x$
Then $\Img {\tilde T} = \Img T$.
Replacing $T$ by $\tilde T$ if necessary, we may assume that $T$ is injective.
Since $Y / \Img T$ is finite-dimensional, it admits a finite basis:
:$\set { \eqclass {y_1} {\Img T}, \ldots, \eqclass {y_m} {\Img T}}$
Consider the direct sum:
:$X \oplus {\Bbb F^m}$
Define the surjective linear transformation $\hat T : X \oplus {\Bbb F^m} \to Y$ by:
:$\map {\hat T} {x, k_1, \ldots, k_m } := \map T x + k_1 y_1 + \cdots + k_m y_m$
Observe:
{{begin-eqn}}
{{eqn | l = \norm {\map {\hat T} {x, k_1, \ldots, k_m } }_Y
      | o = \le
      | r = \norm {\map T x}_Y + \cmod {k_1} \norm {y_1}_Y + \cdots + \cmod {k_m} \norm {y_m}_Y
}}
{{eqn | o = \le
      | r = \norm T \norm x_X + L \sqrt {\cmod {k_1}^2 + \cdots + \cmod {k_m}^2}
}}
{{end-eqn}}
where:
:$\norm T$ denotes the operator norm of $T$
:$L := \sqrt {\norm {y_1}_Y^2 + \cdots + \norm {y_m}_Y^2}$
Hence $\hat T$ is bounded.
Furthermore, $\hat T$ is injective.
Indeed, let
:$\map {\hat T} {x, k_1, \ldots, k_m } = 0$
That is:
:$k_1 y_1 + \cdots + k_m y_m = - \map T x$
Since:
:$k_1 \eqclass {y_1} {\Img T} + \cdots + k_m \eqclass {y_m} {\Img T} = 0$
we have:
:$k_1 = \cdots = k_m = 0$
Then we also have:
:$\map T x = 0$
As $T$ is injective, it follows that:
:$x = 0$
So, we have shown the injectivity of $\hat T$.
That is, $\hat T$ is a bijective bounded linear transformation.
By Banach Isomorphism Theorem, $\hat T$ is a linear isomorphism.
Now the claim follows from:
:$\Img T = \hat T \sqbrk {X \times \set { {\mathbf 0}_{\Bbb F^m} } }$
{{finish|readability}}
Category:Fredholm Operators
Category:Functional Analysis
174f7pcdlbt1kplwlwxtv0x581bjvfc
Theorem: Generalized Hilbert Sequence Space is Metric Space/Lemma 1

Let $x_1, x_2, \ldots, x_m \in A$.
Then there exists $y_1, y_2, \ldots, y_m \in \ell^2$:
:$\forall a,b \in \closedint 1 m : y_a \ne y_b \iff x_a \ne x_b$
:$\forall a,b \in \closedint 1 m : \map {d_{\ell^2} } {y_a, y_b} = \map {d_2} {x_a, x_b}$

Proof:
For each $k \in \closedint 1 m$, let:
:$\ds \sum_{i \mathop \in I} \paren{x_k}_i^2$ converge to $r_k \in \R$. 
From Characterization of Generalized Hilbert Sequence Space, there exists enumeration $J = \set{j_0, j_1, j_2, \ldots}$ of a countable set of $I$:
:$\forall k \in \closedint 1 m : \set{i \in I : \paren{x_k}_i \ne 0} \subseteq J$
:$\forall k \in \closedint 1 m : \sequence{\paren{x_k}_{j_n}} \in \ell^2$
:$\forall k \in \closedint 1 m : \ds \sum_{n \mathop = 0}^\infty \paren{x_k}_{j_n}^2 = r_k$
From P-Sequence Space with Pointwise Addition and Pointwise Scalar Multiplication on Ring of Sequences forms Vector Space:
:$\forall a, b \in \closedint 1 m : \sequence{\paren{x_a}_{j_n} - \paren{x_b}_{j_n}} \in {\ell^2}$
Let $a, b \in \closedint 1 m$
We have:
:$\forall i \in I \setminus J : \paren{x_a}_i = \paren{x_b}_i = 0$
Hence:
:$\forall i \in I \setminus J : \paren{x_a}_i - \paren{x_b}_i = 0$
It follows:
:$\set{i : \paren{x_a}_i - \paren{x_b}_i \ne 0} \subseteq J$
Since $a, b$ were arbitrary:
:$\forall a, b \in \closedint 1 m : \set{i : \paren{x_a}_i - \paren{x_b}_i \ne 0} \subseteq J$
We have:
{{begin-eqn}}
{{eqn | q = \forall a, b \in \closedint 1 m
      | l = \map {d_2} {x_a, x_b}
      | r = \sum_{i \mathop \in I} \paren{\paren{x_a}_i - \paren{x_b}_i}^2
      | c = definition of $d_2$
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren{\paren{x_a}_{j_n} - \paren{x_b}_{j_n} }^2
      | c = Characterization of Generalized Hilbert Sequence Space
}}
{{eqn | r = \map {d_{\ell^2} } {\sequence{\paren{x_a}_{j_n} }, \sequence{\paren{x_b}_{j_n} } }
      | c = {{Defof|P-Sequence Metric|Real $2$-Sequence Metric}}
}}
{{end-eqn}}
For each $k \in \closedint 1 m$, let $y_k = \sequence{\paren{x_k}_{j_n}}$.
We have:
:$\forall k \in \closedint 1 m : y_k \in \ell^2$.
:$\forall a,b \in \closedint 1 m : \map {d_{\ell^2} } {y_a, y_b} = \map {d_2} {x_a, x_b}$
It remains to show that:
:$\forall a,b \in \closedint 1 m : y_a \ne y_b \iff x_a \ne x_b$
Let $y_a \ne y_b$.
By definition of sequence:
:$\exists n \in \N : \paren{y_a}_n \ne \paren{y_b}_n$
That is:
:$\exists n \in \N : \paren{x_a}_{j_n} \ne \paren{x_b}_{j_n}$
Since $j_n \in I$, then:
:$\exists i \in I : \paren{x_a}_i \ne \paren{x_b}_i$
By definition of indexed family:
:$x_a \ne x_b$
Let $x_a \ne x_b$.
By definition of indexed family:
:$\exists i \in I : \paren{x_a}_i \ne \paren{x_b}_i$
Hence:
:either $\paren{x_a}_i \ne 0$ or $\paren{x_b}_i \ne 0$.
In either case:
:$i \in \set{j_0, j_1, j_2, \ldots }$
Hence for some $n \in \N$:
:$\paren{x_a}_{j_n} \ne \paren{x_b}_{j_n}$
That is:
:$\paren{y_a}_n \ne \paren{y_b}_n$
By definition of sequence:
:$y_a \ne y_b$
The result follows.
{{qed}}
Category:Generalized Hilbert Sequence Space is Metric Space
9anjicc5wnonnnrl7kbrlcc4gf4yfnz
Theorem: Acceleration of Point in Straight Line

Let $\mathbf a$ be the acceleration of a particle $P$ in space.
Let $P$ be moving along a straight line $\LL$ whose positive direction has been established.
Then the motion of $P$ can be defined by:
:$\mathbf a = \dfrac {\d^2 s} {\d t^2} \mathbf i$
where $\mathbf i$ denotes the unit vector in the positive direction of $\LL$.

Proof:
We have {{hypothesis}} that $P$ moves along a straight line $\LL$.
Then the rate of change of displacement perpendicular to $\LL$ is zero.
Let the $\LL$ be embedded in a Cartesian space $\CC$.
From the components of acceleration vector, we have:
:$\mathbf a = \dfrac {\d \mathbf v} {\d t} = \dfrac {\d^2 \mathbf r} {\d t^2}$
where:
:$\mathbf v$ is the velocity of $P$ at time $t$
:$\mathbf r$ is the displacement of $P$ at time $t$ expressed as a position vector from a given origin.
Thus:
:$\mathbf a = \dfrac {\d^2 x} {\d t^2} \mathbf i + \dfrac {\d^2 x} {\d t^2} \mathbf j + \dfrac {\d^2 x} {\d t^2} \mathbf k$
where:
:$\mathbf r = x \mathbf i + y \mathbf j + z \mathbf k$
Let us define $\CC$ such that $\LL$ is parallel to the $x$-axis of $\CC$.
Then we have:
{{begin-eqn}}
{{eqn | l = \mathbf v
      | r = \dfrac {\d x} {\d t} \mathbf i + \dfrac {\d y} {\d t} \mathbf j + \dfrac {\d z} {\d t} \mathbf k 
      | c = {{Defof|Velocity}}
}}
{{eqn | r = \dfrac {\d x} {\d t} \mathbf i + 0 \mathbf j + 0 \mathbf k
      | c = as the $y$-axis and $z$-axis are perpendicular to $\LL$
}}
{{eqn | ll= \leadsto
      | l = \mathbf a
      | r = \dfrac {\d^2 x} {\d t} \mathbf i
      | c = {{Defof|Acceleration}}
}}
{{end-eqn}}
{{qed}}
Theorem: Acceleration of Point in Plane in Intrinsic Coordinates

Let $\mathbf a$ be the acceleration of a particle $P$ in space.
Let $P$ be moving in a plane $\PP$.
Then the motion of $P$ can be expressed in intrinsic coordinates as:
:$\mathbf a = \dfrac {\d \map v t} {\d t} \mathbf s + \dfrac {\paren {\map v t}^2} \rho \bspsi$
where:
:$\mathbf s$ denotes the unit vector along the tangential direction of $P$
:$\bspsi$ denotes the unit vector toward the center of curvature of the motion of $P$
:$\map v t$ is the speed of $P$ at the time $t$
:$\rho$ is the radius of curvature of the motion of $P$ at time $t$.

Proof:
{{ProofWanted|Needs some more background work on intrinsic coordinates for this to make sense<br/> See https://dspace.mit.edu/bitstream/handle/1721.1/60691/16-07-fall-2004/contents/lecture-notes/d4.pdf}}
Theorem: Tangential Component of Acceleration of Uniform Circular Motion is Zero

Let $P$ be a particle moving in space in uniform circular motion.
Let $\mathbf a$ denote the acceleration of $P$.
Then the tangential component of $\mathbf a$ is zero.

Proof:
From Acceleration of Point in Plane in Intrinsic Coordinates, the motion of $P$ can be expressed in intrinsic coordinates as:
:$\mathbf a = \dfrac {\d \map v t} {\d t} \mathbf s + \dfrac {\paren {\map v t}^2} \rho \bspsi$
where:
:$\mathbf s$ denotes the unit vector along the tangential direction of $P$
:$\bspsi$ denotes the unit vector toward the center of curvature of the motion of $P$
:$\map v t$ is the speed of $P$ at the time $t$
:$\rho$ is the radius of curvature of the motion of $P$ at time $t$.
By definition, the tangential component of $\mathbf a$ is defined as $\dfrac {\d v} {\d t}$.
Let $\map v t$ denote the speed of $P$ at time $t$.
By definition of uniform circular motion, $\map v t$ is constant.
Hence by Derivative of Constant it follows that:
:$\dfrac {\d \map v t} {\d t} = 0$
Hence the result.
{{qed}}
Theorem: Countably Infinite Set has Enumeration

Let $S$ be a countably inifnite set.
Then there exists a countably infinite enumeration $\set{s_1, s_2, s_3, \ldots}$ of $S$.

Proof:
By definition of countably inifnite set:
:there exists a bijection $f:S \to \N$
From Inverse of Bijection is Bijection:
:$f^{-1} : \N \to S$ is a bijection
Let $s = f^{-1}$.
It follows that $s : \N \to S$ is a countably infinite enumeration $\set{s_1, s_2, s_3, \ldots}$ by definition.
{{qed}}
s8g9y1tnv04add54jfjs9o548er7xyu
Theorem: Generalized Sum of Constant Zero Converges to Zero

Let $G$ be a commutative topological semigroup with identity $0_G$.
Let $\family{g_i}_{i \in I}$ be the indexed family of $G$ defined by:
:$\forall i \in I : g_i = 0_G$
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converges to $0_G$

Proof:
Let $\FF$ denote the set of finite subsets of $I$.
From Power of Identity is Identity:
:$\forall F \in \FF : \ds \map \phi F = \sum_{i \mathop \in F} g_i = 0_G$
Hence the net $\ds \sum \set {g_i: i \in I}$ is a  constant mapping.
From Constant Net is Convergent:
:the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converges to $0_G$
{{qed}}
Category:Generalized Sums
auz2gbdimi6zmnhp6gd97rcy9086cwn
Theorem: Generalized Sum Restricted to Non-zero Summands/Corollary

Let $K \subseteq I : \set{i \in I : g_i \ne 0_G} \subseteq K$
Let $h \in G$.
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converges to $h$
{{iff}}:
:the generalized sum $\ds \sum_{k \mathop \in K} g_k$ converges to $h$

Proof:
Let $J = \set{i \in I : g_i \ne 0_G}$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop \in I} g_i
      | o = \to
      | r = h
}}
{{eqn | ll = \leadstoandfrom
      | l = \sum_{j \mathop \in J} g_j
      | o = \to
      | r = h
      | c = Generalized Sum Restricted to Non-zero Summands
}}
{{eqn | ll = \leadstoandfrom
      | l = \sum_{k \mathop \in K} g_k
      | o = \to
      | r = h
      | c = Generalized Sum Restricted to Non-zero Summands
}}
{{end-eqn}}
{{qed}}
Category:Generalized Sum Restricted to Non-zero Summands
8a2e86ip655cekwchk5shr3s7cttixm