avewright/proofwiki-math huggingface dataset:
Theorem: Perfectly T4 Space is T5

Every perfectly $T_4$ space is a $T_5$ space.

Proof:
Let $T = \struct {S, \tau}$ be a perfectly $T_4$ space.
By Perfectly $T_4$ Property is Hereditary, every subspace of $T$ is also perfectly $T_4$.
In particular, every subspace of $T$ is a $T_4$ space.
{{Recall|T5 Space|$T_5$ space|index = 3}}
{{:Definition:T5 Space/Definition 3}}
It follows that $T$ is a $T_5$ space.
{{qed}}
Theorem: Equivalence of Definitions of Real Exponential Function/Limit of Sequence implies Power Series Expansion

The following definition of the concept of the real exponential function:
=== As the Limit of a Sequence ===
{{:Definition:Exponential Function/Real/Limit of Sequence}}
implies the following definition:
=== As a Power Series Expansion ===
{{:Definition:Exponential Function/Real/Power Series Expansion}}

Proof:
Fix $x \in \R$, and consider the limit:
:$\ds \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$
which is the definition of $\exp x$ as the limit of a sequence.
Since:
:$n \cdot \dfrac x n \to x$
as $n \to \infty$, we have from Generalized Exponential Limit that:
:$\ds \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n = \exp x$
where the right-hand side is defined as a power series.
Hence, for all $x \in \R$, the limit and power series definitions of the exponential function are equivalent.
{{qed}}
Theorem: Equivalence of Definitions of Real Exponential Function/Limit of Sequence implies Power Series Expansion

The following definition of the concept of the real exponential function:
=== As the Limit of a Sequence ===
{{:Definition:Exponential Function/Real/Limit of Sequence}}
implies the following definition:
=== As a Power Series Expansion ===
{{:Definition:Exponential Function/Real/Power Series Expansion}}

Proof:
Let $\exp x$ be the real function defined as the limit of the sequence:
:$\exp x := \ds \lim_{n \mathop \to \infty} \paren {1 + \frac x n}^n$
From the General Binomial Theorem:
{{begin-eqn}}
{{eqn | l = \paren {1 + \frac x n}^n
      | r = 1 + x + \frac {n \paren {n - 1} x^2} {2! \ n^2} + \frac {n \paren {n - 1} \paren {n - 2} x^3} {3! \ n^3} + \cdots
}}
{{eqn | r = \frac {x^0} {0!} + \frac {x^1} {1!} + \paren {\frac {n - 1} n} \frac {x^2} {2!} + \paren {\frac {\paren {n - 1} \paren {n - 2} } {n^2} } \frac {x^3} {3!} + \cdots
}}
{{eqn | r = 1 + x + \paren {1 - \frac 1 n} \frac {x^2} {2!} + \paren {1 - \frac 1 n} \paren {1 - \frac 2 n} \frac {x^3} {3!} + \cdots
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \paren {1 + \frac x n}^n - \paren {1 + x + \paren {1 - \frac 1 n} \frac {x^2} {2!} + \paren {1 - \frac 1 n} \paren {1 - \frac 2 n} \frac {x^3} {3!} + \cdots}
}}
{{end-eqn}}
We have that $\dfrac 1 n$, $\dfrac 2 n$, and so on, are basic null sequences.
Hence from Power over Factorial, this converges to:
:$\exp x - \paren {\dfrac {x^0} {0!} + \dfrac {x^1} {1!} + \dfrac {x^2} {2!} + \dfrac {x^3} {3!} + \cdots} = 0$
as $n \to +\infty$.
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = \exp x
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
}}
{{end-eqn}}
{{qed}}
Theorem: Basis Constant is Greater Than or Equal to One

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a Banach space over $\GF$ with $X \ne \set { {\mathbf 0}_X}$.
Let $E = \sequence {e_n}_{n \mathop \in \N}$ be a Schauder basis for $X$.
Let $K_b$ be the basis constant for $E$. 
Then $K_b \ge 1$.

