avewright/proofwiki-math huggingface dataset:
Theorem: Generalized Sum is Monotone

Let $I$ be an indexing set.
Let $\family {a_i}_{i \mathop \in I}$ be an $I$-indexed family of positive real numbers.
That is, let $a_i \in \R_{\ge 0}$ for all $i \in I$.
Then, for every finite subset $F$ of $I$:
:$\ds \sum_{i \mathop \in F} a_i \le \sum_{i \mathop \in I} a_i$
provided the generalized sum on the right converges.

Proof:
Let $\struct {\FF, \subseteq}$ be the set of finite subsets of $I$, ordered by inclusion.
From Finite Subsets form Directed Set, $\struct {\FF, \subseteq}$ is directed.
For brevity write:
:$\ds s_X = \sum_{i \mathop \in X} a_i$ 
for $X \in \FF$. 
{{AimForCont}} that:
:$\ds \sum_{i \mathop \in F} a_i > \sum_{i \mathop \in I} a_i$
for some finite subset $F$ of $I$.
Take $\epsilon > 0$ such that:
:$\ds \sum_{i \mathop \in F} a_i > \sum_{i \mathop \in I} a_i + \epsilon$ 
Since $\family {s_X}_{X \mathop \in \FF}$ converges to $\ds \sum_{i \mathop \in I} a_i$, there exists a finite set $G$ such that if $X$ is a finite set with $X \supseteq G$, we have:
:$\ds \size {\sum_{i \mathop \in X} a_i - \sum_{i \mathop \in I} a_i} < \epsilon$ 
Then in particular for $X = F \cup G$ we have:
:$\ds \sum_{i \mathop \in F \cup G} a_i \le \sum_{i \mathop \in I} a_i + \epsilon < \sum_{i \mathop \in F} a_i$ 
However since $F \subseteq F \cup G$ and $a_i \in \R_{\ge 0}$ for each $i \in F \cup G$, we have:
:$\ds \sum_{i \mathop \in F} a_i \le \sum_{i \mathop \in F \cup G} a_i < \sum_{i \mathop \in F} a_i$
a contradiction.
So:
:$\ds \sum_{i \mathop \in F} a_i \le \sum_{i \mathop \in I} a_i$
for each $F \in \FF$.
{{qed}}
Category:Generalized Sums
9048jb4dl5b5cigqull7kij9tf3wrs3
Theorem: Convergent Generalized Sum of Positive Reals has Countably Many Non-Zero Terms

Let $\family {a_i}_{i \mathop \in I}$ be an $I$-indexed family of positive real numbers.
That is, let $a_i \in \R_{\ge 0}$ for all $i \in I$.
Suppose that $\ds \sum \set {a_i: i \in I}$ converges.
Then the set $I_{>0} := \set {i \in I: a_i > 0}$ is countable.

Proof:
For $\lambda \in \R$, let $I_{>\lambda} := \set {i \in I: a_i > \lambda}$.
Then as $\ds \sum \set {a_i: i \mathop \in I}$ converges, necessarily all of the sets $I_{> \frac 1 n}$ are finite.
However, we have that $\ds I_{>0} = \bigcup_{n \mathop = 1}^\infty I_{> \frac 1 n}$.
From Countable Union of Countable Sets is Countable, it follows that $I_{>0}$ is countable.
{{qed}}
Category:Generalized Sums
Category:Real Analysis
jqmssgt1mld6q7ug3afwqsdqj1kpa31
Theorem: Mappings Partially Ordered by Extension

Let $S$ and $T$ be sets.
Let $F$ be the set of all mappings from $S$ to $T$.
Let $\RR \subseteq F \times F$ be the relation defined as:
:$\tuple {f, g} \in \RR \iff \Dom f \subseteq \Dom g \land \forall x \in \Dom f: \map f x = \map g x$
That is, $f \mathrel \RR g$ {{iff}} $g$ is an extension of $f$.
Then $\RR$ is an ordering on $F$.

Proof:
Let $x \in \Dom f$ such that $\map f x = y$.
Then by definition $x \in \Dom g$ and $\map g x = y$.
Thus by definition of subset, $f \subseteq g$.
We have that Subset Relation is Ordering.
Hence the result.
{{qed}}
Theorem: Finite Subsets form Directed Set

