avewright/proofwiki-math huggingface dataset:
Theorem: Weak Closure of Unit Sphere is Closed Unit Ball

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be an infinite-dimensional normed vector space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\cl_w$ be the topological closure in $\struct {X, w}$. 
Let:
:$S_X^- = \set {x \in X : \norm x_X = 1}$
Let $B_X^-$ be the closed unit ball of $\struct {X, \norm {\, \cdot \,} }$.
Then $\map {\cl_w} {S_X} = B_X^-$.

Proof:
We firstly show that $\map {\cl_w} {S_X^-} \subseteq B_X^-$. 
We have $S_X^- \subseteq B_X^-$.
From Mazur's Theorem: Corollary, $B_X^-$ is $w$-closed.
Hence from Set is Closed iff Equals Topological Closure, we have that $\map {\cl_w} {B_X^-} = B_X^-$.
From Topological Closure of Subset is Subset of Topological Closure, we then have $\map {\cl_w} {S_X^-} \subseteq B_X^-$.
We now need to show that $B_X^- \subseteq \map {\cl_w} {S_X}$.
We have $S_X \subseteq \map {\cl_w} {S_X}$.
Let $x \in B_X^- \setminus S_X$.
We show that every open neighborhood $U$ of $x$ in $\struct {X, w}$ intersects $S_X$.
Let $U$ be an open neighborhood of $x$ in $\struct {X, w}$. 
From Translation of Open Set in Topological Vector Space is Open, $U - x$ is an open neighborhood of ${\mathbf 0}_X$ in $\struct {X, w}$. 
From Weakly Open Neighborhood of Zero Vector in Infinite-Dimensional Topological Vector Space contains Infinite-Dimensional Vector Subspace, $U - x$ contains a non-zero vector subspace $V$.
Then $x + V \subseteq U$.
We show that $\paren {x + V} \cap S_X \ne \O$ so that $U \cap S_X \ne \O$.
Let $y \in V \setminus \set { {\mathbf 0}_X}$. 
We define $\phi : \hointl 0 \infty \to \R$ by:
:$\map \phi t = \norm {x + t y}_X$
We then have:
{{begin-eqn}}
{{eqn	| l = \cmod {\map \phi t - \map \phi s}
		| r = \cmod {\norm {x + t y}_X - \norm {x + s y}_X}
}}
{{eqn	| o = \le
		| r = \norm {t y - s y}_X
		| c = Reverse Triangle Inequality: Normed Vector Space
}}
{{eqn	| r = \norm {\paren {t - s} y}_X
}}
{{eqn	| r = \cmod {t - s} \norm y_X
		| c = {{NormAxiomVector|1}}
}}
{{end-eqn}}
Hence $\phi$ is Lipschitz.
From Lipschitz Condition implies Uniform Continuity, $\phi$ is continuous.
We have $\map \phi 0 = \norm x_X < 1$.
Note that for:
:$\ds t_0 = \frac {1 + \norm x_X} {\norm y_X} > 0$
we have:
{{begin-eqn}}
{{eqn	| l = \map \phi {t_0}
		| r = \norm {x + t_0 y}_X
}}
{{eqn	| o = \ge
		| r = \norm {t_0 y}_X - \norm x_X
		| c = reverse triangle inequality
}}
{{eqn	| r = t_0 \norm y_X - \norm x_X
		| c = {{NormAxiomVector|1}}
}}
{{eqn	| r = 1 + \norm x_X - \norm x_X
}}
{{eqn	| r = 1
}}
{{end-eqn}}
Hence by the Intermediate Value Theorem, there exists $0 < t^\ast \le t_0$ such that $\map \phi {t^\ast} = 1$, so that $\norm {x + t^\ast y}_X = 1$.
We have $x + t^\ast y \in x + V \subseteq U$ and $x + t^\ast y \in S_X$.
Hence $U \cap S_X \ne \O$.
Since $U$ was an arbitrary open neighborhood of $x$, we have $x \in \map {\cl_w} {S_X}$.
Hence we have $B_X^- \subseteq \map {\cl_w} {S_X}$.
We conclude that $\map {\cl_w} {S_X} = B_X^-$.
{{qed}}
Theorem: Dimension of Direct Product of Vector Spaces

