avewright/proofwiki-math huggingface dataset:
Theorem: Finite Ordinal is not Subset of one of its Elements

Let $n$ be a finite ordinal.
Then:
:$\nexists x \in n: n \subseteq x$
that is, $n$ is not a subset of one of its elements.

Proof:
Let $S$ be the set of all those finite ordinals $n$ which are not a subset of any of its elements.
That is:
:$n \in S \iff n \in \omega \land \forall x \in n: n \nsubseteq x$
We know that $0 = \O$ is not a subset of any of its elements, as $\O$ by definition has no elements.
So $0 \in S$.
Now suppose $n \in S$.
From Set is Subset of Itself:
:$n \subseteq n$
But as $n \in S$ it follows by definition of $S$ that:
:$n \notin n$
By definition of the successor of $n$, it follows that:
:$n^+ \nsubseteq n$
Now from Subset Relation is Transitive:
:$n^+ \subseteq x \implies n \subseteq x$
But since $n \in S$ it follows that:
:$x \notin n$
So:
:$n^+ \nsubseteq n$
and:
:$\forall x \in n: n^+ \nsubseteq x$
So $n^+$ is not a subset of any of its elements.
That is:
:$n^+ \in S$
So by the Principle of Mathematical Induction:
:$S = \omega$
Hence the result.
{{qed}}
Theorem: Element of Minimally Inductive Set is Transitive Set

Let $\omega$ be the minimally inductive set.
Let $n \in \omega$.
Then $x \in n \implies x \subseteq n$.
That is, every element of $n$ is also a subset of it.
In other words, each element of $\omega$ is a transitive set.

Proof:
Let $S \subseteq$ be the set of all transitive elements of $\omega$.
That is:
:$n \in S \iff n \in \omega \land \forall x \in n: x \subseteq n$
It is vacuously true that $0 \in S$, as there are no $x \in 0$.
Now suppose $n \in S$.
If $x \in n^+$ then either $x \in n$ or $x = n$.
In the first case:
:$x \subseteq n$ as $n \in S$
and so:
:$x \subseteq n^+$
In the second case, by definition of successor set:
:$x \subseteq n^+$
By Principle of Mathematical Induction for Minimally Inductive Set it follows that:
:$S = \omega$
Hence the result.
{{qed}}
Theorem: Primitive of Exponential Function