Let $I$ be a set.
Denote with $\FF$ the set of finite subsets of $I$.
Let $\subseteq$ be the subset relation on $\FF$.
Then $\struct {\FF, \subseteq}$ is a directed set.

Proof:
A fortiori from Finite Subsets form Directed Ordering.
{{qed}}
Category:Preorder Theory
Category:Subset Relation
3fty8n41x4782vos1tgeqauwf8cdlw6
Theorem: Strictly Precedes is Strict Ordering

Let $\struct {S, \preceq}$ be an ordered set.
Let $\prec$ be the relation on $S$ defined as:
:$a \prec b \iff \paren {a \ne b} \land \paren {a \preceq b}$
That is, $a \prec b$ {{iff}} $a$ strictly precedes $b$.
Then:
:$a \preceq b \iff \paren {a = b} \lor \paren {a \prec b}$
and $\prec$ is a strict ordering on $S$.

Proof:
We are given that $\struct {S, \preceq}$ is an ordered set.
Theorem: Smallest Element is Unique

Let $\struct {S, \preceq}$ be an ordered set.
If $S$ has a smallest element, then it can have only one.
That is, if $a$ and $b$ are both smallest elements of $S$, then $a = b$.

Proof:
Let $a$ and $b$ both be smallest elements of $S$.
Then by definition:
:$\forall y \in S: a \preceq y$
:$\forall y \in S: b \preceq y$
Thus it follows that:
:$a \preceq b$
:$b \preceq a$
But as $\preceq$ is an ordering, it is antisymmetric.
Hence by definition of antisymmetric, $a = b$.
{{qed}}
Theorem: Greatest Element is Unique

Let $\struct {S, \preceq}$ be a ordered set.
If $S$ has a greatest element, then it can have only one.
That is, if $a$ and $b$ are both greatest elements of $S$, then $a = b$.

Proof:
Let $a$ and $b$ both be greatest elements of $S$.
Then by definition:
:$\forall y \in S: y \preceq a$
:$\forall y \in S: y \preceq b$
Thus it follows that:
:$b \preceq a$
:$a \preceq b$
But as $\preceq$ is an ordering, it is antisymmetric.
Hence, by definition of antisymmetric relation, $a = b$.
{{qed}}
Theorem: Smallest Element is Lower Bound

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $T$ have a smallest element $m \in T$.
Then $m$ is a lower bound of $T$.
It follows by definition that $T$ is bounded below.

Proof:
Let $m \in T$ be a smallest element of $T$.
By definition:
:$\forall y \in T: m \preceq y$
But as $T \subseteq S$, it follows that $m \in S$.
Hence:
:$\exists m \in S: \forall y \in T: m \preceq y$
Thus $T$ is bounded below by the lower bound $m$.
{{qed}}
Theorem: Greatest Element is Upper Bound

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $T$ have a greatest element $M \in T$.
Then $M$ is an upper bound of $T$.
It follows by definition that $T$ is bounded above.

Proof:
Let $M \in T$ be a greatest element of $T$.
By definition:
:$\forall y \in T: y \preceq M$
But as $T \subseteq S$, it follows that $M \in S$.
Hence:
:$\exists M \in S: \forall y \in T: y \preceq M$
Thus $T$ is bounded above by the upper bound $M$.
{{qed}}
Theorem: Intersection of Subset with Lower Bounds

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $T_*$ be the set of all lower bounds of $T$ in $S$.
Then $T_* \cap T \ne \O$ {{iff}}:
:$T$ has a smallest element $m$
and
:$T_* \cap T$ is a singleton such that $T_* \cap T = \set m$

Proof:
Suppose $T_* \cap T = \O$, where $\O$ denotes the empty set.
That means $T$ contains none of its lower bounds, if indeed it has any.
From Smallest Element is Lower Bound, if $T$ had a smallest element, it would be a lower bound contained in $T$.
It follows that $T$ can have no smallest element.
Otherwise $T_* \cap T \ne \O$.
That means $T$ contains at least one of its lower bounds.
Suppose $\exists a, b \in T_* \cap T$.
From Intersection is Subset it follows that $a, b \in T$.
Then:
:$\forall y \in T: a \preceq y$
:$\forall y \in T: b \preceq y$
Thus both $a$ and $b$ fulfil the criteria for being a smallest element of $T$.
From Smallest Element is Unique it follows that $a = b$ and so $T_* \cap T$ is a singleton containing the smallest element of $T$.
{{qed}}
Theorem: Intersection of Subset with Upper Bounds

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $T^*$ be the set of all upper bounds of $T$ in $S$.
Then $T^* \cap T \ne \O$ {{iff}}:
:$T$ has a greatest element $M$
and
:$T^* \cap T$ is a singleton such that $T^* \cap T = \set M$