Let $K$ be a field.
Let $X_1, X_2, \ldots, X_n$ be vector spaces over $K$.
Let:
:$\ds X = \prod_{j \mathop = 1}^n X_j$ be the direct product of $X_1, \ldots, X_n$.
Then:
:$\ds \dim X = \sum_{j \mathop = 1}^n \map \dim {X_j}$

Proof:
For each $1 \le j \le n$, let $\BB_j = \sequence {e_{j, i} }_{i \mathop \in I_j}$ be a basis of $X_j$ where $I_j$ is an index set.
{{WLOG}} suppose that the $I_j$ are disjoint.
For each $1 \le j \le n$ and $i \in I_j$, define $\pi : \set {1, \ldots, n} \to X$ by:
:$\map {\pi_{j, i} } k = \begin{cases}{\mathbf 0}_{X_j} & j \ne k \\ e_{j, i} & j = k\end{cases}$
We show that $\sequence {\pi_{j, i} }_{1 \le j \le n, \, i \in I_j}$ spans $X$.
Let $x = \tuple {\map x 1, \ldots, \map x n} \in X$ where $\map x j \in X_j$.
For each $1 \le j \le n$, we can find $\lambda_{j, 1}, \ldots, \lambda_{j, N_j}$ and $e_{j, i_1}, \ldots, e_{j, i_{j, N_j} } \in X_j$ such that:
:$\ds \map x j = \sum_{s \mathop = 1}^{N_j} \lambda_{j, s} e_{j, i_{j, s} }$
We then have:
:$\ds x = \sum_{j \mathop = 1}^n \sum_{s \mathop = 1}^{N_j} \lambda_{j, s} \pi_{j, i_{j, s} }$
We now need to show that $\sequence {\pi_{j, i} }_{1 \le j \le n, \, i \in I_j}$ is linearly independent.
With the same notation as above, suppose that:
:$\ds \sum_{j \mathop = 1}^n \sum_{s \mathop = 1}^{N_j} \lambda_{j, s} \pi_{j, i_{j, s} } = {\mathbf 0}_X$
Evaluating at $k$ with $1 \le k \le n$, we have that:
:$\ds \sum_{s \mathop = 1}^{N_k} \lambda_{k, s} e_{k, i_{j, s} } = {\mathbf 0}_{X_k}$
Since $\BB_k$ is linearly independent, we have $\lambda_{k, i_{k, s} } = {\mathbf 0}_K$ for $1 \le s \le N_k$.
This holds of all $k$, so we have $\lambda_{j, i_{j, s} } = {\mathbf 0}_K$ for all $1 \le j \le n$ and $1 \le s \le N_j$. 
Hence $\sequence {\pi_{j, i} }_{1 \le j \le n, \, i \in I_j}$ is linearly independent. 
Hence:
:$\ds \map \dim X = \sum_{j \mathop = 1}^n \size {I_j} = \sum_{j \mathop = 1}^n \map \dim {X_j}$
{{qed}}
Category:Direct Product of Vector Spaces
3p749j1t4c1v7ucfzz2rdxwayo5lzyo
Theorem: Frame Spectrum Functor is Contravariant Functor

Let $\mathbf{Frm}$ denote the category of frames.
Let $\mathbf{Top}$ denote the category of topological spaces.
Then:
:the frame spectrum functor $\mathbf {\operatorname {Sp}} : \mathbf{Frm} \to \mathbf{Top}$ is a contravariant functor

