avewright/proofwiki-math huggingface dataset:
Theorem: Inverse Mapping on Group of Units in Unital Banach Algebra is Continuous

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital Banach algebra.
Let $\map G A$ be the group of units of $A$.
Define $\phi : \map G A \to \map G A$ by: 
:$\map \phi x = x^{-1}$
for each $x \in \map G A$. 
Then $\phi$ is continuous.

Proof:
Let $x \in \map G A$ and $y \in A$ be such that: 
:$\ds \norm {x - y} < \frac 1 {\norm {x^{-1} } }$
As shown in Group of Units in Unital Banach Algebra is Open, we have $y \in \map G A$ and: 
:$\norm {1 - x^{-1} y} < 1$
Then, from Element of Unital Banach Algebra Close to Identity is Invertible, we have: 
:$\ds \norm {\paren {x^{-1} y}^{-1} } = \norm {y^{-1} x} \le \frac 1 {1 - \norm {1 - x^{-1} y} }$
Using the algebra norm property, we have: 
:$\ds \frac 1 {1 - \norm {1 - x^{-1} y} } = \frac 1 {1 - \norm {x^{-1} \paren {x - y} } } \le \frac 1 {1 - \norm {x^{-1} } \norm {x - y} }$
We now have: 
{{begin-eqn}}
{{eqn	| l = \norm {y^{-1} }
		| r = \norm {\paren {x \paren {x^{-1} y} }^{-1} }
}}
{{eqn	| r = \norm {\paren {x^{-1} y}^{-1} x^{-1} }
}}
{{eqn	| o = \le
		| r = \norm {\paren {x^{-1} y}^{-1} } \norm {x^{-1} }
		| c = {{Defof|Algebra Norm}}
}}
{{eqn	| o = \le
		| r = \frac {\norm {x^{-1} } } {1 - \norm {x^{-1} } \norm {x - y} }
}}
{{end-eqn}}
Then we have: 
{{begin-eqn}}
{{eqn	| l = \norm {y^{-1} - x^{-1} }
		| r = \norm {y^{-1} \paren {x - y} x^{-1} }
}}
{{eqn	| o = \le
		| r = \norm {y^{-1} } \norm {x - y} \norm {x^{-1} }
		| c = {{Defof|Algebra Norm}}
}}
{{eqn	| o = \le
		| r = \frac {\norm {x^{-1} }^2 \norm {x - y} } {1 - \norm {x^{-1} } \norm {x - y} }
}}
{{end-eqn}}
Taking $y \to x$, we have $\norm {x - y} \to 0$ and so: 
:$\ds \frac {\norm {x^{-1} }^2 \norm {x - y} } {1 - \norm {x^{-1} } \norm {x - y} } \to 0$
so that: 
:$\norm {y^{-1} - x^{-1} } \to 0$ as $y \to x$. 
So $\phi$ is continuous.
{{qed}}
Category:Unital Banach Algebras
789215e1n93dmfohh9ewtldzppkwflr
Theorem: Existence of Transformations whose Commutator equals Identity

Let $\map {C^\infty} \R$ be the space of smooth real functions.
Let $\circ$ denote the composition of mappings.
Let $A : \map {C^\infty} \R \to \map {C^\infty} \R$ be the mapping such that:
:$\forall \phi \in \map {C^\infty} \R : \forall x \in \R : \map {\paren {A \circ \phi} } x := \map {\dfrac {\d \phi} {\d x} } x$
Let $B : \map {C^\infty} \R \to \map {C^\infty} \R$ be the mapping such that
:$\forall \phi \in \map {C^\infty} \R : \forall x \in \R : \map {\paren {B \circ \phi} } x := x \map \phi x$
Let $I : \map {C^\infty} \R \to \map {C^\infty} \R$ be the identity such that:
:$\forall \phi \in \map {C^\infty} \R : I \circ \phi = \phi$
Then:
:$\forall \Psi \in \map {C^\infty} \R : \paren {A \circ B - B \circ A} \circ \Psi = I \circ \Psi$
or with slight abuse of notation:
:$A \circ B - B \circ A = I$