Proof:
Suppose $T^* \cap T = \O$, where $\O$ denotes the empty set.
That means $T$ contains none of its upper bounds, if indeed it has any.
From Greatest Element is Upper Bound, if $T$ had a greatest element, it would be an upper bound contained in $T$.
It follows that $T$ can have no greatest element.
Otherwise $T^* \cap T \ne \O$.
That means $T$ contains at least one of its upper bounds.
Suppose $\exists a, b \in T^* \cap T$.
From Intersection is Subset it follows that $a, b \in T$.
Then:
:$\forall y \in T: y \preceq a$
:$\forall y \in T: y \preceq b$
Thus both $a$ and $b$ fulfill the criteria for being a greatest element of $T$.
From Greatest Element is Unique it follows that $a = b$ and so $T^* \cap T$ is a singleton containing the greatest element of $T$.
{{qed}}
Theorem: Nesbitt's Inequality

Let $a$, $b$ and $c$ be (strictly) positive real numbers.
Then:
:$\dfrac a {b + c} + \dfrac b {a + c} + \dfrac c {a + b} \ge \dfrac 3 2$

Proof:
{{begin-eqn}}
{{eqn | l = \frac a {b + c} + \frac b {a + c} + \frac c {a + b}
      | o = \ge
      | r = \dfrac 3 2
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac {a + b + c} {b + c} + \frac {a + b + c} {a + c} + \frac {a + b + c} {a + b}
      | o = \ge
      | r = \frac 9 2
      | c = by adding $3$
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac {a + b + c} {b + c} + \frac {a + b + c} {a + c} + \frac {a + b + c} {a + b}
      | o = \ge
      | r = \frac {9 \paren {a + b + c} } {\paren {b + c} + \paren {a + c} + \paren {a + b} }
      | c = as $\dfrac {a + b + c} {\paren {b + c} + \paren {a + c} + \paren {a + b} } = \dfrac 1 2$
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac {\frac 1 {b + c} + \frac 1 {a + c} + \frac 1 {a + b} } 3
      | o = \ge
      | r = \frac 3 {\paren {b + c} + \paren {a + c} + \paren {a + b} }
      | c = dividing by $3 \paren {a + b + c}$
}}
{{end-eqn}}
These are the arithmetic mean and the harmonic mean of $\dfrac 1 {b + c}$, $\dfrac 1 {a + c}$ and $\dfrac 1 {a + b}$.
From AM-HM Inequality the last inequality is true.
Thus Nesbitt's Inequality holds.
{{qed}}
Theorem: Nesbitt's Inequality

Let $a$, $b$ and $c$ be (strictly) positive real numbers.
Then:
:$\dfrac a {b + c} + \dfrac b {a + c} + \dfrac c {a + b} \ge \dfrac 3 2$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = S
      | r = \frac a {b + c} + \frac b {c + a} + \frac c {a + b}
}}
{{eqn | l = M
      | r = \frac b {b + c} + \frac c {c + a} + \frac a {a + b}
}}
{{eqn | l = N
      | r = \frac c {b + c} + \frac a {c + a} + \frac b {a + b}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = M + N
      | r = \frac {b + c} {b + c} + \frac {c + a} {c + a} + \frac {a + b} {a + b}
}}
{{eqn | r = 3
}}
{{eqn | n = 2
      | l = S + M
      | r = \frac {a + b} {b + c} + \frac {b + c} {c + a} + \frac {c + a} {a + b}
}}
{{eqn | o = \ge
      | r = 3 \sqrt [3] {\frac {a + b} {b + c} \cdot \frac {b + c} {c + a} \cdot \frac {c + a} {a + b} }
      | c = Cauchy's Mean Theorem
}}
{{eqn | r = 3
}}
{{eqn | n = 3
      | l = N + S
      | r = \frac {c + a} {b + c} + \frac {a + b} {c + a} + \frac {b + c} {a + b}
}}
{{eqn | o = \ge
      | r = 3 \sqrt [3] {\frac {c + a} {b + c} \cdot \frac {a + b} {c + a} \cdot \frac {b + c} {a + b} }
      | c = Cauchy's Mean Theorem
}}
{{eqn | r = 3
}}
{{end-eqn}}
From $(2)$ and $(3)$:
:$(4): \quad M + N + 2 S \ge 6$
From $(1)$ and $(4)$:
{{begin-eqn}}
{{eqn | l = 2 S
      | o = \ge
      | r = 3
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \ge
      | r = \frac 3 2
}}
{{end-eqn}}
{{qed}}
Theorem: Greatest Element is Maximal