Proof:
=== Object Functor is Well-Defined ===
From Spectrum of Locale as Completely Prime Filters is Sober Space:
:for each frame $L$ in $\mathbf {Frm}$, considered as a locale, $\map {\mathbf {\operatorname {Sp} } } L$ is a topological space
It follows that the object functor $\mathbf {\operatorname {Sp}}_0$ is well-defined.
{{qed|lemma}}
Theorem: Characterization of Codimension in terms of Direct Sum

Let $K$ be a field.
Let $X$ be a vector space such that $X \ne {\mathbf 0}_X$.
Let $U \subseteq X$ be a vector subspace of $X$.
Let $0 < \kappa \le \dim X$ be a cardinal number.
Then $U$ has codimension $\kappa$ {{iff}} there exists a subspace $V$ of dimension $\kappa$ such that:
:$X = U \oplus V$
where $\oplus$ denotes the internal direct sum.

Proof:
=== Sufficient Condition ===
Suppose that $U$ has codimension $\kappa$.
Let $X/U$ be the quotient vector space of $X$ modulo $U$.
Since $U$ has codimension $\kappa$, we have $\map \dim {X/U} = \kappa$. 
Let $q : X \to X/U$ be the quotient mapping.
Let $\BB_1 = \set {u_\alpha : \alpha \in I}$ be a basis for $U$, where $I_1$ is an index set with cardinality $\dim U$.
Let $\widetilde {\BB_2} = \set {\map q {z_\beta} : \beta \in \kappa}$ be a basis for $\map \dim {X/U}$.
Let $\BB_2 = \set {z_\beta : \beta \in \kappa}$.
As shown in Construction of Basis for Vector Space from Basis for Vector Subspace and Basis of Quotient, $\BB_2$ is a linearly independent set.
Let $V = \map \span {\BB_2}$.
From Linear Span is Linear Subspace, $V$ is a vector subspace of $X$ with dimension $\kappa$. 
It is also shown in Construction of Basis for Vector Space from Basis for Vector Subspace and Basis of Quotient that $\BB_1 \cup \BB_2$ is linearly independent and hence $U \cap V = \set { {\mathbf 0}_X}$.
Finally, in Construction of Basis for Vector Space from Basis for Vector Subspace and Basis of Quotient it is shown that $\BB_1 \cup \BB_2$ is a basis for $X$.
Hence we have $X = U \oplus V$. 
{{qed|lemma}}
Theorem: Kernel of Non-Zero Linear Functional has Codimension 1

Let $K$ be a field.
Let $X$ be a vector space over $K$.
Let $f : X \to K$ be a non-zero linear functional 
Let $\ker f$ be the kernel of $f$.
Then $\ker f$ has codimension $1$.

Proof:
Let $X/\ker f$ be the quotient vector space of $X$ modulo $\ker f$.
Let $q : X \to X/\ker f$ be the quotient mapping.
From Condition for Mapping from Quotient Vector Space to be Well-Defined, there exists a linear functional $\widetilde f : X/\ker f \to K$ such that:
:$f = \widetilde f \circ q$
Note that if $\map {\widetilde f} {\map q x} = {\mathbf 0}_K$, then we have $\map f x = {\mathbf 0}_K$, hence $x \in \ker f$.
From Kernel of Quotient Mapping, we have $\map q x = {\mathbf 0}_{X/\ker f}$.
Hence $\widetilde f$ is injective.
Since $\widetilde f \ne {\mathbf 0}_X$, we have that $\widetilde f$ is surjective from Linear Functional on Vector Space is Zero or Surjective.
From Dimension of Image of Vector Space under Linear Transformation is Bounded Above by Dimension of Vector Space: Corollary, we have:
:$\map \dim {X/\ker f} = \dim \widetilde f \sqbrk {X/\ker f} = \dim K = 1$
Hence $\ker f$ has codimension $1$.
{{qed}}
Category:Codimensions of Vector Subspaces
t9wx8ah62x72ju160wevpjnx2qlw3a0
Theorem: Codimension of Intersection of Finitely Many Vector Subspaces is Bounded Above by Sum of Codimensions