Proof:
Let $x \in X$ be such that $\norm x = 1$.
Let $\sequence {S_n}_{n \mathop \in \N}$ be the projections associated with $\sequence {e_n}_{n \mathop \in \N}$.
From Projections Associated with Schauder Basis Converge to Identity in Strong Operator Topology and Characterization of Convergence in Strong Operator Topology, we have:
:$\map {S_n} x \to x$
From Modulus of Limit: Normed Vector Space:
:$\norm {\map {S_n} x} \to \norm x = 1$
Then, for each $\epsilon > 0$ there exists $N \in \N$ such that:
:$1 - \epsilon < \norm {\map {S_N} x}$
Let $\map \BB X$ be the space of bounded linear transformations on $\struct {X, \norm {\, \cdot \,} }$.
Let $\norm {\, \cdot \,}_{\map \BB X}$ be the norm on $\map \BB X$.
We then have:
:$1 - \epsilon < \norm {\map {S_N} x} \le \norm {S_N}_{\map \BB X}$
Hence we have:
:$\ds 1 - \epsilon < \sup_{n \mathop \in \N} \norm {S_n}_{\map \BB X} = K_b$
for each $\epsilon > 0$. 
We therefore have $1 \le K_b$.
{{qed}}
Category:Schauder Bases
nb3hv3osd31igwabdi29efghlome3bj
Theorem: Finite Union of Pointwise Equicontinuous Families of Functions is Pointwise Equicontinuous

Let $\struct {X, d_X}$ and $\struct {Y, d_Y}$ be metric spaces.
Let $n \in \N$.
Let $\FF_1, \ldots, \FF_n$ be pointwise equicontinuous families of functions $X \to Y$. 
Let:
:$\ds \FF = \bigcup_{j \mathop = 1}^n \FF_j$ 
Then $\FF$ is pointwise equicontinuous.

Proof:
Let $x_0 \in X$ and $\epsilon > 0$. 
For each $i \in \set {1, \ldots, n}$, there exists $\delta_i > 0$ such that:
:whenever $\map {d_X} {x, x_0} < \delta_i$, we have $\map {d_Y} {\map f x, \map f {x_0} } < \epsilon$ for all $f \in \FF_i$.
Let:
:$\delta = \min \set {\delta_1, \delta_2, \ldots, \delta_n}$
Then for all $x \in X$ with $\map {d_X} {x, x_0} < \delta$, we have $\map {d_X} {x, x_0} < \delta_i$ for each $i \in \set {1, \ldots, n}$ and hence:
:$\map {d_Y} {\map f x, \map f {x_0} } < \epsilon$ for all $f \in \FF_i$.
Hence for all $f \in \FF$ and $x \in X$ with $\map {d_X} {x, x_0} < \delta$, we have:
:$\map {d_Y} {\map f x, \map f {x_0} } < \epsilon$
{{qed}}
Category:Pointwise Equicontinuity
6wndw7juf0st03f9ts2gw5ukvn5wn75
Theorem: Set of Points in Metric Space for which Pointwise Equicontinuous Sequence of Continuous Functions Converges to Continuous Function is Closed

Let $\struct {X, d_X}$ and $\struct {Y, d_Y}$ be metric spaces.
Let $f : X \to Y$ be a continuous function. 
Let $\sequence {f_n}_{n \mathop \in \N}$ be a pointwise equicontinuous sequence of continuous functions $X \to Y$.
Let:
:$C = \set {x \in X : \map {f_n} x \to \map f x \text { as } n \to \infty}$
Then $C$ is closed in $X$.