Let $\struct {S, \preceq}$ be an ordered set which has a greatest element.
Let $M$ be the greatest element of $\struct {S, \preceq}$.
Then $M$ is a maximal element.

Proof:
By definition of greatest element:
:$\forall y \in S: y \preceq M$
Suppose $M \preceq y$.
As $\preceq$ is an ordering, $\preceq$ is by definition antisymmetric.
Thus it follows by definition of antisymmetry that $M = y$.
That is:
:$M \preceq y \implies M = y$
which is precisely the definition of a maximal element.
{{qed}}
Theorem: Smallest Element is Minimal

Let $\struct {S, \preceq}$ be an ordered set which has a smallest element.
Let $m$ be the smallest element of $\struct {S, \preceq}$.
Then $m$ is a minimal element.

Proof:
By definition of smallest element:
:$\forall y \in S: m \preceq y$
Suppose $y \preceq m$.
As $\preceq$ is an ordering, $\preceq$ is by definition antisymmetric.
Thus it follows by definition of  antisymmetry that $m = y$.
That is:
:$y \preceq m \implies m = y$
which is precisely the definition of a minimal element.
{{qed}}
Theorem: Minimal Element in Toset is Unique and Smallest

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $m$ be a minimal element of $\struct {S, \preceq}$.
Then:
:$(1): \quad m$ is the smallest element of $\struct {S, \preceq}$
:$(2): \quad m$ is the only minimal element of $\struct {S, \preceq}$.

Proof:
By definition of minimal element:
:$\forall y \in S: y \preceq m \implies m = y$
As $\struct {S, \preceq}$ is a totally ordered set, by definition $\preceq$ is connected.
That is:
:$\forall x, y \in S: y \preceq x \lor x \preceq y$
It follows that:
:$\forall y \in S: m = y \lor m \preceq y$
But as $m = y \implies m \preceq y$ by definition of $\preceq$, it follows that:
:$\forall y \in S: m \preceq y$
which is precisely the definition of smallest element.
Hence $(1)$ holds.
{{qed|lemma}}
Suppose $m_1$ and $m_2$ are both minimal elements of $S$.
By $(1)$ it follows that both are smallest elements.
It follows from Smallest Element is Unique that $m_1 = m_2$.
That is, $(2)$ holds.
{{qed}}
Theorem: Maximal Element in Toset is Unique and Greatest

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $M$ be a maximal element of $\struct {S, \preceq}$.
Then:
:$(1): \quad M$ is the greatest element of $\struct {S, \preceq}$.
:$(2): \quad M$ is the only maximal element of $\struct {S, \preceq}$.

Proof:
By definition of maximal element:
:$\forall y \in S: M \preceq y \implies M = y$
As $\struct {S, \preceq}$ is a totally ordered set, by definition $\preceq$ is a connected.
That is:
:$\forall x, y \in S: y \preceq x \lor x \preceq y$
It follows that:
:$\forall y \in S: M = y \lor y \preceq M$
But as $M = y \implies y \preceq M$ by definition of $\preceq$, it follows that:
:$\forall y \in S: y \preceq M$
which is precisely the definition of greatest element.
Hence $(1)$ holds.
{{qed|lemma}}
Suppose $M_1$ and $M_2$ are both maximal elements of $S$.
By $(1)$ it follows that both are greatest elements.
It follows from Greatest Element is Unique that $M_1 = M_2$.
That is, $(2)$ holds.
{{qed}}
Theorem: Whitney Embedding Theorem

Every smooth $m$-dimensional manifold admits a smooth embedding into Euclidean space $\R^{2 m}$.