Let $K$ be a field.
Let $X$ be a vector space over $K$.
Let $U_1, U_2, \ldots, U_n$ be vector subspaces of $X$.
Let:
:$\ds U = \bigcap_{j \mathop = 1}^n U_j$
Then:
:$\ds \map {\operatorname {codim} } U \le \sum_{j \mathop = 1}^n \map {\operatorname {codim} } {U_j}$
where $\ds \sum_{j \mathop = 1}^n$ denotes the cardinal sum.

Proof:
Define the direct product:
:$\ds Y = \prod_{j \mathop = 1}^n \paren {X/U_j}$
For each $1 \le j \le n$, let $q_j : X \to X/U_j$ be the quotient mapping.
Define the linear transformation $T : X \to Y$ by:
:$T x = \tuple {\map {q_1} x, \ldots, \map {q_n} x}$ for each $x \in X$.
We have that:
:$\ds \bigcap_{j \mathop = 1}^n \ker q_j \subseteq \ker T$
From Kernel of Quotient Mapping, we have:
:$\ds \bigcap_{j \mathop = 1}^n U_j \subseteq \ker T$
From Condition for Mapping from Quotient Vector Space to be Well-Defined, there exists a linear transformation $\widetilde T : X/U \to Y$ such that:
:$T = \widetilde T \circ q$
We further establish that $\widetilde T$ is injective.
We have $\map {\widetilde T} {\map q x} = {\mathbf 0}_Y$ {{iff}} $T x = {\mathbf 0}_Y$ {{iff}} $x \in \ker T$.
That is, from Kernel of Quotient Mapping, {{iff}} $\map q x = {\mathbf 0}_{X/Y}$.
Hence $\widetilde T$ is injective.
We then have:
{{begin-eqn}}
{{eqn	| l = \dim X/U
		| r = \dim \widetilde T \sqbrk {X/U}
		| c = Dimension of Image of Vector Space under Linear Transformation is Bounded Above by Dimension of Vector Space: Corollary
}}
{{eqn	| o = \le
		| r = \dim Y
		| c = Dimension of Vector Subspace
}}
{{eqn	| r = \map \dim {\prod_{j \mathop = 1}^n X/U_j}
}}
{{eqn	| o = \le
		| r = \sum_{j \mathop = 1}^n \map \dim {X/U_j}
		| c = Dimension of Direct Product of Vector Spaces
}}
{{eqn	| r = \sum_{j \mathop = 1}^n \map {\operatorname {codim} } {U_j}
}}
{{end-eqn}}
We conclude:
:$\ds \map {\operatorname {codim} } U \le \sum_{j \mathop = 1}^n \map {\operatorname {codim} } {U_j}$
{{qed}}
Category:Codimensions of Vector Subspaces
an5uq2dkph5qh30n5g78ao898z5x1u4
Theorem: Weakly Open Neighborhood of Zero Vector in Infinite-Dimensional Topological Vector Space contains Infinite-Dimensional Vector Subspace

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be an infinite-dimensional topological vector space over $\GF$.
Let $w$ be the weak topology of $\struct {X, \tau}$.
Let $U$ be an open neighborhood of ${\mathbf 0}_X$ in $\struct {X, w}$. 
Then $U$ contains an infinite-dimensional vector subspace.
In particular, $U$ contains a vector subspace of finite codimension.