Proof:
From Finite Set of Continuous Functions between Metric Spaces is Pointwise Equicontinuous, $\set f$ is pointwise equicontinuous.
From Finite Union of Pointwise Equicontinuous Families of Functions is Pointwise Equicontinuous, $\set f \cup \set {f_n : n \in \N}$ is pointwise equicontinuous.
From Subset of Metric Space contains Limits of Sequences iff Closed, it is enough to show that every convergent sequence in $\struct {X, d_X}$ taking values in $C$ has its limit in $C$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a convergent sequence in $\struct {X, d_X}$ with limit $x$ such that:
:$\map {f_n} {x_j} \to \map f {x_j}$ as $n \to \infty$ in $\struct {Y, d_Y}$ for each $j \in \N$. 
We need to show that $\map {f_n} x \to \map f x$ as $n \to \infty$ in $\struct {Y, d_Y}$.
Let $\epsilon > 0$. 
Since $\set f \cup \set {f_n : n \in \N}$ is pointwise equicontinuous, there exists $\delta > 0$ such that whenever:
:$\map {d_X} {x, y} < \delta$
we have:
:$\map {d_Y} {\map f x, \map f y} < \dfrac \epsilon 3$
and:
:$\map {d_Y} {\map {f_n} x, \map {f_n} y} < \dfrac \epsilon 3$ for each $n \in \N$.
Since $x_n \to x$ in $\struct {X, d_X}$, we can take $j \in \N$ such that:
:$\map {d_X} {x, x_j} < \delta$
so that:
:$\map {d_Y} {\map f x, \map f {x_j} } < \dfrac \epsilon 3$
and:
:$\map {d_Y} {\map {f_n} x, \map {f_n} {x_j} } < \dfrac \epsilon 3$ for each $n \in \N$.
We use {{Metric-space-axiom|2}} to write:
:$\map {d_Y} {\map {f_n} x, \map f x} \le \map {d_Y} {\map {f_n} x, \map {f_n} {x_j} } + \map {d_Y} {\map {f_n} {x_j}, \map f {x_j} } + \map {d_Y} {\map f {x_j}, \map f x} < \dfrac {2 \epsilon} 3 + \map {d_Y} {\map {f_n} {x_j}, \map f {x_j} }$
For this $j \in \N$, we have $\map {f_n} {x_j} \to \map f {x_j}$, so we can take $N \in \N$ such that:
:$\ds \map {d_Y} {\map {f_n} {x_j}, \map f {x_j} } < \frac \epsilon 3$ for each $n \ge N$.
Hence we have $\map {d_Y} {\map {f_n} x, \map f x} < \epsilon$ for each $n \ge N$.
Since $\epsilon > 0$ was arbitrary, we have $\map {f_n} x \to \map f x$ in $\struct {Y, d_Y}$.
Hence $x \in C$.
Hence from Subset of Metric Space contains Limits of Sequences iff Closed, $C$ is closed.
{{qed}}
Category:Pointwise Equicontinuity
sxlw1piidpcdq7ga4sb8ddjdq0915zh
Theorem: Uniformly Bounded Sequence of Bounded Linear Transformations is Uniformly Equicontinuous

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be normed vector spaces.
Let $\map \BB {X, Y}$ be the space of bounded linear transformations $X \to Y$.
Let $\norm {\, \cdot \,}_{\map \BB {X, Y} }$ be the norm on $\map \BB {X, Y}$.
Let $\sequence {T_n}_{n \mathop \in \N}$ be a sequence in $\map \BB {X, Y}$ such that:
:$\ds \sup_{n \mathop \in \N} \norm {T_n}_{\map \BB {X, Y} } < \infty$
Then $\sequence {T_n}_{n \mathop \in \N}$ is uniformly equicontinuous.

Proof:
Let $x, y \in X$.
Let:
:$\ds M = \sup_{n \mathop \in \N} \norm {T_n}_{\map \BB {X, Y} }$
Fix $n \in \N$.
From Fundamental Property of Norm on Bounded Linear Transformation, we have:
:$\ds \norm {T_n x - T_n y}_Y = \norm {\map {T_n} {x - y} }_Y \le \norm {T_n}_{\map \BB {X, Y} } \norm {x - y}_X$
We have:
:$\norm {T_n}_{\map \BB {X, Y} } \le M$
Hence:
:$\ds \norm {T_n x - T_n y}_Y \le M \norm {x - y}_X$
Hence $T_n$ is Lipschitz with constant $M$ for each $n \in \N$.
From Family of Lipschitz Continuous Functions with same Lipschitz Constant is Uniformly Equicontinuous, $\sequence {T_n}_{n \mathop \in \N}$ is uniformly equicontinuous. 
{{qed}}
Category:Uniform Equicontinuity
qdlmp9sipjzhz88ve38n5vtwf6f4hx7
Theorem: Condition for Sequence to be Schauder Basis in terms of Coordinate Functionals

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be an infinite-dimensional normed vector space over $\GF$.
Let $\sequence {e_n}_{n \mathop \in \N}$ be a sequence in $X$ such that there exists bounded linear functionals $\sequence {e_n^\ast}_{n \mathop \in \N}$ on $X$ such that:
:$(1) \quad$ $\map {e_n^\ast} {e_j} = \delta_{n j}$ for each $i, j \in \N$
:$(2) \quad$ $\ds x = \sum_{n \mathop = 1}^\infty \map {e_n^\ast} x e_n$ for each $x \in X$
where $\delta$ denotes the Kronecker $\delta$. 
Then $\sequence {e_n}_{n \mathop \in \N}$ is a Schauder basis.