Proof:
Let $\Psi \in \map {C^\infty} \R$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {A \circ B - B \circ A} \circ \Psi
      | r = \map {\paren {A \circ B} } \Psi - \map {\paren {B \circ A} } \Psi
      | c = Derivative Operator is Linear Mapping
}}
{{eqn | r = \map A {\map B \Psi} - \map B {\map A \Psi}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map A {x \Psi} - \map B {\dfrac \d {\d x} \Psi}
      | c = {{hypothesis}}
}}
{{eqn | r = \dfrac \d {\d x} \paren {x \Psi} - x \dfrac \d {\d x} \Psi
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {\Psi + x \dfrac \d {\d x} \Psi} - x \dfrac \d {\d x} \Psi
      | c = Product Rule for Derivatives
}}
{{eqn | r = \Psi
      | c = simplification
}}
{{eqn | r = I \circ \Psi
      | c = {{Defof|Identity Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 4

:$\forall A \in \AA : \set{V \in \VV : V \cap A \ne \O}$ is finite

Proof:
Let $A \in \AA$.
By definition of refinement:
:$\exists W \in \WW : A \subseteq W$
From Subsets of Disjoint Sets are Disjoint:
:$\forall V \in \VV : V \cap A \ne \O \leadsto V \cap W \ne \O$
Hence:
:$\set{V \in \VV : V \cap A \ne \O} \subseteq \set{V \in \VV : V \cap W \ne \O}$
We have {{hypothesis}}:
:$\set{V \in \VV : V \cap W \ne \O}$ is finite
From Subset of Finite Set is Finite:
:$\set{V \in \VV : V \cap A \ne \O}$ is finite
Since $A$ was arbitrary, it follows that:
:$\forall A \in \AA : \set{V \in \VV : V \cap A \ne \O}$ is finite
{{qed}}
Category:Characterization of Paracompactness in T3 Space
j1b4h0jbfnyb8m377t9jho2y7e5488c
Theorem: Characterization of Paracompactness in T3 Space/Lemma 7

:$\UU^*$ is an open locally finite refinement of $\UU$

Proof:
==== Lemma 5 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 5}}{{qed|lemma}}
Theorem: Norm of Inverse of Sequence of Invertible Elements Converging to Non-Invertible Element in Unital Banach Algebra

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital Banach algebra.
Let $\map G A$ be the group of units of $A$.
Let $x \in A \setminus \map G A$. 
Let $\sequence {x_n}_{n \in \N}$ be a sequence in $\map G A$ such that $x_n \to x$. 
Then $\norm {x_n^{-1} } \to \infty$ as $n \to \infty$.

Proof:
Note that if there existed $n \in \N$ such that: 
:$\ds \norm {x - x_n} < \frac 1 {\norm {x_n^{-1} } }$
then we would have $x \in \map G A$ from Group of Units in Unital Banach Algebra is Open. 
So, we have: 
:$\ds \frac 1 {\norm {x_n^{-1} } } \le \norm {x - x_n}$ for each $n \in \N$. 
Since we have $x_n \to x$, we have $\norm {x - x_n} \to 0$, and hence: 
:$\ds \frac 1 {\norm {x_n^{-1} } } \to 0$ as $n \to \infty$.
So:
:$\norm {x_n^{-1} } \to \infty$ as $n \to \infty$.
{{qed}}
Category:Unital Banach Algebras
fi129hvbf7ijohab33tencipk8pl96l
Theorem: Element of Unital Banach Algebra on Boundary of Group of Units of Subalgebra is Not Invertible in Algebra

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital Banach algebra.
Let $\map G A$ be the group of units of $A$.
Let $B$ be a closed subalgebra of $A$.
Let $\map G B$ be the group of units of $A$.
Let $x \in \partial \map G B$, where $\partial \map G B$ is the topological boundary of $\map G B$.
Then $x$ is not invertible in $A$.

Proof:
=== Lemma ===
{{:Element of Unital Banach Algebra on Boundary of Group of Units of Subalgebra is Not Invertible in Algebra/Lemma}}{{qed|lemma}}
{{AimForCont}} that there exists $y \in A$ such that $x y = 1$.
From the lemma, there exists a sequence $\sequence {z_n}_{n \in \N}$ in $A$ such that $\norm {z_n} = 1$ for each $n \in \N$, and: 
:$z_n x \to 0$ as $n \to \infty$
From Product Rule for Sequence in Normed Algebra, we have: 
:$z_n x y \to 0$ as $n \to \infty$.
Since $x y = 1$, this gives $z_n \to 0$ as $n \to \infty$. 
From Modulus of Limit: Normed Vector Space, we then have $\norm {z_n} \to 0$ as $n \to \infty$. 
But $\norm {z_n} = 1$ for each $n \in \N$, so this is impossible.
So we have a contradiction and there exists no such $y \in A$.
{{qed}}
Category:Element of Unital Banach Algebra on Boundary of Group of Units of Subalgebra is Not Invertible in Algebra
Category:Unital Banach Algebras
770e0poygpu7yfcm67vy3wf8gsvlc3y
Theorem: Fréchet Filter is Filter

Let $S$ be an infinite set.
Let $\FF$ be the Fréchet filter on $S$.
Then $\FF$ is a filter on $S$.

Proof:
By definition, $\FF$ must satisfy the filter on set axioms:
{{:Axiom:Filter on Set Axioms/Axioms 1}}
Theorem: Existence of Nonprincipal Ultrafilter

Let $S$ be an infinite set.
Then there exists an nonprincipal ultrafilter $U$ on $S$.

Proof:
Let $\FF$ be the Fréchet filter on $S$.
By Fréchet Filter is Filter, $\FF$ is a filter on $S$.
Then, by the Ultrafilter Lemma, there exists some ultrafilter $\UU \supseteq \FF$ on $S$.
The result follows by Ultrafilter is Nonprincipal iff Contains Fréchet Filter.
{{qed}}
{{BPI|Ultrafilter Lemma}}
Category:Nonprincipal Ultrafilters
i7a7a49nhpajz8eo6sekboi7z5c83gg
Theorem: Initial Topology Generated by Countable Family of Functions Separating Points is Metrizable

Let $X$ be a set. 
For each $n \in \N$, let $\struct {Y_n, d_n}$ be a metric space. 
Let $\family {f_n}_{n \in \N}$ be a indexed family of functions $X \to Y_n$ that separates points.
Let $\tau$ be the initial topology on $X$ generated by $\family {f_n}_{n \in \N}$.
Then $\tau$ is metrizable.

Proof:
For each $x, y \in X$, define: 
:$\map {\tilde {d_n} } {x, y} = \min \set {\map {d_n} {\map {f_n} x, \map {f_n} y}, 1}$
From Pointwise Minimum of Metric and Positive Real Number is Topologically Equivalent Metric, $\tilde {d_n}$ is a metric that is topologically equivalent to $d_n$. 
Now define, for each $x, y \in X$:
:$\ds \map d {x, y} = \sum_{n \mathop = 1}^\infty \frac {\map {\tilde {d_n} } {x, y} } {2^n}$
This is certainly finite, since: 
:$\ds \sum_{n \mathop = 1}^\infty \frac {\map {\tilde {d_n} } {x, y} } {2^n} \le 1$
from Sum of Infinite Geometric Sequence and since $\tilde {d_n} \le 1$. 
We show that $d$ is a metric on $X$.
Theorem: Nondeterministic Turing Machine is Equivalent to Deterministic Turing Machine

A nondeterministic turing machines and a deterministic turing machines are equivalent.
{{explain|what is meant by "equivalent"}}

Proof:
=== Every Deterministic Turing Machine can be run by a Nondeterministic Turing Machine ===
The machine definitions only differ in whether $\tuple {q', Y', d } \in \map \delta {q, Y}$ or $\tuple {q', Y', d} = \map \delta {q, Y}$.
Define singletons $\map \delta {q, Y} = \set {\tuple {q', Y', d} }$ from the deterministic mapping and run your DTM on your NTM.
Theorem: Characterization of Paracompactness in T3 Space/Lemma 12

:$\forall A \in \AA : \set{U^* \in \UU^* : U^* \cap A \ne \O}$ is finite

Proof:
===== Lemma 4 =====
{{:Characterization of Paracompactness in T3 Space/Lemma 4}}{{qed|lemma}}
Theorem: Sequence of Smallest 3 Consecutive Triangular Numbers which are Sphenic

The smallest $3$ consecutive triangular numbers which are sphenic is:
:$406$, $435$, $465$

Proof:
Let $T_n$ denote the $n$th triangular number.
The smallest sphenic number is $30$.
Hence we need investigate triangular number from where $T_n \ge 30$.
Thus:
{{begin-eqn}}
{{eqn | l = T_8
      | r = 36
      | rr= = 2^2 \times 3^2
      | c = which is not sphenic
}}
{{eqn | l = T_9
      | r = 45
      | rr= = 3^2 \times 5
      | c = which is not sphenic
}}
{{eqn | l = T_{10}
      | r = 55
      | rr= = 5 \times 11
      | c = which is not sphenic
}}
{{eqn | l = T_{11}
      | r = 66
      | rr= = 2 \times 3 \times 11
      | c = which is sphenic
}}
{{eqn | l = T_{12}
      | r = 78
      | rr= = 2 \times 3 \times 13
      | c = which is sphenic
}}
{{eqn | l = T_{13}
      | r = 91
      | rr= = 7 \times 13
      | c = which is not sphenic
}}
{{eqn | l = T_{14}
      | r = 105
      | rr= = 3 \times 5 \times 7
      | c = which is sphenic
}}
{{eqn | l = T_{15}
      | r = 120
      | rr= = 2^2 \times 3 \times 5
      | c = which is not sphenic
}}
{{eqn | l = T_{16}
      | r = 135
      | rr= = 2^3 \times 17
      | c = which is not sphenic
}}
{{eqn | l = T_{17}
      | r = 153
      | rr= = 3^2 \times 17
      | c = which is not sphenic
}}
{{eqn | l = T_{18}
      | r = 171
      | rr= = 3^2 \times 19
      | c = which is not sphenic
}}
{{eqn | l = T_{19}
      | r = 190
      | rr= = 2 \times 5 \times 19
      | c = which is sphenic
}}
{{eqn | l = T_{20}
      | r = 210
      | rr= = 2 \times 3 \times 5 \times 7
      | c = which is not sphenic
}}
{{eqn | l = T_{21}
      | r = 231
      | rr= = 3 \times 7 \times 11
      | c = which is sphenic
}}
{{eqn | l = T_{22}
      | r = 253
      | rr= = 11 \times 23
      | c = which is not sphenic
}}
{{eqn | l = T_{23}
      | r = 276
      | rr= = 2^2 \times 3 \times 23
      | c = which is not sphenic
}}
{{eqn | l = T_{24}
      | r = 300
      | rr= = 2^2 \times 3 \times 5^2
      | c = which is not sphenic
}}
{{eqn | l = T_{25}
      | r = 325
      | rr= = 5^2 \times 13
      | c = which is not sphenic
}}
{{eqn | l = T_{26}
      | r = 351
      | rr= = 3^3 \times 13
      | c = which is not sphenic
}}
{{eqn | l = T_{27}
      | r = 351
      | rr= = 2 \times 3^3 \times 7
      | c = which is not sphenic
}}
{{eqn | l = T_{28}
      | r = 406
      | rr= = 2 \times 7 \times 29
      | c = which is sphenic
}}
{{eqn | l = T_{29}
      | r = 435
      | rr= = 3 \times 5 \times 29
      | c = which is sphenic
}}
{{eqn | l = T_{30}
      | r = 465
      | rr= = 3 \times 5 \times 31
      | c = which is sphenic
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 8

:there exists a $\sigma$-discrete refinement $\AA$ of $\UU$

Proof:
Let $\tau_{X \times X}$ denote the product topology on the cartesian product $X \times X$.
By definition of even cover there exists a neighborhood $V$ of the diagonal $\Delta_X$ of $X \times X$ in the product space $\struct {X \times X, \tau_{X \times X} }$:
:$\set{\map V x : x \in X}$ is a refinement of $\UU$
where:
:$V$ is seen as a relation on $X \times X$
:$\map V x$ denotes the image of $x$ under $V$.
In what follows subsets of $X \times X$ will be treated at times as a relation on $X \times X$.
Theorem: Union is Empty iff Sets are Empty/Set of Sets

Let $\SS$ be a set of sets.
Then:
:$\ds \bigcup \SS = \O \iff \forall S \in \SS: S = \O$

Proof:
{{begin-eqn}}
{{eqn | r = \bigcup \SS = \O
      | o = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \neg \exists x
      | r = x \in \paren {\bigcup \SS}
      | c = {{Defof|Empty Set}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall x
      | r = \neg \paren {x \in \bigcup \SS }
      | c = De Morgan's Laws (Predicate Logic)
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall x
      | r = \neg \paren {\exists S \in \SS : x \in S}
      | c = {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall x, \forall S \in \SS
      | r = x \notin S
      | c = De Morgan's Laws: Assertion of Universality
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | q = \forall S \in \SS 
      | r = S = \O
      | c = {{Defof|Empty Set}}
}}
{{end-eqn}}
{{qed}}
Category:Union is Empty iff Sets are Empty
l590pgsvw082jtgons9w42ftd3d8ne7
Theorem: Union of Set of Sets is Non-empty iff some Set is Non-empty

Let $\SS$ be a set of sets.
Then:
:$\ds \bigcup \SS \ne \O \iff \exists S \in \SS: S \ne \O$

Proof:
Follows immediately from Union of Set of Sets is Empty iff Sets are Empty.
{{qed}}
Category:Set Union
Category:Empty Set
d7pgvuvtxh20cuxq475qz4ipp5fv37w
Theorem: Hölder Mean for Exponent 1 is Arithmetic Mean

Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be real numbers.
For $p \in \R_{\ne 0}$, let $\map {M_p} {x_1, x_2, \ldots, x_n}$ denote the '''Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$'''.
Then:
:$\map {M_1} {x_1, x_2, \ldots, x_n} = \dfrac {x_1 + x_2 + \cdots + x_n} n$
which is the arithmetic mean of $x_1, x_2, \ldots, x_n$.

Proof:
Recall the definition of the '''Hölder mean with exponent $p$''':
:$\ds \map {M_p} {x_1, x_2, \ldots, x_n} = \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^p}^{1 / p}$
Then:
{{begin-eqn}}
{{eqn | l = \map {M_1} {x_1, x_2, \ldots, x_n}
      | r = \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^1}^{1 / 1}
      | c = 
}}
{{eqn | r = \frac 1 n \sum_{k \mathop = 1}^n {x_k}
      | c = simplifying
}}
{{end-eqn}}
which is the arithmetic mean by definition.
{{qed}}
Theorem: Hölder Mean for Exponent -1 is Harmonic Mean

Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be real numbers.
For $p \in \R_{\ne 0}$, let $\map {M_p} {x_1, x_2, \ldots, x_n}$ denote the '''Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$'''.
Then:
:$\map {M_{-1} } {x_1, x_2, \ldots, x_n} = \dfrac 1 {\dfrac 1 n \paren {\dfrac 1 {x_1} + \dfrac 1 {x_2} + \cdots + \dfrac 1 {x_n} } }$
which is the harmonic mean of $x_1, x_2, \ldots, x_n$.

Proof:
Recall the definition of the '''Hölder mean with exponent $p$''':
:$\ds \map {M_p} {x_1, x_2, \ldots, x_n} = \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^p}^{1 / p}$
Then:
{{begin-eqn}}
{{eqn | l = \map {M_{-1} } {x_1, x_2, \ldots, x_n}
      | r = \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^{-1} }^{1 / -1}
      | c = 
}}
{{eqn | r = \paren {\frac 1 n \sum_{k \mathop = 1}^n {\dfrac 1 {x_k} } }^{-1}
      | c = simplifying
}}
{{eqn | r = \dfrac 1 {\ds \frac 1 n \sum_{k \mathop = 1}^n {\dfrac 1 {x_k} } }
      | c = simplifying
}}
{{end-eqn}}
which is the harmonic mean by definition.
{{qed}}
Theorem: Limit of Hölder Mean as Exponent tends to Infinity

Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be real numbers.
For $p \in \R_{\ne 0}$, let $\map {M_p} {x_1, x_2, \ldots, x_n}$ denote the '''Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$'''.
Then:
:$\ds \lim_{p \mathop \to +\infty} \map {M_p} {x_1, x_2, \ldots, x_n} = \max \set {x_1, x_2, \ldots, x_n}$

Proof:
Let $p \in \R$ such that $p \ne 0$.
Let it be assumed (or arranged) that:
:$x_1 \ge x_2 \ge \cdots \ge x_n$
Then:
{{begin-eqn}}
{{eqn | l = \lim_{p \mathop \to +\infty} \map {M_p} {x_1, x_2, \ldots, x_n}
      | r = \lim_{p \mathop \to +\infty} \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_k}^p}^{1 / p}
      | c = 
}}
{{eqn | r = \lim_{p \mathop \to +\infty} \paren {\frac 1 n \sum_{k \mathop = 1}^n {x_1}^p \paren {\dfrac {x_k} {x_1} }^p}^{1 / p}
      | c = 
}}
{{eqn | r = \lim_{p \mathop \to +\infty} x_1 \paren {\frac 1 n \sum_{k \mathop = 1}^n \paren {\dfrac {x_k} {x_1} }^p}^{1 / p}
      | c = taking $p$th root of ${x_1}^p$ and moving it outside the parenthesis
}}
{{eqn | r = x_1 \lim_{p \mathop \to +\infty} \paren {\frac 1 n \sum_{k \mathop = 1}^n \paren {\dfrac {x_k} {x_1} }^p}^{1 / p}
      | c = Multiple Rule for Limits of Real Functions
}}
{{eqn | r = x_1
      | c = {{explain|Somehow we equate $\ds \lim_{p \mathop \to +\infty} \paren {\frac 1 n \sum_{k \mathop {{=}} 1}^n \paren {\dfrac {x_k} {x_1} }^p}^{1 / p}$ to $1$, not sure how this is justified}}
}}
{{eqn | r = \max \set {x_1, x_2, \ldots, x_n}
      | c = {{hypothesis}}: $x_1 \ge x_2 \ge \cdots \ge x_n$
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Hölder Mean as Exponent tends to Negative Infinity

Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be real numbers.
For $p \in \R_{\ne 0}$, let $\map {M_p} {x_1, x_2, \ldots, x_n}$ denote the '''Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$'''.
Then:
:$\ds \lim_{p \mathop \to -\infty} \map {M_p} {x_1, x_2, \ldots, x_n} = \min \set {x_1, x_2, \ldots, x_n}$

Proof:
Let $p \in \R$ such that $p \ne 0$.
Let it be assumed (or arranged) that:
:$x_1 \ge x_2 \ge \cdots \ge x_n$
Then:
{{begin-eqn}}
{{eqn | l = \lim_{p \mathop \to -\infty} \map {M_p} {x_1, x_2, \ldots, x_n}
      | r = \dfrac 1 {\ds \lim_{p \mathop \to +\infty} \map {M_p} {\dfrac 1 {x_1}, \dfrac 1 {x_2}, \ldots, \dfrac 1 {x_n} } }
      | c = {{explain|Justify this step}}
}}
{{eqn | r = \dfrac 1 {\paren {\dfrac 1 {x_n} } }
      | c = Limit of Hölder Mean as Exponent tends to Infinity
}}
{{eqn | r = x_n
      | c = 
}}
{{eqn | r = \min \set {x_1, x_2, \ldots, x_n}
      | c = {{hypothesis}}: $x_1 \ge x_2 \ge \cdots \ge x_n$
}}
{{end-eqn}}
{{qed}}
Theorem: Minimum is Less than or Equal to Geometric Mean

:$\min \set {x_1, x_2, \ldots, x_n} \le \map G {x_1, x_2, \ldots, x_n}$
Equality holds {{iff}}:
:$x_1 = x_2 = \cdots x_n$
or $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.

Proof:
From Limit of Hölder Mean as Exponent tends to Zero is Geometric Mean:
:$\map G {x_1, x_2, \ldots, x_n} = \ds \lim_{p \mathop \to 0} \map {M_p} {x_1, x_2, \ldots, x_n}$
where $\map {M_p} {x_1, x_2, \ldots, x_n}$ denotes the Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$.
Then from Minimum is Less than or Equal to Hölder Mean:
$\min \set {x_1, x_2, \ldots, x_n} \le \map {M_p} {x_1, x_2, \ldots, x_n}$
where equality holds {{iff}}:
:$x_1 = x_2 = \cdots x_n$
or:
:$p < 0$ and $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.
In this context, if such an $x_k = 0$ then:
:$\ds \prod_{k \mathop = 1}^n x_k = 0$
and so by definition:
$\map G {x_1, x_2, \ldots, x_n} = 0$
Thus we have:
:$\min \set {x_1, x_2, \ldots, x_n} \le \map G {x_1, x_2, \ldots, x_n}$
{{qed}}
Theorem: Maximum is Greater than or Equal to Geometric Mean

:$\max \set {x_1, x_2, \ldots, x_n} \ge \map G {x_1, x_2, \ldots, x_n}$
Equality holds {{iff}}:
:$x_1 = x_2 = \cdots x_n$
or $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.

Proof:
From Limit of Hölder Mean as Exponent tends to Zero is Geometric Mean:
:$\map G {x_1, x_2, \ldots, x_n} = \ds \lim_{p \mathop \to 0} \map {M_p} {x_1, x_2, \ldots, x_n}$
where $\map {M_p} {x_1, x_2, \ldots, x_n}$ denotes the Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$.
Then from Maximum is Greater than or Equal to Hölder Mean:
$\max \set {x_1, x_2, \ldots, x_n} \ge \map {M_p} {x_1, x_2, \ldots, x_n}$
where equality holds {{iff}}:
:$x_1 = x_2 = \cdots x_n$
or:
:$p < 0$ and $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.
In this context, if such an $x_k = 0$ then:
:$\ds \prod_{k \mathop = 1}^n x_k = 0$
and so by definition:
$\map G {x_1, x_2, \ldots, x_n} = 0$
Thus we have:
:$\max \set {x_1, x_2, \ldots, x_n} \ge \map G {x_1, x_2, \ldots, x_n}$
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 20

Let $N$ be a neighborhood of the diagonal $\Delta_X$ of $X \times X$ in the product space $\struct {X \times X, \tau_{X \times X} }$.
Then there exists an open neighborhood $W$ of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} }$:
:$W$ is symmetric as a relation on $X \times X$, that is, $W = W^{-1}$
:the composite relation $W \circ W$ is a subset of $N$, that is, $W \circ W \subseteq N$