Proof:
Let $X^\ast$ be the topological dual space of $X$.
From Open Sets in Weak Topology of Topological Vector Space, there exists $f_1, \ldots, f_n \in X^\ast$ and $\epsilon > 0$ such that:
:$\set {x \in X : \cmod {\map {f_j} x} < \epsilon \text { for each } 1 \le j \le n} \subseteq U$
{{WLOG}} assume that $f_j \ne {\mathbf 0}_{X^\ast}$ for each $j$. 
From Kernel of Linear Transformation is Linear Subspace, we have that:
:$\ker f_j$ is a vector subspace for each $1 \le j \le n$.
From Set of Linear Subspaces is Closed under Intersection:
:$\ds \bigcap_{j \mathop = 1}^n \ker f_j$ is a vector subspace.
From Intersection of Finitely Many Kernels of Linear Functionals in Infinite-Dimensional Vector Space is Infinite-Dimensional with Finite Codimension, we have that:
:$\ds \bigcap_{j \mathop = 1}^n \ker f_j$ is infinite-dimensional
and:
:$\ds \map {\operatorname {codim} } {\bigcap_{j \mathop = 1}^n \ker f_j} < \infty$
where $\operatorname {codim}$ denotes codimension.
{{qed}}
Category:Weak Topologies on Topological Vector Spaces
8gl67a4cowcgu71vw1kng8mnaid04a5
Theorem: Infinite-Dimensional Banach Space contains Basic Sequence with Basis Constant Arbitrarily Close to 1

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be an infinite-dimensional Banach space over $\GF$.
Then for each $\epsilon > 0$, $X$ contains a basic sequence with basis constant at most $1 + \epsilon$.

Proof:
Let:
:$S_X = \set {x \in X : \norm x_X = 1}$
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\cl_w$ be the closure taken in $\struct {X, w}$.
From Weak Closure of Unit Sphere is Closed Unit Ball, we have ${\mathbf 0}_X \in \map {\cl_w} {S_X}$. 
Further:
:$\ds \inf_{x \mathop \in S_X} \norm x = 1 > 0$
From Subset of Banach Space Bounded Away from Zero including Zero Vector in Weak Closure contains Basic Sequence with Basis Constant Arbitrarily Close to 1, for each $\epsilon > 0$, $S_X$ contains a basic sequence with basis constant at most $1 + \epsilon$. 
{{qed}}
Theorem: Subset of Normed Vector Space is Bounded Away from Zero iff Closure does not contain Zero

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$.
Let $S \subseteq X$.
Let $\cl$ be the closure in $\struct {X, \norm {\, \cdot \,} }$.
We have that:
:$\ds \inf_{x \mathop \in S} \norm x > 0$
{{iff}} ${\mathbf 0}_X \not \in \map \cl S$.

Proof:
=== Sufficient Condition ===
Suppose that ${\mathbf 0}_X \not \in \map \cl S$.
Then there exists an open neighborhood $U$ of ${\mathbf 0}_X$ such that $U \cap S = \O$.
From the definition of an open set in a normed vector space, there exists $M > 0$ such that:
:$\set {x \in X : \norm x_X < M} \subseteq U$
so that:
:$\set {x \in X : \norm x_X < M} \cap S = \O$
Hence we have:
:$\ds \inf_{x \mathop \in S} \norm x \ge M > 0$
{{qed|lemma}}
Theorem: Outer Jordan Content of Degenerate Set

Let $M \subseteq \R^n$ be a bounded subset of Euclidean $n$-space.
Suppose that, for every $\tuple {x_1, \dots, x_n} \in M$, we have that:
:$x_k = \gamma$
for some fixed $k \in \set {1, \dots, n}$ and $\gamma \in \R$.
Then:
:$\map {m^*} M = 0$
where $m^*$ denotes the outer Jordan content.

