avewright/proofwiki-math huggingface dataset:
Theorem: Real Multiplication is Sequentially Computable

Let $f : \R^2 \to \R$ be defined as:
:$\map f {x, y} = x y$
Then $f$ is sequentially computable.

Proof:
Follows immediately from Product of Computable Real Sequences is Computable.
{{qed}}
Category:Computability Theory
buyid8unyfwvt87jsb37szhzr7ondsm
Theorem: Reciprocal of Computable Rational Sequence is Computable

Let $\sequence {x_n}$ be a computable rational sequence.
Suppose that, for all $n \in \N$:
:$x_n \ne 0$
Then:
:$\sequence {\dfrac 1 {x_n}}$ is a computable rational sequence.

Proof:
By definition of computable rational sequence, there exist total recursive $f, g : \N \to \N$ such that:
:$x_n = \dfrac {k_n} {\map g n + 1}$
where $\map f n$ codes the integer $k_n$.
We will define $f', g' : \N \to \N$ as:
:$\map {f'} n = \map {\sgn_\Z} {k_n} \times_\Z \paren {\map g n + 1}_\Z$
:$\map {g'} n = \map {\operatorname{pred}} {\size {k_n}}$
We have that both $f'$ and $g'$ are total recursive by:
* Signum Function on Integers is Primitive Recursive
* Multiplication of Integers is Primitive Recursive
* Code Number for Non-Negative Integer is Primitive Recursive
* Absolute Value of Integer is Primitive Recursive
* Predecessor Function is Primitive Recursive
We now need to show that, for all $n \in \N$:
:$\dfrac 1 {x_n} = \dfrac {k'_n} {\map {g'} n + 1}$
where $\map {f'} n$ codes the integer $k'_n$.
Since $x_n \ne 0$ by assumption, we have:
:$k_n \ne 0$
for all $n \in \N$.
We will now examine the cases of:
:$k_n > 0$
:$k_n < 0$
Suppose $k_n > 0$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {x_n}
      | r = \dfrac {\map g n + 1} {k_n}
}}
{{eqn | r = \dfrac {\map \sgn {k_n} \paren {\map g n + 1} } {\size {k_n} }
      | c = $\map \sgn {k_n} = 1$ and $k_n = \size {k_n}$
}}
{{eqn | r = \dfrac {\map \sgn {k_n} \paren {\map g n + 1} } {\map {\operatorname{pred} } {\size {k_n} } + 1}
      | c = $\size {k_n} \ge 1$
}}
{{eqn | r = \dfrac {k'_n} {\map {g'} n + 1}
}}
{{end-eqn}}
Suppose $k_n < 0$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {x_n}
      | r = \dfrac {\map g n + 1} {k_n}
}}
{{eqn | r = \dfrac {- \map \sgn {k_n} \paren {\map g n + 1} } {- \size {k_n} }
      | c = $\map \sgn {k_n} = -1$ and $k_n = - \size {k_n}$
}}
{{eqn | r = \dfrac {\map \sgn {k_n} \paren {\map g n + 1} } {\size {k_n} }
}}
{{eqn | r = \dfrac {\map \sgn {k_n} \paren {\map g n + 1} } {\map {\operatorname{pred} } {\size {k_n} } + 1}
      | c = $\size {k_n} \ge 1$
}}
{{eqn | r = \dfrac {k'_n} {\map {g'} n + 1}
}}
{{end-eqn}}
Thus, by Proof by Cases, the result holds.
{{qed}}
Category:Computability Theory
1c12pdoaxec84lawbvp3tnln3m3c6t9
Theorem: Seminorm on Vector Space induces Norm on Quotient

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $p$ be a seminorm on $X$.
Let:
:$N = \set {x \in X : \map p x = 0}$
From Set of Points for which Seminorm is Zero is Vector Subspace, $N$ is a vector subspace.
Let $X/N$ be the quotient vector space of $X$ modulo $N$.
Let $\pi : X \to X/N$ be the quotient mapping.
Then the mapping $\norm {\, \cdot \,} : X/N \to \hointr 0 \infty$ defined by:
:$\norm {\map \pi x} = \map p x$
is well-defined and a norm on $X/N$.