Proof:
It remains to verify that for each $x \in X$, if:
:$\ds \sum_{n \mathop = 1}^\infty \alpha_n e_n = x$
for some sequence $\sequence {\alpha_n}_{n \mathop \in \N}$ in $\GF$, then:
:$\alpha_n = \map {e_n^\ast} x$
Then we will have that:
:$\ds \sum_{n \mathop = 1}^\infty \alpha_n e_n = x$
is satisfied for a unique sequence $\sequence {\alpha_n}_{n \mathop \in \N}$ in $\GF$, and $\sequence {e_n}_{n \mathop \in \N}$ will have been shown to be a Schauder basis.
Let $n \in \N$.
We have:
{{begin-eqn}}
{{eqn	| l = \map {e_n^\ast} x
		| r = \map {e_n^\ast} {\sum_{j \mathop = 1}^\infty \alpha_j e_j}
}}
{{eqn	| r = \map {e_n^\ast} {\lim_{N \mathop \to \infty} \sum_{j \mathop = 1}^N \alpha_j e_j}
}}
{{eqn	| r = \lim_{N \mathop \to \infty} \sum_{j \mathop = 1}^N \alpha_j \map {e_n^\ast} {e_j}
		| c = $e_n^\ast$ is a bounded linear functional and using Sequential Continuity is Equivalent to Continuity in Metric Space
}}
{{eqn	| r = \lim_{N \mathop \to \infty} \sum_{j \mathop = 1}^N \alpha_j \delta_{n j}
}}
{{eqn	| r = \lim_{N \mathop \to \infty} \alpha_n
		| c = for $N \ge n$ we have $\ds \sum_{j \mathop = 1}^N \alpha_j \delta_{n j} = \alpha_n \delta_{n n} = \alpha_n$ by {{Defof|Kronecker Delta}}
}}
{{eqn	| r = \alpha_n 
}}
{{end-eqn}}
as desired.
{{qed}}
Category:Schauder Bases
ta3couw42zssdaq2xuq1s9n43s64q2o
Theorem: Grunblum's Criterion

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a Banach space over $\GF$.
Let $\sequence {e_j}_{j \mathop \in \N}$ be a sequence of non-zero vectors in $X$.
Then $\sequence {e_j}_{j \mathop \in \N}$ is a basic sequence {{iff}} there exists $K > 0$ such that for any sequence $\sequence {\alpha_j}_{j \mathop \in \N}$ in $\GF$ we have:
:$\ds \norm {\sum_{j \mathop = 1}^m \alpha_j e_j} \le K \norm {\sum_{j \mathop = 1}^n \alpha_j e_j}$ for $m \le n$.
Further, if $\sequence {e_j}_{j \mathop \in \N}$ is a basic sequence then the minimal such $K$ is the basis constant $K_b$ of $\sequence {e_j}_{j \mathop \in \N}$.

Proof:
Let $\map \BB X$ be the space of bounded linear transformations.
Let $\norm {\, \cdot \,}_{\map \BB X}$ be the norm on $\map \BB X$.
Theorem: Basic Sequences in Banach Spaces are Equivalent iff Map between is Linear Isomorphism

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ and $\struct {Y, \norm {\, \cdot \,}_Y}$ be Banach spaces over $\GF$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a basic sequence in $\struct {X, \norm {\, \cdot \,}_X}$ and $\sequence {y_n}_{n \mathop \in \N}$ be a basic sequence in $\struct {Y, \norm {\, \cdot \,}_Y}$.
Let $\sqbrk {x_n}_{n \mathop \in \N}$ and $\sqbrk {y_n}_{n \mathop \in \N}$ be the closed linear spans of $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {y_n}_{n \mathop \in \N}$ respectively.  
Then $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {y_n}_{n \mathop \in \N}$ are equivalent {{iff}}:
:there exists a linear isomorphism $T : \sqbrk {x_n}_{n \mathop \in \N} \to \sqbrk {y_n}_{n \mathop \in \N}$ such that:
::$T x_n = y_n$ for each $n \in \N$.