Proof:
{{ProofWanted}}
{{Namedfor|Hassler Whitney|cat = Whitney, H.}}
Theorem: Max Semigroup is Idempotent

Let $\struct {S, \preceq}$ be a totally ordered set.
Then the semigroup $\struct {S, \max}$ is an idempotent semigroup.

Proof:
The fact that $\struct {S, \max}$ is a semigroup is demonstrated in Max Operation on Toset forms Semigroup.
Then the max operation is idempotent:
:$\forall x \in S: \max \set {x, x} = x$
The result follows by the definition of idempotent semigroup.
{{qed}}
Theorem: Continuity of Linear Transformations

Let $H, K$ be Hilbert spaces, and let $A: H \to K$ be a linear transformation.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$A$ is continuous}}
{{item|(2):|$A$ is continuous at $\mathbf 0_H$}}
{{item|(3):|$A$ is continuous at some point}}
{{item|(4):|$\exists c > 0: \forall h \in H: \norm {\map A h}_K \le c \norm h_H$}}
{{end-itemize}}

Proof:
It is clear that $(1) \implies (2) \implies (3)$.
For $(4) \implies (2)$:
For any $\epsilon > 0$, there exists $\delta = \dfrac \epsilon c$, such that when $\norm {\mathbf 0_H - h}_H < \delta$:
:$\norm {\map A h - \map A {\mathbf 0_H} }_K \le c \norm h_H < c\delta = \epsilon$
Now we prove $(3) \implies (1)$:
Let $A$ be continuous at some point $h_0$.
For any sequence $h_n \to h$ in $H$:
:$h_n - h + h_0 \to h_0$
Hence:
:$\ds \lim_{n \mathop \to \infty} \map A {h_n - h + h_0} = \lim_{n \mathop \to \infty} \map A {h_n} - \map A h + \map A {h_0} = \map A {h_0}$
We see that:
:$\ds \lim_{n \mathop \to \infty} \map A {h_n} = \map A h$
Thus $A$ is continuous.
Now for the proof $(2) \implies (4)$.
We have that $A$ is continuous at $\mathbf 0_H$.
Hence there exists an open ball of positive real radius $a$, centered at $\mathbf 0_H$, such that its image under $A$ is included in the open ball of radius $1$, centered at $\mathbf 0_K$. 
This is, if $\norm h_H < a$, then:
:$\norm {\map A h}_K < 1$
Let $h$ be an arbitrary element in $H$.
Let $\epsilon > 0$.
We have:
:$\norm {\dfrac a {\norm h_H + \epsilon} h}_H < a$
Hence:
:$\norm {\map A {\dfrac a {\norm h_H + \epsilon} h} }_K = \dfrac a {\norm h_H + \epsilon} \norm {\map A h}_K < 1$
Therefore:
:$\norm {\map A h}_K < \dfrac 1 a \norm h_H + \dfrac \epsilon a$
Let $\epsilon \to 0$.
Therefore, we can take:
:$c := \dfrac 1 a$
{{qed}}
Theorem: Equivalence of Definitions of Norm of Linear Transformation

Let $H, K$ be Hilbert spaces.
Let $A: H \to K$ be a bounded linear transformation.
{{TFAE|def = Norm on Bounded Linear Transformation}}

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \lambda_1
      | r = \sup \set {\norm {A h}_K: \norm h_H \le 1}
}}
{{eqn | l = \lambda_2
      | r = \sup \set {\dfrac {\norm {A h}_K} {\norm h_H}: h \in H, h \ne 0_H}
}}
{{eqn | l = \lambda_3
      | r = \sup \set {\norm {A h}_K: \norm h_H = 1}
}}
{{eqn | l = \lambda_4
      | r = \inf \set {c > 0: \forall h \in H: \norm {A h}_K \le c \norm h_H}
}}
{{end-eqn}}
From Norm on Bounded Linear Transformation is Finite:
:$\lambda_4 < \infty$
We will show that:
:$\lambda_4 \ge \lambda_2 \ge \lambda_1 \ge \lambda_3 \ge \lambda_4$
Theorem: Max Semigroup on Toset forms Semilattice

Let $\struct {S, \preceq}$ be a totally ordered set. 
Then the max semigroup $\struct {S, \max}$ is a semilattice.