Proof:
We first want to show that if $\map \pi x = \map \pi y$ for $x, y \in X$, then $\map p x = \map p y$. 
From Quotient Mapping is Linear Transformation and Kernel of Quotient Mapping, it is enough to show that:
:if $y - x \in N$ then $\map p x = \map p y$.
It is therefore enough to show that if $x \in X$ and $z \in N$, then:
:$\map p {x + z} = \map p x$
Let $x \in X$ and $z \in N$. 
Then $\map p z = 0$. 
From Reverse Triangle Inequality: Seminormed Vector Space, we have:
:$\map p x = \size {\map p x - \map p z} \le \map p {x + z}$
From {{NormAxiomVector|3}}, we also have:
:$\map p {x + z} \le \map p x + \map p z = \map p x$ 
Hence we have $\map p {x + z} = \map p x$. 
Hence $\norm {\, \cdot \,}$ is well-defined.
We now prove the norm axioms.
Theorem: Completion Theorem (Normed Vector Space)

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Then there exists a Banach space $\struct {\widetilde X, \widetilde {\norm {\, \cdot \,} } }$ and a linear isometry $\phi : X \to \widetilde X$ such that $\phi \sqbrk X$ is dense in $\widetilde X$.
Further, the Banach space $\struct {\widetilde X, \widetilde {\norm {\, \cdot \,} } }$ is unique up to isometric isomorphism.

Proof:
=== Proof of Existence ===
Let $\struct {X^{\ast \ast}, \norm {\, \cdot \,}_{X^{\ast \ast} } }$ be the second normed dual of $\struct {X, \norm {\, \cdot \,} }$.
From Normed Dual Space is Banach Space, $\struct {X^{\ast \ast}, \norm {\, \cdot \,}_{X^{\ast \ast} } }$ is a Banach space. 
Let $\phi : X \to X^{\ast \ast}$ be the evaluation transformation.
From Evaluation Linear Transformation on Normed Vector Space is Linear Isometry, $\phi$ is a linear isometry. 
Let $\widetilde X = \map \cl {\phi \sqbrk X}$ where $\cl$ denotes the closure in $\struct {X^{\ast \ast}, \norm {\, \cdot \,}_{X^{\ast \ast} } }$.
Let $\widetilde {\norm {\, \cdot \,} }$ be the restriction of $\norm {\, \cdot \,}_{X^{\ast \ast} }$ to $\map \cl {\phi \sqbrk X}$.
From Subspace of Complete Metric Space is Closed iff Complete, $\struct {\widetilde X, \widetilde {\norm {\, \cdot \,} } }$ is a Banach space.
Further, $\phi \sqbrk X$ is dense in $\map \cl {\phi \sqbrk X}$.
So $\struct {\widetilde X, \widetilde {\norm {\, \cdot \,} } }$ satisfies the conditions of the theorem.
{{qed|lemma}}
Theorem: Composition of Linear Isometries is Linear Isometry

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm \cdot_X}$, $\struct {Y, \norm \cdot_Y}$ and $\struct {Z, \norm \cdot_Z}$ be normed vector spaces over $\GF$.
Let $T : X \to Y$ and $S : Y \to Z$ be linear isometries.
Then $S T$ is a linear isometry.

Proof:
From Composition of Linear Transformations is Linear Transformation, $S T$ is a linear transformation. 
For $x \in X$, we have:
{{begin-eqn}}
{{eqn	| l = \norm {S T x}_Z
		| r = \norm {T x}_Y
		| c = $S$ is a linear isometry
}}
{{eqn	| r = \norm x_X
		| c = $T$ is a linear isometry
}}
{{end-eqn}}
So $S T$ is a linear isometry.
{{qed}}
Category:Linear Isometries
t1kfbsw92etaabuw93wgd6258et54zv
Theorem: Reciprocal of Computable Real Sequence is Computable