:$\ds \int e^x \rd x = e^x + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {a^x}
      | r = a^x \ln a
      | c = Derivative of General Exponential Function
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\dfrac {a^x} {\ln a} }
      | r = a^x
      | c = Derivative of Constant Multiple
}}
{{eqn | ll= \leadsto
      | l = \int a^x \rd x
      | r = \dfrac {a^x} {\ln a}
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential Function

:$\ds \int e^x \rd x = e^x + C$
where $C$ is an arbitrary constant.

Proof:
Let $u = x \ln a$.
{{begin-eqn}}
{{eqn | l = \int a^x \rd x
      | r = \int \map \exp {x \ln a} \rd x
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \frac 1 {\ln a} \int \map \exp u \rd u
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = \frac {\map \exp u} {\ln a} + C
      | c = Primitive of Exponential Function
}}
{{eqn | r = \frac {\map \exp {x \ln a} } {\ln a} + C
      | c = Definition of $u$
}}
{{eqn | r = \frac {a^x} {\ln a} + C
      | c = {{Defof|Power to Real Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Natural Number Addition Commutes with Zero

Let $\N$ be the natural numbers.
Then:
:$\forall n \in \N: 0 + n = n = n + 0$

Proof:
Proof by induction:
From definition of addition:
{{begin-eqn}}
{{eqn | q = \forall m, n \in \N
      | l = m + 0
      | r = m
      | c = 
}}
{{eqn | l = m + n^+
      | r = \paren {m + n}^+
      | c = 
}}
{{end-eqn}}
For all $n \in \N$, let $\map P n$ be the proposition:
:$0 + n = n = n + 0$
Theorem: Natural Number Addition Commutativity with Successor

Let $\N$ be the natural numbers.
Then:
:$\forall m, n \in \N: m^+ + n = \paren {m + n}^+$

Proof:
Proof by induction:
From definition of addition:
{{begin-eqn}}
{{eqn | q = \forall m, n \in \N
      | l = m + 0
      | r = m
      | c = 
}}
{{eqn | l = m + n^+
      | r = \paren {m + n}^+
      | c = 
}}
{{end-eqn}}
For all $n \in \N$, let $\map P n$ be the proposition:
:$\forall m \in \N: m^+ + n = \paren {m + n}^+$
=== Basis for the Induction ===
From definition of addition:
{{begin-eqn}}
{{eqn | q = \forall m \in \N
      | l = m^+ + 0
      | r = m^+
      | c = 
}}
{{eqn | r = \paren {m + 0}^+
      | c = 
}}
{{end-eqn}}
Thus $\map P 0$ is seen to be true.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k^+}$ is true.
So this is our induction hypothesis $\map P k$:
:$\forall m \in \N: m^+ + k = \paren {m + k}^+$
Then we need to show that $\map P {k^+}$ follows directly from $\map P k$:
:$\forall m \in \N: m^+ + k^+ = \paren {m + k^+}^+$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = m^+ + k^+
      | r = \paren {m^+ + k}^+
      | c = {{Defof|Addition in Minimally Inductive Set|Addition}}
}}
{{eqn | r = \paren {\paren {m + k}^+}^+
      | c = induction hypothesis
}}
{{eqn | r = \paren {m + k^+}^+
      | c = {{Defof|Addition in Minimally Inductive Set|Addition}}
}}
{{end-eqn}}
So $\map P k \implies \map P {k^+}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall m, n \in \N: m^+ + n = \paren {m + n}^+$
{{qed}}
Theorem: Natural Number Addition Commutativity with Successor

Let $\N$ be the natural numbers.
Then:
:$\forall m, n \in \N: m^+ + n = \paren {m + n}^+$

Proof:
Using the following axioms:
{{:Axiom:Axiomatization of 1-Based Natural Numbers}}
Proof by induction:
From Axiomatization of $1$-Based Natural Numbers, we have by definition that:
{{begin-eqn}}
{{eqn | q = \forall m, n \in \N
      | l = m + 0
      | r = m
}}
{{eqn | l = \paren {m + n}^+
      | r = m + n^+
}}
{{end-eqn}}
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\forall m \in \N_{> 0}: \paren {m + 1} + n = \paren {m + n} + 1$
=== Basis for the Induction ===
When $n = 1$, we have:
:$\paren {m + 1} + 1 = \paren {m + 1} + 1$
which holds trivially.
Thus $\map P 1$ is seen to be true.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis $\map P k$:
:$\forall m \in \N: \paren {m + 1} + k = \paren {m + k} + 1$
Then we need to show that $\map P {k^+}$ follows directly from $\map P k$:
:$\forall m \in \N: \paren {m + 1} + \paren {k + 1} = \paren {m + \paren {k + 1} } + 1$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \paren {m + \paren {k + 1} } + 1
      | r = \paren {\paren {m + k} + 1} + 1
      | c = Natural Number Addition is Associative/Proof 3
}}
{{eqn | r = \paren {\paren {m + 1} + k} + 1
      | c = Induction Hypothesis
}}
{{eqn | r = \paren {m + 1} + \paren {k + 1}
      | c = Natural Number Addition is Associative/Proof 3
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall m, n \in \N_{> 0}: \paren {m + 1} + n = \paren {m + n} + 1$
{{qed}}
Theorem: Natural Numbers are Comparable

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then $m$ and $n$ are comparable by the ordering relation $\le$.
That is, either:
:$(1): \quad m \le n$
or:
:$(2): \quad n \le m$
or possibly both.

Proof:
Let $\N$ be defined as the minimally inductive set $\omega$.
By definition of the ordering on minimally inductive set:
:$m \le n \iff \begin {cases} m = n & \text {or} \\ m \in n & \end {cases}$
Thus it is sufficient to prove that exactly one of the following is the case:
:$(1): \quad m \in n$
:$(2): \quad m = n$
:$(3): \quad n \in m$
The proof operates by induction:
For each $n \in \omega$, let $\map S n$ be the set of all $m \in \omega$ which are comparable with $n$.
Let $S$ be the set of all $n \in \N$ for which $\map S n = \omega$.
Thus the proof is equivalent to demonstrating that $S = \omega$.
=== Basis for the Induction ===
First consider $\map S 0$.
Clearly $0 \in \map S 0$ as $0 = 0$.
Let $m \in \map S 0$.
Then $m \notin 0$ as $0 = \O$.
So either:
:$(1): \quad 0 = m$, in which case $0 \in m^+$ by definition of successor set
or:
:$(2): \quad 0 \in m$, in which case, because $m \in m^+$ by definition of successor set, again $0 \in m^+$.
In all cases, $m \in \map S 0 \implies m^+ \in \map S 0$.
So $\map S 0 = \omega$ by induction.
This is the basis for the induction.
=== Induction Hypothesis ===
The induction hypothesis is that:
:$\map S k = \omega$
for some $k \in \omega$.
It is now necessary to show that it follows that:
:$\map S {k^+} = \omega$
=== Induction Step ===
This is the induction step:
Consider the set $\map S {k^+}$, given that $\map S k = \omega$.
From the basis for the induction, we have that $k^+ \in \map S 0$.
That is, $k^+$ is comparable with $0$.
So $0$ is comparable with $k^+$ and so $0 \in \map S {k^+}$.
Suppose $m \in \map S {k^+}$.
Then either:
:$(1): \quad k^+ \in m$, in which case $k^+ \in m^+$
or:
:$(2): \quad k^+ = m$, in which case the same applies: $k^+ \in m^+$
or:
:$(3): \quad m \in k^+$.
In case $(3)$, either:
:$(3 \text a): \quad m = k$, in which case $m^+ = k^+$
or:
:$(3 \text b): \quad m \in k$.
Case $(3 \text b)$ is treated as follows.
We have that $m^+ \in \map S k$ by the induction hypothesis.
Therefore, either:
:$(4 \text a): \quad k \in m^+$
or:
:$(4 \text b): \quad k = m^+$
or:
:$(4 \text c): \quad m^+ \in k$.
$(4 \text a)$ is not compatible with $m \in k$, because either:
:$k \in m$
or
:$k = m$
and so $k \subseteq m$ which contradicts Finite Ordinal is not Subset of one of its Elements.
Both $(4 \text b)$ and $(4 \text c)$ imply that $m^+ \in n^+$.
Hence $\map S {k^+} = \omega$.
It follows by the Principle of Finite Induction that $S = \omega$.
{{qed|lemma}}
It then follows from Finite Ordinal is not Subset of one of its Elements that it is not possible for more than one of:
:$(1): \quad m \in n$
:$(2): \quad m = n$
:$(3): \quad n \in m$
to be true at the same time.
{{qed}}
Theorem: Natural Numbers are Comparable

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then $m$ and $n$ are comparable by the ordering relation $\le$.
That is, either:
:$(1): \quad m \le n$
or:
:$(2): \quad n \le m$
or possibly both.

Proof:
Let $\N$ be defined as the von Neumann construction $\omega$.
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
Then from Minimally Inductive Class under Progressing Mapping induces Nest, $\omega$ is a nest in which:
:$\forall m, n \in \omega: \map g x \subseteq y \lor y \subseteq x$
From the definition of $\map g x$ in this context:
:$\forall x \in \omega: \map g x = x^+$
That is:
:$\forall m, n \in \N: m + 1 \subseteq n \lor n \subseteq m$
whence the result.
{{qed}}
Theorem: Natural Numbers are Comparable

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then $m$ and $n$ are comparable by the ordering relation $\le$.
That is, either:
:$(1): \quad m \le n$
or:
:$(2): \quad n \le m$
or possibly both.

Proof:
{{ProofWanted|Proof using Minimally Inductive Class under Slowly Progressing Mapping is Nest by exploiting Successor Mapping is Slowly Progressing.}}
Theorem: Zero is Zero Element for Natural Number Multiplication

Let $\N$ be the natural numbers.
Then $0$ is a zero element for multiplication:
:$\forall n \in \N: 0 \times n = 0 = n \times 0$

Proof:
Proof by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:$0 \times n = 0 = n \times 0$
Theorem: Hilbert Space Isomorphism is Equivalence Relation

Hilbert space isomorphism is an equivalence relation.

Proof:
Checking the three defining properties of an equivalence relation in turn:
Theorem: Element of Finite Ordinal iff Subset

Let $m, n$ be distinct finite ordinals.
Then:
:$m \in n \iff m \subseteq n$

Proof:
Let $m \in n$.
Since $n$ is an ordinal, it is transitive.
Therefore, it follows directly that $m \subseteq n$.
Now let $m \subseteq n$.
We have by hypothesis that $m \ne n$.
From Natural Numbers are Comparable it follows that either $m \in n$ or $n \in m$.
Suppose $n \in m$.
Then $\exists x \in m: m \subseteq x$ which contradicts Finite Ordinal is not Subset of one of its Elements.
The only option left is that $m \in n$.
Hence the result.
{{qed}}
Theorem: Ordering on Natural Numbers is Compatible with Addition

Let $m, n, k \in \N$ where $\N$ is the set of natural numbers.
Then:
:$m < n \iff m + k < n + k$

Proof:
Proof by induction:
For all $k \in \N$, let $\map P k$ be the proposition:
:$m < n \iff m + k < n + k$
$\map P 0$ is true, as this just says $m + 0 = m < n = n + 0$.
This is our basis for the induction.
Theorem: Hilbert Space Isomorphism is Bijection

Let $H, K$ be Hilbert spaces.
Denote by $\innerprod \cdot \cdot_H$ and $\innerprod \cdot \cdot_K$ their respective inner products.
Let $U: H \to K$ be an isomorphism.
Then $U$ is a bijection.

Proof:
As $U$ is an isomorphism, it is necessarily surjective.
Suppose now that $g, h \in H$ are such that $\map U g = \map U h$.
Then as $U$ is a linear map, it follows that $\map U {g - h} = \bszero_K$, the zero vector of $K$.
From property $(3)$ of an isomorphism, conclude that:
:$0 = \innerprod {\bszero_K} {\bszero_K}_K = \innerprod {\map U {g - h} } {\map U {g - h} }_K = \innerprod {g - h} {g - h}_H$
Property $(5)$ of an inner product ensures us that $g - h = \bszero_H$, that is $g = h$.
Hence $U$ is injective.
As $U$ is both injective and surjective, it is a bijection.
{{qed}}
Category:Hilbert Spaces
h2skvnfesr02phgce1ee7vtrpwssknh
Theorem: Surjection that Preserves Inner Product is Linear

Let $H, K$ be Hilbert spaces, and denote by ${\innerprod \cdot \cdot}_H$ and ${\innerprod \cdot \cdot}_K$ their respective inner products.
Let $U: H \to K$ be a surjection such that:
:$\forall g, h \in H: {\innerprod g h}_H = {\innerprod {Ug} {Uh} }_K$
Then $U$ is a linear map, and hence an isomorphism.

Proof:
Let $x, y \in H$.
Let $\alpha \in \GF$.
By surjectivity of $U$, choose $z \in H$ such that $Uz = \map U {\alpha x + y} - \paren { \alpha Ux + Uy }$.
Then:
{{begin-eqn}}
{{eqn | l = {\innerprod {Uz} {Uz} }_K
      | r = {\innerprod {\map U {\alpha x + y} - \paren{\alpha Ux + Uy } } {Uz} }_K
}}
{{eqn | r = {\innerprod {\map U {\alpha x + y} } {Uz} }_K - \paren{ \alpha {\innerprod {Ux} {Uz} }_K + {\innerprod {Uy} {Uz} }_K}
      | c = by linearity in the first coordinate
}}
{{eqn | r = {\innerprod {\alpha x + y} z }_H - \paren{ \alpha {\innerprod x z }_H + {\innerprod y z }_H}
      | c = as $U$ preserves the inner product
}}
{{eqn | r = 0
      | c = by linearity in the first coordinate
}}
{{end-eqn}}
By positivity, $Uz = {\bf 0}_K$.
Hence:
:$\map U {\alpha x + y} = \alpha U x + U y$
Thus, $U$ is linear.
{{qed}}
Theorem: Linear Operator on General Logarithm

Let $\phi: \R^\R \to \R^\R, y \mapsto \map \phi y$ be a linear operator on the space of functions from $\R\to\R$.
Let $y$ be a real function such that:
:$\forall x \in \R: \map y x > \map \bszero x = 0$.
Let $\log_a y$ be the logarithm of $y$ to base $a$.
Then:
:$\map \phi {\log_a y} = \dfrac 1 {\ln a} \paren {\map \phi {\ln y} }$
where $\ln$ is the natural logarithm.

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {\log_a y}
      | r = \map \phi {\frac {\ln y}{\ln a} }
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac 1 {\ln a} \paren {\map \phi {\ln y} }
      | c = {{Defof|Linear Operator}}
}}
{{end-eqn}}
{{qed}}
Category:Linear Operators
Category:Logarithms
jrexc2dlq51lr59wq4z0hkwxy9y6hva
Theorem: Ordering on Natural Numbers is Compatible with Multiplication

Let $m, n, k \in \N$ where $\N$ is the set of natural numbers.
Let $k \ne 0$.
Then:
:$m < n \iff m \times k < n \times k$

Proof:
Proof by induction:
First we note that if $k = 0$ then $m \times k = 0 = n \times k$ whatever $m$ and $n$ are, and the proposition clearly does not hold.
So, for all $k \in \N \setminus \set 0$, let $\map P k$ be the proposition:
:$m < n \iff m \times k < n \times k$
From Identity Element of Natural Number Multiplication is One:
:$m \times 1 = m < n = n \times 1$
and so $\map P 1$ is true.
This is our basis for the induction.
Theorem: Natural Number Ordering is Transitive

Let $m, n, k \in \N$ where $\N$ is the set of natural numbers.
Let $<$ be the relation defined on $\N$ such that:
:$m < n \iff m \in n$
where $\N$ is defined as the minimally inductive set $\omega$.
Then:
:$k < m, m < n \implies k < n$
That is: $<$ is a transitive relation.

Proof:
Let $k < m, m < n$.
By definition it follows that $k \in m, m \in n$.
We have from Element of Finite Ordinal iff Subset that:
:$k \in m \iff k \subseteq m$
:$m \in n \iff m \subseteq n$
It follows from Subset Relation is Transitive that $k \subseteq n$.
Hence the result.
{{qed}}
Category:Natural Numbers
dkmzf5dhzfezvnoysnhrzgvt227sly4
Theorem: Proper Subset of Finite Ordinal is Equivalent to Smaller Ordinal

Let $n$ be a finite ordinal.
Let $x \subsetneq n$.
Then for some finite ordinal $m < n$:
:$m \sim x$
where $m \sim x$ denotes that $m$ is (set) equivalent to $x$.
That is, every proper subset of a finite ordinal $n$ is equivalent to some finite ordinal smaller than $n$.

Proof:
Proof by induction:
For all finite ordinals $n$, let $\map P n$ be the proposition:
:$x \subsetneq n \implies \exists m \in \N: m < n: m \sim x$
$\map P 0$ is vacuously true, as there are no proper subsets of $0 = \O$.
This is our basis for the induction.
Theorem: Hilbert Space Direct Sum is Hilbert Space

Let $\sequence {H_i}_{i \mathop \in I}$ be a $I$-indexed family of Hilbert spaces over $\Bbb F \in \set {\R, \C}$.
Let $H = \ds \bigoplus_{i \mathop \in I} H_i$ be their Hilbert space direct sum.
Then $H$ is a Hilbert space.

Proof:
{{Proofread}}
{{wtd|I think some of the partial results are up on their own pages now, and thus can be replaced by a reference (or this should become the case).
Furthermore, this is *so* long, transclusions and/or foldable templates are a must}}
Theorem: Morera's Theorem

Let $D$ be a simply connected domain in $\C$.
Let $f: D \to \C$ be a continuous function.
Let $f$ be such that:
:$\ds \int_\gamma \map f z \rd z = 0$
for every simple closed contour $\gamma$ in $D$
Then $f$ is analytic on $D$.

Proof:
For a fixed $z_0 \in D$ and $z \in D$ we consider the function:
:$\ds \map F z = \int_\gamma \map f w \rd w$
where $\gamma$ is any (simple) contour starting at $z_0$ and ending at $z$.
By Primitive of Function on Connected Domain, $F$ is a primitive of $f$.
Since $F$ is analytic and $F' = f$, we conclude that $f$ is analytic as well.
{{qed}}
Theorem: Relation is Antisymmetric iff Intersection with Inverse is Coreflexive

Let $\RR$ be a relation on $S$.
Then:
:$\RR$ is antisymmetric
{{iff}}:
:$\RR \cap \RR^{-1}$ is coreflexive
where $\RR^{-1}$ is the inverse of $\RR$.
That is, {{iff}}:
:$\RR \cap \RR^{-1} \subseteq \Delta_S$

Proof:
=== Necessary Condition ===
Let $\RR$ be an antisymmetric relation.
Let $\tuple {a, b} \in \RR \cap \RR^{-1}$.
That means:
:$\tuple {a, b} \in \RR$
and
:$\tuple {a, b} \in \RR^{-1}$
which means, by definition of inverse relation:
:$\tuple {b, a} \in \RR$
But as $\RR$ is antisymmetric, that means $a = b$.
Thus:
:$\tuple {a, b} = \tuple {a, a}$
and so:
:$\tuple {a, b} \in \Delta_S$
where $\Delta_S$ is the diagonal relation.
Thus from the definition of subset:
:$\RR \cap \RR^{-1} \subseteq \Delta_S$
Hence, by definition, $\RR$ is coreflexive.
{{qed|lemma}}
Theorem: Min Operation on Toset forms Semigroup

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $\map \min {x, y}$ denote the min operation on $x, y \in S$.
Then $\struct {S, \min}$ is a semigroup.

Proof:
By the definition of the min operation, either:
:$\map \min {x, y}= x$
or
:$\map \min {x, y}= y$
So $\min$ is closed on $S$.
From Min Operation is Associative:
:$\forall x, y, z \in S: \map \min {x, \map \min {y, z} } = \map \min {\map \min {x, y}, z}$
Hence the result, by definition of semigroup.
{{qed}}
Theorem: Max Semigroup is Commutative

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

Proof:
Let $x, y \in S$. 
From Max Operation is Commutative:
:$\map \max {x, y} = \map \max {y, x}$ 
Hence the result, by definition of commutative semigroup.
{{qed}}
Theorem: Relation is Connected iff Union with Inverse and Diagonal is Trivial Relation

Let $\RR$ be a relation on $S$.
Then $\RR$ is a connected relation {{iff}}:
:$\RR \cup \RR^{-1} \cup \Delta_S = S \times S$
where $\RR^{-1}$ is the inverse of $\RR$ and $\Delta_S$ is the diagonal relation.

Proof:
=== Necessary Condition ===
Let $\RR$ be a connected relation.
By definition of relation:
:$\RR \subseteq S \times S$
:$\RR^{-1} \subseteq S \times S$
:$\Delta_S \subseteq S \times S$
So from Union is Smallest Superset (and indeed, trivially):
:$\RR \cup \RR^{-1} \cup \Delta_S \subseteq S \times S$
Let $\tuple {a, b} \in S \times S$.
Suppose $a = b$.
Then $\tuple {a, b} \in \Delta_S$ by definition of the diagonal relation.
Then by Set is Subset of Union:
:$\tuple {a, b} \in \RR \cup \RR^{-1} \cup \Delta_S$
Suppose otherwise, that is, that $a \ne b$.
As $\RR$ is connected, either:
:$\tuple {a, b} \in \RR$
or:
:$\tuple {b, a} \in \RR$
From the definition of inverse relation, either:
:$\tuple {a, b} \in \RR$
or:
:$\tuple {a, b} \in \RR^{-1}$
That is:
:$\tuple {a, b} \in R \cup \RR^{-1}$
Again by Set is Subset of Union:
:$\tuple {a, b} \in \RR \cup \RR^{-1} \cup \Delta_S$
So, by definition of subset:
:$S \times S \subseteq \RR \cup \RR^{-1} \cup \Delta_S$
Hence, by definition of set equality:
:$\RR \cup \RR^{-1} \cup \Delta_S = S \times S$
{{qed|lemma}}
Theorem: Triangle Inequality for Generalized Sums

Let $V$ be a Banach space.
Let $\norm {\,\cdot\,}$ denote the norm on $V$.
Let $\family {v_i}_{i \mathop \in I}$ be an indexed subset of $V$.
Let the generalized sum $\ds \sum \set {v_i: i \in I}$ converge absolutely.
Then:
:$(1): \quad \ds \norm {\sum \set {v_i: i \in I} } \le \sum \set {\norm {v_i}: i \in I}$

Proof:
First of all, note that Absolutely Convergent Generalized Sum Converges assures us that the {{LHS}} in $(1)$ is defined.
{{AimForCont}} there exists an $\epsilon > 0$ such that:
:$\ds \norm {\sum \set {v_i: i \in I} } > \sum \set {\norm {v_i}: i \in I} + \epsilon$
This supposition is seen to be equivalent to:
:$\ds \norm {\sum \set {v_i: i \in I} } > \sum \set {\norm {v_i}: i \in I}$
{{explain|Expand below sentence to be more clear}}
Then, by definition of a generalized sum, there necessarily exists a finite subset $F$ of $I$ with:
:$\ds \norm {\sum_{i \mathop \in F} v_i} > \norm {\sum \set {v_i: i \in I} } - \epsilon > \sum \set {\norm {v_i}: i \in I}$
However, using the standard triangle equality on this ''finite'' sum (that is, {{Norm-axiom-mult|3}}, repetitively), we also have:
:$\ds \norm {\sum_{i \mathop \in F} v_i} \le \sum_{i \mathop \in F} \norm {v_i} \le \sum \set {\norm {v_i}: i \in I}$
Here the second inequality follows from Generalized Sum is Monotone.
These two estimates constitute a contradiction, and therefore such an $\epsilon$ cannot exist.
Hence:
:$\ds \norm {\sum \set {v_i: i \in I} } \le \sum \set {\norm {v_i}: i \in I}$
{{qed}}
Category:Generalized Sums
Category:Banach Spaces
Category:Triangle Inequality
ssai2k9x6ao308nf4k6w1y3hg5ag5p6