Proof:
{{WLOG}} suppose that $X = \sqbrk {x_n}_{n \mathop \in \N}$ and $Y = \sqbrk {y_n}_{n \mathop \in \N}$.
We are assured that $X$ and $Y$ are still Banach spaces by Closed Subspace of Banach Space forms Banach Space.
Theorem: Block Basic Sequence is Basic Sequence

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a Banach space over $\GF$.
Let $\sequence {e_n}_{n \mathop \in \N}$ be a Schauder basis for $\struct {X, \norm {\, \cdot \,} }$.
Let $K_b$ be the basis constant of $\sequence {e_n}_{n \mathop \in \N}$.
Let $\sequence {p_n}_{n \mathop \in \N}$ be a strictly increasing sequence and let $p_0 = 0$. 
Let $\sequence {\alpha_n}_{n \mathop \in \N}$ be a sequence in $\GF$.
Define a block basic sequence $\sequence {u_n}_{n \mathop \in \N}$ of $\sequence {e_n}_{n \mathop \in \N}$ by:
:$\ds u_n = \sum_{j \mathop = p_{n - 1} + 1}^{p_n} \alpha_j e_j$ 
for each $n \in \N$.
Then $\sequence {u_n}_{n \mathop \in \N}$ is a basic sequence.
Further, let $K_b'$ be the basis constant of $\sequence {u_n}_{n \mathop \in \N}$.
Then $K_b' \le K_b$.

Proof:
Let $\sequence {\beta_k}_{k \mathop \in \N}$ be a sequence in $\GF$.
Then we have:
:$\ds \sum_{k \mathop = 1}^m \beta_k u_k = \sum_{k \mathop = 1}^m \beta_k \sum_{j \mathop = p_{k - 1} + 1}^{p_k} \alpha_j e_j = \sum_{k \mathop = 1}^m \sum_{j \mathop = p_{k - 1} + 1}^{p_k} \beta_k \alpha_j e_j$
Taking $\gamma_j = \alpha_j \beta_k$ for all $p_{k - 1} + 1 \le j \le p_k$, we have:
:$\ds \sum_{k \mathop = 1}^m \alpha_k u_k = \sum_{j \mathop = 1}^{p_m} c_j e_j$
By Grunblum's Criterion applied to $\sequence {e_j}_{j \mathop \in \N}$, we have:
:$\ds \norm {\sum_{j \mathop = 1}^{p_m} c_j e_j} \le K_b \norm {\sum_{j \mathop = 1}^{p_n} c_j e_j} = K_b \norm {\sum_{k \mathop = 1}^n \beta_k u_k}$
We have then shown:
:$\ds \norm {\sum_{k \mathop = 1}^m \beta_k u_k} \le K_b \norm {\sum_{k \mathop = 1}^n \beta_k u_k}$ for $m \le n$
for any sequence $\sequence {\beta_k}_{k \mathop \in \N}$ in $\GF$.
Hence from Grunblum's Criterion, $\sequence {u_n}_{n \mathop \in \N}$ is a basic sequence and $K_b' \le K_b$.
{{qed}}
Theorem: Orthonormal Basis for Separable Hilbert Space is Monotone Basis

Let $\GF \in \set {\R, \C}$.
Let $\HH$ be a separable Hilbert space over $\GF$. 
Let $\sequence {e_n}_{n \mathop \in \N}$ be an orthonormal basis for $\HH$. 
Then $\sequence {e_n}_{n \mathop \in \N}$ is a monotone basis.