Let $\sequence {x_m}$ be a computable real sequence.
Suppose that, for all $m \in \N$:
:$x_m \ne 0$
Then:
:$\sequence {\dfrac 1 {x_m}}$
is a computable real sequence.

Proof:
=== Lemma ===
{{:Reciprocal of Computable Real Sequence is Computable/Lemma}}{{qed|lemma}}
{{WIP}}
q5p794tqe40tdq8trij5g61hmx3n9ql
Theorem: Center of Mass in Barycentric Coordinates

Let $p_0, p_1, p_2, p_3$ be fixed non-coplanar points, such that $p_i = \tuple {x_i, y_1, z_i}$.
Let $p$ be a point in ordinary space expressed in barycentric coordinates {{WRT}} $\set {p_0, p_1, p_2, p_3}$:
:$p = \lambda_0 p_0 + \lambda_1 p_1 + \lambda_2 p_2 + \lambda_3 p_3$
such that:
:$\lambda_0 + \lambda_1 + \lambda_2 + \lambda_3 = 1$
Let point masses of mass $\lambda_0, \lambda_1, \lambda_2, \lambda_3$ be placed at $p_0, p_1, p_2, p_3$ respectively.
Then $p$ is the center of mass of $\set {p_0, p_1, p_2, p_3}$.

Proof:
From the definition of center of mass with discrete masses:
:$\ds Mp = \sum_{i \mathop = 0}^3 \lambda_i p_i$
From the restriction on barycentric coordinates:
:$\ds M = \sum_{i \mathop = 0}^3 \lambda_i = 1$
Thus:
:$\ds p = \sum_{i \mathop = 0}^3 \lambda_i p_i = \lambda_0 p_0 + \lambda_1 p_1 + \lambda_2 p_2 + \lambda_3 p_3$
{{qed}}
Theorem: Representation of Number Base in that Base

Let $b \in \Z$ be an integer such that $b > 1$.
Then $b$ is expressed in base $b$ as $10$.

Proof:
By the Basis Representation Theorem, $b$ can be expressed uniquely in the form:
:$\ds b = \sum_{j \mathop = 0}^m r_j b^j$
where:
:$m$ is such that $b^m \le n < b^{m + 1}$
:all the $r_j$ are such that $0 \le r_j < b$.
As $b = b^1$, we have that:
:$b = 1 \times b^1 + 0 \times b^0$
That is, by definition of base $b$:
:$b = \sqbrk {1 0}_b$
Hence the result.
{{qed}}
Theorem: Frequency of Beats

Let $W_1$ and $W_2$ be harmonic waves whose frequencies are $f_1$ and $f_2$.
Let the superpositon of $W_1$ onto $W_2$ exhibit the phenomenon of beats.
The frequency $f_b$ of those beats is:
:$f_b = \size {f_2 - f_1}$