Proof:
For each $i \ne k$, let:
:$a_i$ be a lower bound of $\set {x_i : \tuple {x_1, \dots, x_n} \in M}$
:$b_i$ be an upper bound of $\set {x_i : \tuple {x_1, \dots, x_n} \in M}$
Consider the closed rectangle:
:$R = \closedint {a_1} {b_1} \times \dots \times \closedint {a_{k - 1}} {b_{k - 1}} \times \closedint \gamma \gamma \times \closedint {a_{k + 1}} {b_{k + 1}} \times \dots \times \closedint {a_n} {b_n}$
By the hypothesis, along with the definitions of $a_i$ and $b_i$:
:$M \subseteq R$
Therefore, $\set R$ is a finite covering of $M$ by closed $n$-rectangles.
But since $\gamma - \gamma = 0$:
:$\map V R = 0$
and so:
:$\map {m^*} M \le 0$
The result follows.
{{qed}}
Category:Outer Jordan Content
92ub9t5wgsr1wwzb8qhnau85omhgbq5
Theorem: Bounded Below Weakly Null Sequence in Infinite-Dimensional Banach Space contains Basic Subsequence with Basis Constant Arbitrarily Close to 1

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be an infinite-dimensional Banach space over $\GF$.
Let $w$ be the weak topology on $\struct {X, \norm {\, \cdot \,}_X}$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence converging to $x$ in $\struct {X, w}$ such that:
:$\ds \inf_{n \mathop \in \N} \norm {x_n}_X > 0$
Let $\epsilon > 0$.
Then $\sequence {x_n}_{n \mathop \in \N}$ has a basic subsequence $\sequence {x_{n_k} }_{k \mathop \in \N}$ with basis constant at most $1 + \epsilon$.

Proof:
Let $\cl_w$ be the closure taken in $\struct {X, w}$.
Let $S = \set {x_n : n \in \N}$.
From Point in Set Closure iff Limit of Net, we have ${\mathbf 0}_X \in \map {\cl_w} S$.
From Subset of Banach Space Bounded Away from Zero including Zero Vector in Weak Closure contains Basic Sequence with Basis Constant Arbitrarily Close to 1, $S$ contains a basic sequence $\sequence {y_n}_{n \mathop \in \N}$.
We take:
:$y_k = x_{j_k}$ for each $n \in \N$.
Let $n_1 = j_1$. 
For $k \ge 2$, set $n_k = j_{k^\ast}$ where $k^\ast$ is least such that $j_{k^\ast} > \max \set {n_1, \ldots, n_{k - 1} }$.
We argue that $\sequence {x_{n_k} }_{k \mathop \in \N}$ is basic with basis constant at most $1 + \epsilon$.
Since $\sequence {y_k}_{k \mathop \in \N}$ is basic, for any sequence $\sequence {\alpha_j}_{j \mathop \in \N}$ we have that:
:$\ds \norm {\sum_{j \mathop = 1}^m \alpha_j y_j}_X \le \paren {1 + \epsilon} \norm {\sum_{j \mathop = 1}^n \alpha_j y_j}_X$ for $m \le n$
by Grunblum's Criterion.
Set $\alpha_j = 0$ if $j \ne j_{k^\ast}$ for any $k \in \N$.
Then we obtain:
:$\ds \norm {\sum_{k \mathop = 1}^m \alpha_k x_{n_k} }_X \le \paren {1 + \epsilon} \norm {\sum_{k \mathop = 1}^n \alpha_k x_{n_k} }_X$ for $m \le n$
for any sequence $\sequence {\alpha_k}_{k \mathop \in \N}$ in $\GF$, after relabelling $\alpha_{j_{k^\ast} } = \alpha_k$.
Hence by Grunblum's Criterion,  $\sequence {x_{n_k} }_{k \mathop \in \N}$ is basic with basis constant at most $1 + \epsilon$.
{{qed}}
Theorem: Outer Jordan Content of Subdivision

Let $\RR \subseteq \R^n$ be a closed $n$-rectangle.
Let $M \subseteq \RR$ be a subset.
Let $P$ be a finite subdivision of $\RR$.
Then:
:$\ds \map {m^*} M = \sum_{R \mathop \in P} \map {m^*} {M \cap R^\circ}$
where:
:$m^*$ denotes the outer Jordan content
:$R \in P$ denotes that $R$ is a subrectangle of $P$
:$R^\circ$ denotes the interior of $R$