Proof:
Let $\map \BB \HH$ be the space of bounded linear transformations on $\HH$.
Let $\norm {\, \cdot \,}_{\map \BB \HH}$ be the norm on $\map \BB \HH$. 
We firstly show that $\sequence {e_n}_{n \mathop \in \N}$ is a Schauder basis.
For each $n \in \N$, define $e_n^\ast : \HH \to \GF$ by:
:$\map {e_n^\ast} x = \innerprod x {e_n}$ for each $x \in \HH$.
Since $\sequence {e_n}_{n \mathop \in \N}$ is an orthogonal set, we have:
:$\map {e_n^\ast} {e_j} = \innerprod {e_n} {e_j} = \delta_{n j}$
where $\delta$ is the Kronecker $\delta$.
From the Riesz Representation Theorem (Hilbert Spaces), $e_n^\ast$ is bounded for each $n \in \N$.
From Characterization of Bases (Hilbert Spaces), we have:
:$\ds x = \sum_{n \mathop = 1}^\infty \innerprod x {e_n} e_n = \sum_{n \mathop = 1}^\infty \map {e_n^\ast} x e_n$
From Condition for Sequence to be Schauder Basis in terms of Coordinate Functionals, $\sequence {e_n}_{n \mathop \in \N}$ is a Schauder basis.
Let $\sequence {S_n}_{n \mathop \in \N}$ be the projections associated with $\sequence {e_n}_{n \mathop \in \N}$.
Let $K_b$ be the basis constant of $\sequence {e_n}_{n \mathop \in \N}$. 
Then we have:
:$\ds \map {S_n} x = \sum_{j \mathop = 1}^n \innerprod x {e_j} e_j$ for each $x \in X$. 
From Pythagoras's Theorem (Inner Product Space) and {{NormAxiomVector|1}}, we have:
:$\ds \norm {\map {S_n} x}^2 = \sum_{j \mathop = 1}^n \cmod {\innerprod x {e_j} }^2$
By Bessel's Inequality, we then have:
:$\norm {\map {S_n} x}^2 \le \norm x^2$ 
Hence:
:$\norm {S_n}_{\map \BB \HH} \le 1$
Then:
:$\ds \sup_{n \mathop \in \N} \norm {S_n}_{\map \BB \HH} \le 1$
Hence by the definition of the basis constant, we have $K_b \le 1$. 
From Basis Constant is Greater Than or Equal to One, we have $1 \le K_b$.
Hence $K_b = 1$.
So $\sequence {e_n}_{n \mathop \in \N}$ is a monotone basis.
{{qed}}
Category:Monotone Bases
Category:Hilbert Spaces
84o7c489ebn5coe3dts04amul3nnhyo
Theorem: Subset of Banach Space Bounded Away from Zero including Zero Vector in Weak Closure contains Basic Sequence with Basis Constant Arbitrarily Close to 1

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $w$ be the weak topology on $X$.
Let $\cl_w$ be the closure taken in $\struct {X, w}$. 
Let $S \subseteq X$ be such that:
:$\ds \inf_{x \mathop \in S} \norm x_X > 0$
and:
:${\mathbf 0}_X \in \map {\cl_w} S$
Let $\epsilon > 0$. 
Then there exists a basic sequence in $S$ with basis constant $K_b \le 1 + \epsilon$.

Proof:
For convenience, we first prove a lemma in the normed dual space of $X$.
Theorem: Equations of Circular Motion in Cartesian Plane/Polar Form

Let:
{{begin-eqn}}
{{eqn | n = 1
      | l = \mathbf e_r
      | r = \mathbf i \cos \theta + \mathbf j \sin \theta
}}
{{eqn | n = 2
      | l = \mathbf e_\theta
      | r = -\mathbf i \sin \theta + \mathbf j \cos \theta
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \mathbf r
      | r = r_0 \mathbf e_r
}}
{{eqn | l = \mathbf v = \dot {\mathbf r}
      | r = r_0 \dot \theta \mathbf e_\theta
}}
{{eqn | l = \mathbf a = \ddot {\mathbf r}
      | r = -r_0 \dot \theta^2 \mathbf e_r + r_0 \ddot \theta e_\theta
}}
{{end-eqn}}