Proof:
Let $\omega_1$ and $\omega_2$ denote the angular frequency of $W_1$ and $W_2$ respectively.
Let us consider the harmonic waves that are $W_1$ and $W_2$ as they disturb the medium at $x = 0$.
{{WLOG}}, therefore, let $W_1$ and $W_2$ be be expressed as:
{{begin-eqn}}
{{eqn | l = \map {\phi_1} t
      | r = \sin \omega_1 t
      | c = 
}}
{{eqn | l = \map {\phi_2} t
      | r = \sin \omega_2 t
      | c = 
}}
{{end-eqn}}
where:
{{begin-eqn}}
{{eqn | l = \omega_1
      | r = 2 \pi f_1
      | c = {{Defof|Angular Frequency}}
}}
{{eqn | l = \omega_2
      | r = 2 \pi f_2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map {\phi_1} t + \map {\phi_2} t
      | r = \sin \omega_1 t + \sin \omega_2 t
      | c = superimposing the two waves
}}
{{eqn | r = 2 \map \sin {\dfrac {\omega_1 t + \omega_2 t} 2} \map \cos {\dfrac {\omega_1 t - \omega_2 t} 2}
      | c = Sine plus Sine
}}
{{eqn | r = 2 \map \sin {\dfrac {\paren {\omega_1 + \omega_2} t} 2} \map \cos {\dfrac {\paren {\omega_1 - \omega_2} t} 2}
      | c = simplifying
}}
{{eqn | r = 2 \map \sin {\dfrac {\paren {\omega_1 + \omega_2} t} 2} \map \cos {\dfrac {\size {\omega_1 - \omega_2} t} 2}
      | c = Cosine Function is Even
}}
{{end-eqn}}
Hence the superimposition of the two waves is equivalent to forming the product of the waves of frequency $\dfrac {\omega_1 + \omega_2} 2$ and $\dfrac {\size {\omega_1 - \omega_2} } 2$.
:620px
In the above diagram, there are $3$ waves superimposed:
:$(1) \quad \pm 2 \map \cos {\dfrac {\size {\omega_1 - \omega_2} t} 2}$ in red
:$(2) \quad 2 \map \sin {\dfrac {\paren {\omega_1 + \omega_2} t} 2}$ in green
:$(3) \quad 2 \map \sin {\dfrac {\paren {\omega_1 + \omega_2} t} 2} \map \cos {\dfrac {\size {\omega_1 - \omega_2} t} 2}$ in blue
Hence we see:
{{begin-eqn}}
{{eqn | l = \size {\map {\phi_1} t + \map {\phi_2} t}
      | o = \le
      | r = \size {2 \map \cos {\dfrac {\size {\omega_1 - \omega_2} t} 2} }
      | c = as $\map \sin {\dfrac {\paren {\omega_1 + \omega_2} t} 2} \le 1$ throughout
}}
{{end-eqn}}
Hence the angular frequency $\omega_b$ of the slower component is seen to be:
:$\omega_b = \dfrac {\size {\omega_1 - \omega_2} } 2$
By definition of angular frequency:
{{begin-eqn}}
{{eqn | l = f_b
      | r = \dfrac {\omega_b} {2 \pi}
      | c = {{Defof|Angular Frequency}}
}}
{{eqn | r = \dfrac 1 {2 \pi} \dfrac {\size {\omega_1 - \omega_2} } 2
      | c = 
}}
{{eqn | r = \dfrac {\size {\frac {\omega_1} {2 \pi} - \frac {\omega_2} {2 \pi} } } 2
      | c = 
}}
{{eqn | r = \dfrac {\size {f_1 - f_2} } 2
      | c = 
}}
{{end-eqn}}
Hence the frequency of the slower component is seen to be:
:$\dfrac {\size {f_1 - f_2} } 2$
Finally we note that the beats themselves occur at the peaks and troughs of the slower component.
That is, the frequency $f_b$ of those beats is twice $\dfrac {\size {f_1 - f_2} } 2$.
The result is apparent.
{{qed}}
Theorem: Amplitude of Beats

Let $W_1$ and $W_2$ be harmonic waves whose frequencies are $f_1$ and $f_2$.
Let the amplitude of $W_1$ and $W_2$ both be $a$.
Let the superpositon of $W_1$ onto $W_2$ exhibit the phenomenon of beats.
The amplitude $A_b$ of those beats at time $t$ is:
:$A_b = 2 a \map \cos {\pi \size {f_1 - f_2} t - \dfrac \epsilon 2}$