Proof:
The Max Semigroup is Commutative and idempotent. 
Hence the result, by definition of a semilattice.
{{qed}}
Theorem: Max Operation Yields Supremum of Parameters

Let $\struct {S, \preceq}$ be a totally ordered set. 
Let $x, y \in S$.
Then:
:$\max \set {x, y} = \sup \set {x, y}$
where:
:$\max$ denotes the max operation
:$\sup$ denotes the supremum.

Proof:
As $\struct {S, \preceq}$ be a totally ordered set, all elements of $S$ are $\preceq$-comparable.
Therefore there are two cases to consider:
Theorem: Mappings to Vector Space form Vector Space

Let $X$ be a non-empty set.
Let $V$ be a vector space over a field (or division ring) $K$.
Let $V^X$ denote the set of all mappings from $X$ to $V$.
Let $+$ denote pointwise addition on $V^X$.
Let $\circ$ denote pointwise ($K$)-scalar multiplication on $V^X$.
Then $\struct {V^X, +, \circ}_K$ is a vector space over $K$.

Proof:
{{ProofWanted}}
Category:Vector Spaces
jibm3x64dds1jlq3x2ncpdml0gfa8az
Theorem: Equivalence of Formulations of Pasch's Axiom

The two forms of Pasch's Axiom in Tarski's Geometry are consistent.
That is, the expressions:
:$(1): \quad \forall a, b, c, p, q: \exists x: \mathsf B a p c \land \mathsf B b q c \implies \mathsf B p x b \land \mathsf B q x a$
and:
:$(2): \quad \forall a, b, c, p, q: \exists x: \mathsf B a p c \land \mathsf B q c b \implies \mathsf B a x q \land \mathsf B b p x$
are logically equivalent.

Proof:
{{proof wanted|It is important that we identify which other axioms this equivalence is based on for foundational purposes (and possible generalisations)}}
Theorem: Square-Summable Indexed Sets Closed Under Addition

Let $\family {a_i}_{i \mathop \in I}, \family {b_i}_{i \mathop \in I}$ be $I$-indexed families of real numbers.
Let:
{{begin-eqn}}
{{eqn | l = \sum \set { {a_i}^2: i \in I}
      | o = <
      | r = \infty
}}
{{eqn | l = \sum \set { {b_i}^2: i \in I}
      | o = <
      | r = \infty
}}
{{end-eqn}}
where $\ds \sum$ denotes the generalized sums.
Then:
:$\ds \sum \set {\paren {a_i + b_i}^2: i \in I} < \infty$

Proof:
First we note that:
:$\forall i \in I: {a_i}^2 > 0$ and ${b_i}^2 > 0$
This will be used throughout implicitly.
There are two cases to consider: $a_i b_i < 0$ and $a_i b_i > 0$.
Theorem: Generalized Sum Preserves Inequality

Let $\family {a_i}_{i \mathop \in I}, \family {b_i}_{i \mathop \in I}$ be $I$-indexed families of positive real numbers.
That is, let $a_i, b_i \in \R_{\ge 0}$ for all $i \in I$.
Suppose that for all $i \in I$, $a_i \le b_i$.
Furthermore, suppose that $\ds \sum \set {b_i: i \in I}$ converges.
Then:
:$\ds \sum \set {a_i: i \in I} \le \sum \set {b_i: i \in I}$
In particular, $\ds \sum \set {a_i: i \in I}$ converges.

Proof:
First, it is proven that $\ds \sum \set {a_i: i \in I}$ converges.
Then, the inequality $\ds \sum \set {a_i: i \in I} \le \sum \set {b_i: i \in I}$ is well-defined, and hence can be proven.
Theorem: Generalized Sum is Linear

Let $\family {z_i}_{i \mathop \in I}$ and $\family {w_i}_{i \mathop \in I}$ be $I$-indexed families of complex numbers.
That is, let $z_i, w_i \in \C$ for all $i \in I$.
Let $\ds \sum \set {z_i: i \in I}$ and $\sum \set {w_i: i \mathop \in I}$ converge to $z, w \in \C$, respectively.
Then:
:$(1): \quad \ds \sum \set {z_i + w_i: i \in I}$ converges to $z + w$
:$(2): \quad \forall \lambda \in \C: \ds \sum \set {\lambda z_i: i \in I}$ converges to $\lambda z$