Proof:
Let:
:$\VV = \set{V \in \tau : V \times V \subseteq N}$
From Neighborhood of Diagonal induces Open Cover:
:$\VV$ is an open cover of $T$
We have {{hypothesis}}, $\VV$ is even.
From Characterization of Even Cover, there exists an open neighborhood $R$ of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} }$:
:$\set{\map R x : x \in S}$ is a refinement of $\VV$
where:
:$R$ is seen as a relation on $X \times X$
:$\map R x$ denotes the image of $x$ under $R$.
By definition of refinement of cover:
:$\forall x \in X : \exists V \in \VV : \map R x \subseteq V$
From Cartesian Product of Subsets:
:$\forall x \in X : \exists V \in \VV : \map R x \times \map R x \subseteq V \times V$
From Subset Relation is Transitive:
:$\forall x \in X : \map R x \times \map R x \subseteq N$
Let $W = R \cap R^{-1}$, where $R^{-1}$ is the inverse relation of $R$ on $X \times X$.
From Inverse of Open Set in Product Space is Open in Inverse Product Space:
:$R^{-1}$ is open in $\struct {X \times X, \tau_{X \times X}}$
By {{Open-set-axiom|2}}:
:$W$ is open in $\struct {X \times X, \tau_{X \times X}}$
From Inverse of Reflexive Relation is Reflexive:
:$R^{-1}$ is reflexive
From Intersection of Reflexive Relations is Reflexive:
:$W$ is reflexive
By definition of reflexive:
:$W$ is an open neighborhood of the diagonal $\Delta_X$.
From Intersection of Relation with Inverse is Symmetric Relation:
:$W$ is a symmetric relation on $X \times X$
We have:
{{begin-eqn}}
{{eqn | q = \forall x, y, z \in X 
      | l = \tuple{y,z} \in \map W x \times \map W x
      | o = \leadsto
      | r = y, z \in \map W x
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadsto
      | r = \tuple{x, y}, \tuple{x, z} \in W
      | c = {{Defof|Image of Element under Relation}}
}}
{{eqn | o = \leadsto
      | r = \tuple{x, y}, \tuple{x, z} \in R
      | c = Intersection is Subset and {{Defof|Subset}}
}}
{{eqn | o = \leadsto
      | r = y, z \in \map R x
      | c = {{Defof|Image of Element under Relation}}
}}
{{eqn | o = \leadsto
      | r = \tuple{y, z} \in \map R x \times \map R x
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadsto
      | r = \tuple{y, z} \in N
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
By definition of subset:
:$\forall x \in X : \map W x \times \map W x \subseteq N$
From Composition of Symmetric Relation with Itself is Union of Products of Images:
:$W \circ W = \ds \bigcup_{x \in X} \map W x \times \map W x$
From Union of Subsets is Subset:
:$W \circ W \subseteq N$
{{qed}}