Proof:
Let $\omega_1$ and $\omega_2$ denote the angular frequency of $W_1$ and $W_2$ respectively.
Let us consider the harmonic waves that are $W_1$ and $W_2$ as they disturb the medium at $x = 0$.
{{WLOG}}, therefore, let $W_1$ and $W_2$ be be expressed as:
{{begin-eqn}}
{{eqn | l = \map {\phi_1} t
      | r = a \sin \omega_1 t 
      | c = 
}}
{{eqn | l = \map {\phi_2} t
      | r = a \map \sin {\omega_2 t + \epsilon}
      | c = 
}}
{{end-eqn}}
where:
{{begin-eqn}}
{{eqn | l = \omega_1
      | r = 2 \pi f_1
      | c = {{Defof|Angular Frequency}}
}}
{{eqn | l = \omega_2
      | r = 2 \pi f_2
      | c = 
}}
{{end-eqn}}
and $\epsilon$ is the phase of $\phi_1$ {{WRT}} $\phi_2$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\phi_1} t + \map {\phi_2} t
      | r = a \sin \omega_1 t + a \map \sin {\omega_2 t + \epsilon}
      | c = superimposing the two waves
}}
{{eqn | r = 2 a \map \sin {\dfrac {\omega_1 t + \omega_2 t + \epsilon} 2} \map \cos {\dfrac {\omega_1 t - \paren {\omega_2 t + \epsilon} } 2}
      | c = Sine plus Sine
}}
{{eqn | r = 2 a \map \sin {\dfrac {\paren {\omega_1 + \omega_2} t + \epsilon} 2} \map \cos {\dfrac {\paren {\omega_1 - \omega_2} t - \epsilon} 2}
      | c = simplifying
}}
{{eqn | r = 2 a \map \sin {\dfrac {\paren {\omega_1 + \omega_2} t + \epsilon} 2} \map \cos {\dfrac {\size {\omega_1 - \omega_2} t - \epsilon} 2}
      | c = Cosine Function is Even
}}
{{eqn | ll= \leadsto
      | l = \size {\map {\phi_1} t + \map {\phi_2} t}
      | o = \le
      | r = \size {2 a \map \cos {\dfrac {\size {\omega_1 - \omega_2} t - \epsilon} 2} }
      | c = as $\map \sin {\dfrac {\paren {\omega_1 + \omega_2} t} 2} \le 1$ throughout
}}
{{end-eqn}}
Hence the amplitude $a$ of the slower component is seen to be:
:$A_b = \dfrac {\size {\omega_1 - \omega_2} } 2$
By definition of angular frequency:
{{begin-eqn}}
{{eqn | l = A_b
      | r = 2 a \map \cos {\dfrac {\size {\omega_1 - \omega_2} t - \epsilon} 2}
      | c = 
}}
{{eqn | r = 2 a \map \cos {\dfrac {\size {2 \pi f_1 - 2 \pi f_2} t - \epsilon} 2}
      | c = {{Defof|Angular Frequency}}
}}
{{eqn | r = 2 a \map \cos {\pi \size {f_1 - f_2} t - \dfrac \epsilon 2}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Bounded Summation of Integers is Primitive Recursive

Let the function $f : \N^{k + 1} \to \N$ be primitive recursive.
Let the function $g : \N^{k + 1} \to \N$ be defined as:
:$\ds \map g {n_1, \dotsc, n_k, z} = \paren {\sum_{y = 0}^{z - 1} \ell_y}_\Z$
where $\map f {n_1, \dotsc, n_k, y}$ codes the integer $\ell_y$.
Then, $g$ is primitive recursive.

Proof:
We can equivalently write $g$ as:
:$\map g {n_1, \dotsc, n_k, z} = \begin{cases} 0 & : z = 0 \\ \map g {n_1, \dotsc, n_k, z - 1} +_\Z \map f {n_1, \dotsc, n_k, z - 1} & : z > 0 \end{cases}$
which is clearly obtained by primitive recursion from:
* Addition of Integers is Primitive Recursive
{{qed}}
Category:Primitive Recursive Functions
o6ths46j2qt84x6qz2burn6a7jxbeoq
Theorem: Generalized Sum over Union of Disjoint Index Sets

Let $\struct {G, +}$ be a commutative topological semigroup.
Let $I$ and $J$ be disjoint indexing sets.
Let $K = I \cup J$.
Let $\family{g_k}_{k \mathop \in K}$ be an indexed family of elements of $G$.
Let the generalized sums $\ds \paren{\sum_{i \mathop \in I} g_i}$ and $\ds \paren{\sum_{j \mathop \in J} g_j}$ converge.
Then:
:the generalized sum $\ds \sum_{k \mathop \in K} g_k$ converges
and:
:$\ds \sum_{k \mathop \in K} g_k = \paren{\sum_{i \mathop \in I} g_i} + \paren{\sum_{j \mathop \in J} g_j}$

Proof:
Let $0_G$ be the identity of the semigroup $\struct {G, +}$.
Let $\family{f_k}_{k \mathop \in K}$ be an indexed family of elements of $G$ defined by:
:$\forall k \in K : f_k = \begin{cases}
g_k & : k \in I \\
0_G & : k \in J 
\end{cases}$
Let $\family{h_k}_{k \mathop \in K}$ be an indexed family of elements of $G$ defined by:
:$\forall k \in K : h_k = \begin{cases}
0_G & : k \in I \\
g_k & : k \in J 
\end{cases}$
From Generalized Sum Restricted to Non-zero Summands:
:$\ds \sum_{k \mathop \in K} f_k = \sum_{i \mathop \in I} g_i$
and:
:$\ds \sum_{k \mathop \in K} h_k = \sum_{j \mathop \in J} g_j$
From Sum Rule for Convergent Generalized Sums:
:$\ds \sum_{k \mathop \in K} \paren{f_k + h_k} = \sum_{k \mathop \in K} f_k + \sum_{k \mathop \in K} h_k = \sum_{i \mathop \in I} g_i + \sum_{j \mathop \in J} g_j$
We have:
{{begin-eqn}}
{{eqn | q = \forall k \in K 
      | l = f_k + h_k
      | r = \begin{cases}
g_k + 0_G & : k \in I \\
0_G + g_k & : k \in J 
\end{cases}
      | c = definition of $f$ and $h$
}}
{{eqn | r = \begin{cases}
g_k & : k \in I \\
g_k & : k \in J 
\end{cases}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = g_k
}}
{{end-eqn}}
Hence:
:$\ds \sum_{k \mathop \in K} g_k = \paren{\sum_{i \mathop \in I} g_i} + \paren{\sum_{j \mathop \in J} g_j}$
{{qed}}
Category:Generalized Sums
hwk0oovcj50scidr2pu9uko88thklnz
Theorem: Sum Rule for Convergent Nets

Let $\struct {G, +}$ be a commutative topological semigroup.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {g_\lambda}_{\lambda \mathop \in \Lambda}$ and $\family {h_\lambda}_{\lambda \mathop \in \Lambda}$ be an indexed family of elements in $G$.
Let $\family {g_\lambda}_{\lambda \mathop \in \Lambda}$ and $\family {h_\lambda}_{\lambda \mathop \in \Lambda}$ be convergent to the following limits:
:$\ds \lim_{\lambda \mathop \in \Lambda} g_\lambda = a$
:$\ds \lim_{\lambda \mathop \in \Lambda} h_\lambda = b$
Then:
:the indexed family $\family {g_\lambda + h_\lambda}_{\lambda \mathop \in \Lambda}$ converges to the limit:
::$\ds \lim_{\lambda \mathop \in \Lambda} g_\lambda + h_\lambda = a + b$

Proof:
Let $U$ be an open neighborhood of $a + b$.
By definition of topological semigroup:
:the binary operation $+ : G \times G \to G$ is continuous.
By definition of continuous mapping:
:$\exists W, V$ open neighborhoods of $a$ and $b$ respectively:
::$+ \sqbrk {W \times V} \subseteq U$
By definition of convergence:
:$\exists \lambda_1 \in \Lambda : \forall \mu \in \Lambda : \lambda_1 \preceq \mu \implies g_\mu \in W$
and:
:$\exists \lambda_2 \in \Lambda : \forall \mu \in \Lambda : \lambda_2 \preceq \mu \implies h_\mu \in V$
By definition of directed set:
:$\exists \lambda \in \Lambda : \lambda_1, \lambda_2 \preceq \lambda$
By definition of directed set:
:$\forall \mu \in \Lambda : \lambda \preceq \mu \implies \lambda_1, \lambda_2 \preceq \mu$
Hence $\forall \mu \in \Lambda$ such that $\lambda \preceq \mu$:
:$g_\mu + h_\mu \in U$
Since $U$ was arbitrary, for all open neighborhoods $U$ of $a + b$:
:$\exists \lambda \in \Lambda : \forall \mu \in \Lambda : \lambda \preceq \mu \leadsto g_\mu + h_\mu \in U$
By definition of limit of net:
:$\ds \lim_{\lambda \in \Lambda} g_\lambda + h_\lambda = a + b$
{{qed}}
Category:Nets (Set Theory)
iu2zumnjqb6zii0doi3odiegdx3mfqi
Theorem: Sum Rule for Convergent Generalized Sums

Let $\struct {G, +}$ be a commutative topological semigroup.
Let $\family {g_i}_{i \mathop \in I}$ and $\family {h_i}_{i \mathop \in I}$ be an indexed family of elements in $G$.
Let the generalized sums $\ds \sum_{i \mathop \in I} g_i$ and $\ds \sum_{i \mathop \in I} h_i$ be convergent to the following limits:
:$\ds \sum_{i \mathop \in I} g_i = a$
:$\ds \sum_{i \mathop \in I} h_i = b$
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} \paren{g_i + h_i}$ converges to the limit:
::$\ds \sum_{i \mathop \in I} \paren{g_i + h_i} = a + b$

Proof:
Consider the set $\FF$ of finite subsets of $I$.
By definition of Definition:Generalized Sum:
:$\ds \sum_{i \mathop \in I} g_i$ is the net $\ds \family{\sum_{i \mathop \in F} g_i}_{F \mathop \in \FF}$
and
:$\ds \sum_{i \mathop \in I} h_i$ is the net $\ds \family{\sum_{i \mathop \in F} h_i}_{F \mathop \in \FF}$
By definition of convergence:
:$\ds \lim_{F \mathop \in \FF} \paren{\sum_{i \mathop \in F} g_i} = a$
and:
:$\ds \lim_{F \mathop \in \FF} \paren{\sum_{i \mathop \in F} h_i} = b$
From Sum Rule for Convergent Nets:
:$\ds \lim_{F \mathop \in \FF} \paren{\sum_{i \mathop \in F} g_i + \sum_{i \mathop \in F} h_i} = a + b$
We have:
:$\forall F \in \FF : \ds \paren{\sum_{i \mathop \in F} g_i} + \paren{\sum_{i \mathop \in F} h_i} = \sum_{i \mathop \in F} \paren{g_i + h_i}$
Hence:
:$\ds \lim_{F \mathop \in \FF} \sum_{i \mathop \in F} \paren{g_i + h_i} = a + b$
By definition of generalized sum, $\ds \sum_{i \mathop \in I} \paren{g_i + h_i}$ converges to the limit:
:$\ds \sum_{i \mathop \in I} \paren{g_i + h_i} = a + b$ 
{{qed}}
Category:Generalized Sums
6tfrhmb33exrkudzq5bzq6b25r6qj7i
Theorem: Inequality Rule for Real Convergent Nets

Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ and $\family {y_\lambda}_{\lambda \mathop \in \Lambda}$ be indexed families of elements in $\R$.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ and $\family {y_\lambda}_{\lambda \mathop \in \Lambda}$ be convergent to the following limits:
:$\ds \lim_{\lambda \mathop \in \Lambda} x_\lambda = l$
:$\ds \lim_{\lambda \mathop \in \Lambda} y_\lambda = m$
Let there exist $\lambda \in \Lambda$ such that:
:$\forall \mu \in \Lambda : \lambda \preceq \mu: x_\mu \le y_\mu$
Then:
:$l \le m$

Proof:
{{AimForCont}}
:$l > m$
Let $\epsilon = \dfrac {\paren{l - m}} 2$.
Hence:
:$\epsilon > 0$
and:
:$(1) \quad l - \epsilon = m + \epsilon$ 
By definition of convergence:
:$\exists \lambda_1 \in \Lambda : \forall \mu \in \Lambda : \lambda_1 \preceq \mu \implies \size{l - x_\mu} < \epsilon$
and:
:$\exists \lambda_2 \in \Lambda : \forall \mu \in \Lambda : \lambda_2 \preceq \mu \implies \size{m - y_\mu} < \epsilon$
From Closed Interval Defined by Absolute Value:
:$(2) \quad \forall \mu \in \Lambda : \lambda_1 \preceq \mu \implies l - \epsilon < x_\mu$
and:
:$(3) \quad \forall \mu \in \Lambda : \lambda_2 \preceq \mu \implies m + \epsilon > y_\mu$
By definition of directed set:
:$\exists \mu \in \Lambda : \lambda, \lambda_1, \lambda_2 \preceq \mu$
We have:
{{begin-eqn}}
{{eqn | l = x_\mu
      | o = >
      | r = l - \epsilon
      | c = from $(2)$
}}
{{eqn | r = m + \epsilon
      | c = from $(1)$
}}
{{eqn | o = >
      | r = y_\mu
      | c = from $(3)$
}}
{{end-eqn}}
This contradicts the hypothesis:
:$\forall \mu \in \Lambda : \lambda \preceq \mu: x_\mu \le y_\mu$
Hence:
:$l \le m$
{{qed}}
Category:Nets (Set Theory)
a09r35tb0swe27wgbcxq5ysb6dq85qf
Theorem: Generalized Sum over Subset of Absolutely Convergent 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 the generalized sum $\ds \sum_{i \mathop \in I} v_i$ be absolutely net convergent.
Let $J \subseteq I$.
Then:
:the generalized sum $\ds \sum_{j \mathop \in J} v_j$ is absolutely net convergent.

Proof:
By definition  of absolute net convergence, let:
:$\ds \sum_{i \mathop \in I} \norm{v_i} = M$
Let $F \subseteq J$ be finite.
From Subset Relation is Transitive:
:$F \subseteq I$
From Absolutely Convergent Generalized Sum Converges to Supremum:
:$\ds \sum_{j \mathop \in F} \norm{v_j} \le M$
Since $F \subseteq J$ was arbitrary, it follows that:
:$\forall F \subseteq J : F$ is finite $: \ds \sum_{j \mathop \in F} \norm{v_j} \le M$
From Bounded Generalized Sum is Absolutely Convergent:
:$\ds \sum_{j \mathop \in J} \norm{v_j}$ is absolutely net convergent
{{qed}}
Category:Banach Spaces
Category:Generalized Sums
2gkhsjqrk5t2ulnqct7t9ttcyzbrhgk
Theorem: Inequality Rule for Absolutely Convergent Generalized Sums

Let $V$ be a Banach space.
Let $\family {v_i}_{i \mathop \in I}$ be an indexed family of elements of $V$.
Let the generalized sum $\ds \sum \set {v_i: i \in I}$ be absolutely net convergent.
Let $\family {w_i}_{i \mathop \in I}$ be an indexed family of elements of $V$:
:$\forall i \in I : \norm{w_i} \le \norm{v_i}$
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} \norm{w_i}$ is absolutely net convergent
and:
:$\ds \sum_{i \mathop \in I} \norm{w_i} \le \sum_{i \mathop \in I} \norm{v_i}$

Proof:
By definition  of absolutely net convergence, let:
:$\ds \sum_{i \mathop \in I} \norm{v_i} = M$
Let $F \subseteq I$ be finite.
From Absolutely Convergent Generalized Sum Converges to Supremum:
:$\ds \sum_{i \mathop \in F} \norm{v_i} \le M$
So {{Hypothesis}}:
:$\ds \sum_{i \mathop \in F} \norm{w_i}  \le \ds \sum_{i \mathop \in F} \norm{v_i} \le M$
Since $F \subseteq J$ was arbitrary, it follows that:
:$\forall F \subseteq F : F$ is finite $: \ds \sum_{i \mathop \in F} \norm{w_i} \le M$
From Bounded Generalized Sum is Absolutely Convergent:
:$\ds \sum_{i \mathop \in I} \norm{w_i}$ is absolutely net convergent
From Inequality Rule for Real Convergent Nets:
:$\ds \sum_{i \mathop \in I} \norm{w_i} \le \sum_{i \mathop \in I} \norm{v_i}$
{{qed}}
Category:Banach Spaces
Category:Generalized Sums
ozhauu1w38g3eakv7415tb9nf2uwatu