Proof:
=== Proof of $(1)$ ===
Let $\epsilon > 0$.
To verify the convergence, it is necessary to find a finite $F \subseteq I$ such that:
:$\ds \map d {\sum_{i \mathop\in G} z_i + w_i, z + w} < \epsilon$ for all finite $G$ with $F \subseteq G \subseteq I$
Now let $F_z, F_w \subseteq I$ be finite subsets of $I$ such that:
:$\ds \map d {\sum_{i \mathop \in G} z_i, z} < \frac \epsilon 2$ for all finite $G$ with $F_z \subseteq G \subseteq I$
:$\ds \map d {\sum_{i \mathop \in G} w_i, w} < \frac \epsilon 2$ for all finite $G$ with $F_w \subseteq G \subseteq I$
The set $F_z \cup F_w$ will be the sought $F$. Let $G$ be finite such that $F_z \cup F_w \subseteq G \subseteq I$.
It follows that:
{{begin-eqn}}
{{eqn | l = \map d {\sum_{i \mathop \in G} z_i + w_i, z + w}
      | r = \size {\paren {\sum_{i \mathop \in G} z_i + w_i} - \paren {z + w} }
      | c = {{Defof|Metric Induced by Norm}}
}}
{{eqn | r = \size {\paren {\sum_{i \mathop \in G} z_i - z} + \paren {\sum_{i \mathop \in G} w_i - w} }
}}
{{eqn | o = \le
      | r = \size {\paren {\sum_{i \mathop \in G} z_i - z} } + \size {\paren {\sum_{i \mathop \in G} w_i, w} }
      | c = Triangle Inequality for $\size {\, \cdot \,}$
}}
{{eqn | r = \map d {\sum_{i \mathop\in G} z_i, z} + \map d {\sum_{i \mathop\in G} w_i, w}
      | c = {{Defof|Metric Induced by Norm}}
}}
{{eqn | o = <
      | r = \epsilon
      | c = $F_z, F_w \subseteq G$
}}
{{end-eqn}}
From the definition of convergence, it is concluded that:
:$\ds \sum \set {z_i + w_i: i \in I} = z + w$
{{qed|lemma}}
Theorem: Min Operation Yields Infimum of Parameters

Let $\struct {S, \preceq}$ be a totally ordered set. 
Let $x, y \in S$.
Then:
:$\map \min {x, y} = \map \inf {\set {x, y} }$
where:
:$\min$ denotes the min operation
:$\inf$ denotes the infimum.

Proof:
As $\struct {S, \preceq}$ be a totally ordered set, all elements of $S$ are $\preceq$-comparable.
Therefore there are two cases to consider:
Theorem: Convergence of Generalized Sum of Complex Numbers

Let $\family {z_j}_{j \mathop \in I}$ be an $I$-indexed family of complex numbers.
That is, let $z_j \in \C$ for all $j \in I$.
Let $\map \Re {z_j}$ and $\map \Im {z_j}$ denote the families of real and imaginary parts of the family $z_j$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\ds \sum_{j \mathop \in I} z_j$ converges to $z \in \C$}}
{{item|(2):|$\ds \sum_{j \mathop \in I} \map \Re {z_j}, \sum_{j \mathop \in I} \map \Im {z_j}$ converge to $\map \Re z, \map \Im z \in \R$, respectively}}
{{end-itemize}}

Proof:
=== $(2)$ implies $(1)$ ===
By Generalized Sum is Linear, the stated convergences lead to:
{{begin-eqn}}
{{eqn | l = z
      | r = \map \Re z + i \map \Im z
      | c = {{Defof|Real Part}} and {{Defof|Imaginary Part}}
}}
{{eqn | r = \sum_{j \mathop \in I} \map \Re {z_j} + i \sum_{j \mathop \in I} \map \Im {z_j}
      | c = Statement $(2)$
}}
{{eqn | r = \sum_{j \mathop \in I} \paren {\map \Re {z_j} + i \map \Im {z_j} }
      | c = Generalized Sum is Linear
}}
{{eqn | r = \sum_{j \mathop \in I} z_j
      | c = {{Defof|Real Part}} and {{Defof|Imaginary Part}}
}}
{{end-eqn}}
{{qed|lemma}}