Proof:
From Equations of Circular Motion in Cartesian Plane:
{{begin-eqn}}
{{eqn | l = \mathbf r
      | r = r_0 \paren {\mathbf i \cos \theta + \mathbf j \sin \theta}
}}
{{eqn | l = \mathbf v = \dot {\mathbf r}
      | r = r_0 \paren {-\dot \theta \mathbf i \sin \theta + \dot \theta \mathbf j \cos \theta}
}}
{{eqn | l = \mathbf a = \ddot {\mathbf r}
      | r = r_0 \paren {-\ddot \theta \mathbf i \sin \theta - \dot \theta^2 \mathbf i \cos \theta + \ddot \theta \mathbf j \cos \theta - \dot \theta^2 \mathbf j \sin \theta}
}}
{{end-eqn}}
The result follows by substituting $\mathbf e_r$ and $\mathbf e_\theta$ from $(1)$ and $(2)$.
{{qed}}
Theorem: Weak-* Closure of Isometric Copy of Set in Second Dual contains Isometric Copy of Weak Closure of Set in Original Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $S \subseteq X$. 
Let $w$ be the weak topology on $X$.
Let $\cl_w$ be the closure taken in $\struct {X, w}$. 
Let $\struct {X^{\ast \ast}, \norm {\, \cdot \,}_{X^{\ast \ast} } }$ be the second normed dual of $\struct {X, \norm {\, \cdot \,}_X}$.
Let $w^\ast$ be the weak-$\ast$ topology on $X^{\ast \ast}$.
Let $\cl_{w^\ast}$ be the closure taken in $\struct {X^{\ast \ast}, w^\ast}$. 
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
Then:
:$\map \iota {\map {\cl_w} S} \subseteq \map {\cl_{w^\ast} } {\iota S}$

Proof:
From Evaluation Linear Transformation on Normed Vector Space is Weak to Weak-* Homeomorphism onto Image, $\iota : \struct {X, w} \to \struct {\iota X, w^\ast}$ is a homeomorphism.
From Homeomorphism iff Image of Closure equals Closure of Image and Closure of Subset in Subspace, we have:
:$\map \iota {\map {\cl_w} S} = \map {\cl_{w^\ast} } {\iota S} \cap \iota X$
Hence:
:$\map \iota {\map {\cl_w} S} \subseteq \map {\cl_{w^\ast} } {\iota S}$
{{qed}}
Category:Weak-* Topologies
Category:Weak Topologies on Topological Vector Spaces
6zd570dqe57tqtoh0nw9gxi9my4fucf
Theorem: Dimension of Quotient Vector Space

Let $K$ be a field.
Let $X$ be a vector space over $K$.
Let $Y$ be a vector subspace of $X$.
Let $X/Y$ be the quotient vector space of $X$ modulo $Y$.
Then we have:
:$\dim Y + \map \dim {X/Y} = \dim X$
Hence $X$ is finite-dimensional {{iff}} both $Y$ and $X/Y$ are.

Proof:
We show that there exists disjoint sets $\BB_1, \BB_2$ such that:
:$\size {\BB_1} = \dim Y$
and:
:$\size {\BB_2} = \map \dim {X/Y}$
such that $\BB_1 \cup \BB_2$ is a basis for $X$.
By the definition of dimension and the cardinal sum, we will then have:
:$\dim Y + \map \dim {X/Y} = \dim X$
Let $q : X \to X/Y$ be the quotient mapping.
Let $\BB_1 = \set {y_\alpha : \alpha \in I_1}$ be a basis for $Y$, where $I_1$ is an index set with cardinality $\dim Y$. 
Let $\widetilde {\BB_2} = \set {\map q {z_\beta} : \beta \in I_2}$ be a basis for $\map \dim {X/Y}$, where $I_2$ is an index set with cardinality $\map \dim {X/Y}$.
Let $\BB_2 = \set {\map q {z_\beta} : \beta \in I_2}$.
From Construction of Basis for Vector Space from Basis for Vector Subspace and Basis of Quotient, $\BB_1 \cup \BB_2$ is a basis for $X$ and $\BB_1 \cap \BB_2 = \O$.
Hence $\map \dim X = \size {\BB_1 \cup \BB_2} = \size {\BB_1} + \size {\BB_2} = \map \dim Y + \map \dim {X/Y}$.
Finally, if $X$ is finite-dimensional, then since:
:$\dim Y \le \dim X$
and:
:$\map \dim {X/Y} \le \dim X$
we have that both $Y$ and $X/Y$ are finite-dimensional.
Conversely if $Y$ and $X/Y$ are finite-dimensional then:
:$\dim X = \dim Y + \map \dim {X/Y} < \infty$
{{qed}}
Category:Quotient Vector Spaces
jftzey9chw27uz8ol2cwy67843dtssh