Proof:
Write $P = \tuple {P_1, P_2, \dots, P_n}$.
Further write $P_i = \set {x_{i,0}, \dots, x_{i, m_i}}$ for each $i$.
By applying Outer Jordan Content of Separated Union for each $\tuple {i, x_{i,j}}$, the result follows.
{{qed}}
Category:Outer Jordan Content
1vo5j7tteg6xz8dsp69u1hwo9qr232j
Theorem: Outer Jordan Content of Closed Rectangle

Let $\RR \subseteq \R^n$ be a closed $n$-rectangle.
Then:
:$\map {m^*} \RR = \map V \RR$
where:
:$m^*$ denotes the outer Jordan content
:$V$ denotes the content of a rectangle

Proof:
Clearly, $\set \RR$ is a finite covering of $\RR$ by closed $n$-rectangles.
Therefore:
:$\map {m^*} \RR \le \map V \RR$
{{qed|lemma}}
Now, let $\varepsilon > 0$ be arbitrary.
By Characterizing Property of Infimum of Subset of Real Numbers, there is a finite covering $\CC$ of $\RR$ by closed $n$-rectangles such that:
:$\ds \sum_{R \mathop \in \CC} \map V R < \map {m^*} \RR + \varepsilon$
{{WLOG}} we may assume that $R \subseteq \RR$ for every $R \in \CC$.
Write:
:$\ds \RR = \prod_{i \mathop = 1}^n \closedint {A_i} {B_i}$
For each $i \in \set {1, \dots, n}$, let:
:$\ds P_i =  \set {a_i, b_i : R = \prod_{j \mathop = 1}^n \closedint {a_j} {b_j} \in \CC}$
or in other words, $P_i$ is a finite subdivision of $\closedint {A_i} {B_i}$ that contains both endpoints of $\closedint {a_i} {b_i}$, for every $R \in \CC$.
Form the subdivision $P = \tuple {P_1, \dots, P_n}$ of $\RR$.
Additionally, for each $R \in \CC$, form the subdivision $P_R = \tuple {P_1 \cap R, \dots, P_n \cap R}$.
Since the endpoints of $R$ are in $P$, every subrectangle of $P_R$ is also a subrectangle of $P$.
Conversely, since $\CC$ covers $\RR$, every subrectangle of $P$ is a subrectangle of some $P_R$.
Therefore, if we denote the set of all subrectangles of $P$ by $P^*$, we find that:
{{begin-eqn}}
{{eqn | l = \map {m^*} \RR + \varepsilon
      | o = >
      | r = \sum_{R \mathop \in \CC} \map V R
}}
{{eqn | r = \sum_{R \mathop \in \CC} \sum_{r \mathop \in P_R^*} \map V r
      | c = Content of Subdivided Rectangle
}}
{{eqn | o = \ge
      | r = \sum_{r \mathop \in P^*} \map V r
      | c = Every $r \in P^*$ appears in some $P_R^*$
}}
{{eqn | r = \map V \RR
      | c = Content of Subdivided Rectangle
}}
{{end-eqn}}
Hence, by Real Plus Epsilon:
:$\map V \RR \le \map {m^*} \RR$
The result follows.
{{qed}}
Category:Outer Jordan Content
9a24ih8lkeozs1efzb08nmln3g446c4
Theorem: Terms in Convergent Series Converge to Zero/Normed Vector Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$.
Let $\sequence {x_j}_{j \mathop \in \N}$ be a sequence such that:
:$\ds \sum_{j \mathop = 1}^\infty x_j$ converges.
Then:
:$x_j \to {\mathbf 0}_X$ in $\struct {X, \norm {\, \cdot \,} }$ as $j \to \infty$.

Proof:
Let:
:$\ds s_n = \sum_{j \mathop = 1}^n x_j$
Let $\epsilon > 0$. 
Since $\sequence {s_n}_{n \mathop \in \N}$ converges, it is Cauchy by Convergent Sequence is Cauchy Sequence.
Hence there exists $N \in \N$ such that for $m, n \ge N$ we have:
:$\norm {s_m - s_n}_X < \epsilon$
Then in particular:
:$\norm {s_n - s_{n - 1} }_X = \norm {x_n}_X < \epsilon$
for $n \ge N + 1$. 
Hence we have $\norm {x_n}_X \to {\mathbf 0}_X$ in $\struct {X, \norm {\, \cdot \,} }$ as $n \to \infty$.
From Sequence in Normed Vector Space Convergent to Limit iff Norm of Sequence minus Limit is Null Sequence, we have:
:$x_j \to {\mathbf 0}_X$ in $\struct {X, \norm {\, \cdot \,} }$ as $j \to \infty$.
{{qed}}
Category:Terms in Convergent Series Converge to Zero
4381x4d1wnab67erhn17m4ia7x5b67m
Theorem: Point in Set Closure iff Limit of Filter

Let $\struct {X, \tau}$ be a topological space.
Let $\cl$ denote closure in $\struct {X, \tau}$. 
Let $\FF$ be a filter on $X$.
Let $E \subseteq X$.
Let $x \in X$.
We have that $x \in \map \cl E$ {{iff}} there exists a filter on $X$ such that: 
:$\FF$ converges to $x$
and:
:$E \in \FF$

Proof:
=== Necessary Condition ===
Let $\UU_x$ be the neighborhood filter at $x$. 
Suppose that $x \in \map \cl E$.
Then $U \cap E \ne \O$ for all $U \in \UU_x$.
Let $\BB = \set {U \cap E : U \in \UU_x}$.
Since $X \in \UU_x$, we have $E \in \BB$ and hence $\BB \ne \O$.
Since $x \in \map \cl E$, we have that:
:$U \cap E \ne \O$ for all $U \in \UU_x$
by the definition of topological closure.
Hence $\O \not \in \BB$.
Finally, let $U_1, U_2 \in \UU_x$.
Then $U_1 \cap U_2 \in \UU_x$, so $\paren {U_1 \cap E} \cap \paren {U_2 \cap E} = \paren {U_1 \cap U_2} \cap E \in \BB$.
Hence we can define $\FF$ as the filter generated by $\BB$.
We have already established that $E \in \BB \subseteq \FF$.
Now, for each $U \in \UU_x$, we have that $U \cap E \in \FF$.
We have $U \cap E \subseteq U$.
Hence, by the definition of a filter, we have $U \in \FF$.
Hence $\UU_x \subseteq \FF$.
Hence $\FF$ converges to $x$.
{{qed}}
Theorem: Filter Generated by Net is Well-Defined

Let $X$ be a set.
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a net.
Then the filter generated by $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ is well-defined.

Proof:
For each $\lambda_0 \in \Lambda$, let $B_{\lambda_0} = \set {x_\lambda : \lambda \succeq \lambda_0}$.
Let $\BB = \set {B_\lambda : \lambda \in \Lambda}$. 
Clearly $\BB \ne \O$ and $\O \not \in \BB$.
We need to show that for each $\lambda_1, \lambda_2 \in \Lambda$, there exists $\lambda_0 \in \Lambda$ such that $B_{\lambda_0} \subseteq B_{\lambda_1} \cap B_{\lambda_2}$.
Since $\struct {\Lambda, \preceq}$ is directed, there exists $\lambda_0 \in \Lambda$ such that $\lambda_0 \succeq \lambda_1$ and $\lambda_0 \succeq \lambda_2$. 
Hence for each $\lambda \in \Lambda$ with $\lambda \succeq \lambda_0$, we have $\lambda_0 \succeq \lambda_1$ and $\lambda_0 \succeq \lambda_2$ by transitivity. 
Hence $\set {x_\lambda : \lambda \succeq \lambda_0} \subseteq \set {x_\lambda : \lambda \succeq \lambda_1} \cap \set {x_\lambda : \lambda \succeq \lambda_2}$. 
This was the requirement.
{{qed}}
Category:Filters on Sets
tpsqz7a0074vx3uet3ij4cnault5vd3