avewright/proofwiki-math huggingface dataset:
Theorem: Reduced Compton Wavelength of Electron

The Compton wavelength of the electron is:
{{begin-eqn}}
{{eqn | l = \lambdabar_\E
      | o = \approx
      | r = 3 \cdotp 86159 \, 267 \times 10^{-13} \, \mathrm m
}}
{{eqn | o = \approx
      | r = 3 \cdotp 86159 \, 267 \times 10^{-11} \, \mathrm {cm}
}}
{{end-eqn}}

Proof:
By definition, the reduced Compton wavelength $\lambdabar_\E$ of an electron is given as:
:$\lambdabar_\E = \dfrac {\lambda_\E} {2 \pi}$
where $\lambda_\E$ denotes the Compton wavelength of the electron.
Then we have:
{{begin-eqn}}
{{eqn | l = \lambda_\E
      | o = \approx
      | r = 2 \cdotp 42631 \, 02386 \, 7(73) \times 10^{-12} \, \mathrm m
      | c = Compton Wavelength of Electron
}}
{{eqn | ll= \leadsto
      | l = \lambdabar_\E
      | o = \approx
      | r = \dfrac {2 \cdotp 42631 \, 02386 \, 7(73) \times 10^{-12} } {2 \pi} \, \mathrm m
      | c = 
}}
{{eqn | o = \approx
      | r = 3 \cdotp 86159 \, 267 \times 10^{-13} \, \mathrm m
      | c = by calculation
}}
{{eqn | o = \approx
      | r = 3 \cdotp 86159 \, 267 \times 10^{-11} \, \mathrm {cm}
      | c = by calculation
}}
{{end-eqn}}
{{qed}}
Theorem: Translation of Local Basis in Topological Vector Space

Let $K$ be a topological field.
Let $\struct {X, \tau}$ be a topological vector space over $K$.
Let $\sequence {U_\alpha}_{\alpha \mathop \in A}$ be a local basis at ${\mathbf 0}_X$.
Let $x \in X$.
Then $\sequence {U_\alpha + x}_{\alpha \in A}$ is an local basis at $x$.

Proof:
From Translation of Open Set in Topological Vector Space is Open, $U_\alpha + x$ is an open neighborhood of $x$ in $\struct {X, \tau}$ for each $\alpha \in A$. 
Let $U$ be an open neighborhood of $x$ in $\struct {X, \tau}$.
From Translation of Open Set in Topological Vector Space is Open, $U - x$ is an open neighborhood of ${\mathbf 0}_X$ in $\struct {X, \tau}$.
Since $\sequence {U_\alpha}_{\alpha \mathop \in A}$ is local basis at ${\mathbf 0}_X$, there exists $\beta \in A$ such that:
:$U_\beta \subseteq U - x$ 
Then:
:$U_\beta + x \subseteq U$
Since $U$ was arbitrary, we obtain that $\sequence {U_\alpha + x}_{\alpha \in A}$ is an local basis at ${\mathbf 0}_X$.
{{qed}}
Category:Local Bases
Category:Topological Vector Spaces
Category:Translation of Subsets of Vector Spaces
86mfvxasokshobqbs82celgayei9on8
Theorem: Dilation of Subset of Vector Space Distributes over Sum/General Case

Let $\family {E_\alpha}_{\alpha \mathop \in A}$ be an $A$-indexed family of sets. 
Let $\lambda \in K$.
Then:
:$\ds \lambda \sum_{\alpha \mathop \in A} E_\alpha = \sum_{\alpha \mathop \in A} \paren {\lambda E_\alpha}$

Proof:
Let $x \in X$.
We have:
:$\ds x \in \lambda \sum_{\alpha \mathop \in A} E_\alpha$
{{iff}} there exists:
:a finite subset $F \subseteq E_\alpha$
:$x_\alpha \in F$ for each $\alpha \in F$
such that:
:$\ds x = \lambda \sum_{\alpha \in F} x_\alpha$
This is equivalent to:
:$\ds x = \sum_{\alpha \in F} \lambda x_\alpha$
for a finite subset $F \subseteq E_\alpha$, with $x_\alpha \in F$ for each $\alpha \in F$. 
Hence we obtain:
:$\ds x \in \lambda \sum_{\alpha \mathop \in A} E_\alpha$ {{iff}} $x \in \sum_{\alpha \mathop \in A} \paren {\lambda E_\alpha}$
so that:
:$\ds \lambda \sum_{\alpha \mathop \in A} E_\alpha = \sum_{\alpha \mathop \in A} \paren {\lambda E_\alpha}$
{{qed}}
Category:Dilation of Subset of Vector Space Distributes over Sum
a39p3oddf54h37zs949aqeru99myqj5
Theorem: Dilation of Subset of Vector Space Distributes over Sum/Finite Case

Let $A_1, \ldots, A_n \subseteq X$ and $\lambda \in \GF$. 
Then:
:$\ds \lambda \sum_{j \mathop = 1}^n A_j = \sum_{j = 1}^n \paren {\lambda A_j}$
where:
:$\ds \lambda \paren \ldots$ denotes dilation by $\lambda$
:$\ds \sum_{j \mathop = 1}^n A_j$ denotes the linear combination of subsets of a vector space.

Proof:
Let $x \in X$.
We have:
:$\ds x \in \lambda \sum_{j \mathop = 1}^n A_j$
{{iff}} there exists $x_j \in A_j$ for each $j \in \set {1, 2, \ldots, n}$ such that:
:$\ds x = \lambda \sum_{j \mathop = 1}^n x_j$
This is equivalent to:
:$\ds x = \sum_{j \mathop = 1}^n \lambda x_j \in \sum_{j = 1}^n \paren {\lambda A_j}$ for some $x_j \in A_j$. 
Hence we have:
:$\ds x \in \lambda \sum_{j \mathop = 1}^n A_j$
{{iff}}:
:$\ds x \in \sum_{j = 1}^n \paren {\lambda A_j}$
Hence we obtain:
:$\ds \lambda \sum_{j \mathop = 1}^n A_j = \sum_{j = 1}^n \paren {\lambda A_j}$
{{qed}}
Category:Dilation of Subset of Vector Space Distributes over Sum
efcqj1frtarem86vh334r8300eq5nn5
Theorem: Linear Combination of Balanced Sets is Balanced

Let $\GF \in \set {\R, \C}$.
Let $X$ be a vector space over $\GF$.
Let $\family {E_\alpha}_{\alpha \mathop \in A}$ be an $A$-indexed family of balanced sets. 
Let $\lambda_\alpha \in \GF$ for each $\alpha \mathop \in A$. 
Then:
:$\ds \sum_{\alpha \mathop \in A} \lambda_\alpha E_\alpha$ is balanced.

Proof:
Let $s \in \C$ have $\cmod s \le 1$.
Then, we have:
{{begin-eqn}}
{{eqn	| l = s \sum_{\alpha \mathop \in A} \lambda_\alpha E_\alpha
		| r = \sum_{\alpha \mathop \in A} \lambda_\alpha \paren {s E_\alpha}
		| c = Dilation of Subset of Vector Space Distributes over Sum: General Case
}}
{{eqn	| o = \subseteq
		| r = \sum_{\alpha \mathop \in A} \lambda_\alpha E_\alpha 
		| c = {{Defof|Balanced Set}}
}}
{{end-eqn}}
So:
:$\ds \sum_{\alpha \mathop \in A} \lambda_\alpha E_\alpha$ is balanced.
{{qed}}
Category:Balanced Sets
bb0s79bdleuj7j33unq79cq42cux5tu
Theorem: Compton Wavelength of Proton

The Compton wavelength of the proton is:
{{begin-eqn}}
{{eqn | l = \lambda_{\mathrm p}
      | o = \approx
      | r = 1 \cdotp 32140 \, 98553 \, 9(40) \times 10^{-15} \, \mathrm m
}}
{{eqn | o = \approx
      | r = 1 \cdotp 32140 \, 98553 \, 9(40) \times 10^{-13} \, \mathrm {cm}
}}
{{end-eqn}}

Proof:
By definition, the Compton wavelength $\lambda_{\mathrm p}$ of a proton is given as:
:$\lambda_{\mathrm p} = \dfrac h {m_{\mathrm p} c}$
where:
:$m_{\mathrm p}$ denotes the mass of the proton
:$h$ denotes Planck's constant
:$c$ denotes the speed of light.
Then we have:
{{begin-eqn}}
{{eqn | l = h
      | r = 6 \cdotp 62607 \, 015 \times 10^{-34} \, \mathrm {J \, s}
      | c = that is: joule seconds
      | cc= {{Defof|Planck's Constant|subdef = Value}}
}}
{{eqn | l = m_{\mathrm p}
      | o = \approx
      | r = 1 \cdotp 67262 \, 19236 \, 9(51) \times 10^{-27} \, \mathrm {kg}
      | c = that is: kilograms
      | cc= Mass of Proton
}}
{{eqn | l = c
      | r = 299 \, 792 \, 458 \, \mathrm {m \, s^{-1} }
      | c = that is: metres per second
      | cc= {{Defof|Speed of Light|subdef = Value}}
}}
{{eqn | ll= \leadsto
      | l = \lambda_{\mathrm p}
      | o = \approx
      | r = \dfrac {6 \cdotp 62607 \, 015 \times 10^{-34} } {1 \cdotp 67262 \, 19236 \, 9(51) \times 10^{-27} \times 299 \, 792 \, 458} \, \mathrm m
}}
{{eqn | o = \approx
      | r = 1 \cdotp 32140 \, 98553 \, 9(40) \times 10^{-15} \, \mathrm m
      | cc= by calculation
}}
{{eqn | o = \approx
      | r = 1 \cdotp 32140 \, 98553 \, 9(40) \times 10^{-13} \, \mathrm {cm}
      | cc= by calculation
}}
{{end-eqn}}
{{qed}}
Theorem: Reduced Compton Wavelength of Proton

The Compton wavelength of the proton is:
{{begin-eqn}}
{{eqn | l = \lambdabar_{\mathrm p}
      | o = \approx
      | r = 2 \cdotp 10308 \, 9103 \times 10^{-16} \, \mathrm m
}}
{{eqn | o = \approx
      | r = 2 \cdotp 10308 \, 9103 \times 10^{-14} \, \mathrm {cm}
}}
{{end-eqn}}

Proof:
By definition, the reduced Compton wavelength $\lambdabar_{\mathrm p}$ of a proton is given as:
:$\lambdabar_{\mathrm p} = \dfrac {\lambda_{\mathrm p} } {2 \pi}$
where $\lambda_{\mathrm p}$ denotes the Compton wavelength of the proton.
Then we have:
{{begin-eqn}}
{{eqn | l = \lambda_{\mathrm p}
      | o = \approx
      | r = 1 \cdotp 32140 \, 98553 \, 9(40) \times 10^{-15} \, \mathrm m
      | c = Compton Wavelength of Proton
}}
{{eqn | ll= \leadsto
      | l = \lambdabar_{\mathrm p}
      | o = \approx
      | r = \dfrac {1 \cdotp 32140 \, 98553 \, 9(40) \times 10^{-15} } {2 \pi} \, \mathrm m
      | c = 
}}
{{eqn | o = \approx
      | r = 2 \cdotp 10308 \, 9103 \times 10^{-16} \, \mathrm m
      | c = by calculation
}}
{{eqn | o = \approx
      | r = 2 \cdotp 10308 \, 9103 \times 10^{-14} \, \mathrm {cm}
      | c = by calculation
}}
{{end-eqn}}
{{qed}}
Theorem: Pseudometric Space is First-Countable

Let $M = \struct {A, d}$ be a pseudometric space.
Then $M$ is first-countable.

Proof:
Let $x \in A$.
Let:
:$\BB = \set {\map {B_{1/n} } x: n \in \N_{>0} }$
where $\map {B_\epsilon} x$ denotes the open $\epsilon$-ball of $x$ in $M$.
By Surjection from Natural Numbers iff Countable, we have that $\BB$ is countable.
By the definition of a first-countable space, it suffices to show that $\BB$ is a local basis at $x$.
By Open Ball of Pseudometric Space is Open Set, every element of $\BB$ is an open neighborhood of $x$.
Let $U$ be an open neighborhood of $x$.
By the definition of an open set, there exists a strictly positive real number $\epsilon$ such that $\map {B_\epsilon} x \subseteq U$.
By the Axiom of Archimedes, there exists a natural number $n > \dfrac 1 \epsilon$.
That is, $\dfrac 1 n < \epsilon$, and so:
:$\map {B_{1/n} } x \subseteq \map {B_\epsilon} x \subseteq U$
The result follows from Subset Relation is Transitive.
{{qed}}
Category:Pseudometric Spaces
Category:First-Countable Spaces
sj56p0d2fnkpbbqjiqqtxhkz35s79s2
Theorem: Open Ball is Open Set/Pseudometric Space

Let $M = \struct {A, d}$ be a pseudometric space.
Let $x \in A$.
Let $\epsilon \in \R_{>0}$.
Let $\map {B_\epsilon} x$ be an open $\epsilon$-ball of $x$ in $M$.
Then $\map {B_\epsilon} x$ is an open set of $M$.

Proof:
Let $y \in \map {B_\epsilon} x$.
From Open Ball of Point Inside Open Ball, there exists $\delta \in \R_{>0}$ such that:
:$\map {B_\delta} y \subseteq \map {B_\epsilon} x$
The result follows from the definition of open set.
{{qed}}
Category:Open Ball is Open Set
Category:Open Sets (Pseudometric Spaces)
cfo383emog4gc3sb9ds6voahhtm6k8a
Theorem: Dimension of Rydberg Constant

The '''Rydberg constant''' has the dimension $\mathsf {L^{-1} }$.

Proof:
By definition, the Rydberg constant is:
:$R_\infty = \dfrac {m_\E \E^4} {8 \varepsilon_0^2 h^3 c}$
where:
:$m_\E$ denotes the electron rest mass
:$\E$ denotes the elementary charge
:$\varepsilon_0$ denotes the vacuum permittivity
:$h$ denotes Planck's constant
:$c$ denotes the speed of light.
We have:
{{begin-eqn}}
{{eqn | l = m_\E
      | o = \text {has dimension}
      | r = \mathsf M
      | c = {{Defof|Mass of Electron}}
}}
{{eqn | l = \E
      | o = \text {has dimension}
      | r = \mathsf {I T}
      | c = {{Defof|Elementary Charge}}
}}
{{eqn | l = \varepsilon_0
      | o = \text {has dimension}
      | r = \mathsf {M^{-1} L^{-3} T^4 I^2}
      | c = {{Defof|Vacuum Permittivity|subdef = Dimension}}
}}
{{eqn | l = h
      | o = \text {has dimension}
      | r = \mathsf {M L^2 T^{-1} }
      | c = {{Defof|Planck's Constant|subdef = Dimension}}
}}
{{eqn | l = c
      | o = \text {has dimension}
      | r = \mathsf {L T^{-1} }
      | c = {{Defof|Speed of Light|subdef = Dimension}}
}}
{{eqn | ll= \leadsto
      | l = R_\infty
      | o = \text {has dimension}
      | r = \dfrac {\mathsf M \cdot \paren {\mathsf {I T} }^4} {\paren {\mathsf {M^{-1} L^{-3} T^4 I^2} }^2 \cdot \paren {\mathsf {M L^2 T^{-1} } }^3 \cdot \mathsf {L T^{-1} } }
      | c = 
}}
{{eqn | r = \dfrac {\mathsf {M I^4 T^4 } } {\mathsf {M^{-2} L^{-6} T^8 I^4} \cdot \mathsf {M^3 L^6 T^{-3} } \cdot \mathsf {L T^{-1} } }
      | c = 
}}
{{eqn | r = \dfrac {\mathsf {M I^4 T^4 } } {\mathsf {M L T^4 I^4} }
      | c = 
}}
{{eqn | r = \mathsf {L^{-1} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Rydberg Constant
Category:Dimensions of Measurement
ssaq0ap0r4g3vp2781xw3z56eizd11m
Theorem: Null Sequence in Metrizable Topological Vector Space Dominates some Sequence of Scalars Tending to Infinity

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a metrizable topological vector space over $\GF$.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence with $x_n \to {\mathbf 0}_X$. 
Then there exists a sequence of positive real numbers $\sequence {\gamma_n}_{n \mathop \in \N}$ such that:
:$\gamma_n \to \infty$
and:
:$\gamma_n x_n \to {\mathbf 0}_X$

Proof:
From Birkhoff-Kakutani Theorem: Topological Vector Space, there exists an invariant metric $d$ on $X$ that induces $\tau$.
Then:
:$\map d {x_n, { {\mathbf 0}_X} } \to 0$
Pick $n_1 \in \N$ such that:
:$\map d {x_n, { {\mathbf 0}_X} } < 1$ for $n > n_1$.
Inductively, for $k \ge 2$, pick $n_k > n_{k - 1}$ such that:
:$\map d {x_n, { {\mathbf 0}_X} } < k^{-2}$ for $n > n_k$.
For $n < n_2$, set $\gamma_n = 1$. 
For $k \ge 2$ and $n_k \le n < n_{k + 1}$, set $\gamma_n = k$.
For each $n$, let $\map k n$ be the unique $k \in \N$ such that $n_k \le n < n_{k + 1}$. 
Since $n_k < n_{k + 1}$, we have $\map k n \to \infty$ as $n \to \infty$.
Now, for $n \ge n_2$:
{{begin-eqn}}
{{eqn	| l = \map d {\gamma_n x_n, { {\mathbf 0}_X} }
		| r = \map d {\map k n x_n, { {\mathbf 0}_X} }
}}
{{eqn	| o = \le
		| r = \map k n \map d {x_n, { {\mathbf 0}_X} }
		| c = Subadditivity of Invariant Metric on Vector Space
}}
{{eqn	| o = <
		| r = \frac 1 {\map k n}
		| c = since $\map d {x_n, { {\mathbf 0}_X} } < k^{-2}$ for $n > n_k$
}}
{{end-eqn}}
Taking $n \to \infty$, we obtain:
:$\map d {\gamma_n x_n, { {\mathbf 0}_X} } \to 0$
and hence:
:$\gamma_n x_n \to {\mathbf 0}_X$
{{qed}}
Theorem: Characterization of Continuous Linear Transformation from Metrizable Topological Vector Space to Topological Vector Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau_X}$ be a metrizable topological vector space over $\GF$.
Let $\struct {Y, \tau_Y}$ be a topological vector space over $\GF$.
Let $T : X \to Y$ be a linear transformation.
{{TFAE}}
:$(1): \quad$ $T$ is continuous
:$(2): \quad$ $T$ is bounded
:$(3): \quad$ for every sequence $\sequence {x_n}_{n \mathop \in \N}$ in $X$ with $x_n \to {\mathbf 0}_X$ as $n \to \infty$, the sequence $\sequence {T x_n}_{n \mathop \in \N}$ is von Neumann-bounded in $Y$
:$(4): \quad$ for every sequence $\sequence {x_n}_{n \mathop \in \N}$ in $X$ with $x_n \to {\mathbf 0}_X$ as $n \to \infty$, we have $T x_n \to {\mathbf 0}_Y$ as $n \to \infty$.

Proof:
=== $(1)$ implies $(2)$ ===
This is precisely the result Continuous Linear Transformation between Topological Vector Spaces is Bounded.
{{qed|lemma}}
Theorem: Composition of Open Mappings is Open Mapping

Let $\struct {X, \tau_X}$, $\struct {Y, \tau_Y}$ and $\struct {Z, \tau_Z}$ be topological spaces.
Let $f : X \to Y$ and $g : Y \to Z$ be open mappings.
Then $g \circ f : X \to Z$ is an open mapping.

Proof:
Let $U$ be an open set in $\struct {X, \tau_X}$.
Since $f : X \to Y$ is open, we have $f \sqbrk U \in \tau_Y$.
Since $g : Y \to Z$ is open, we have $g \sqbrk {f \sqbrk U} \in \tau_Z$.
That is, whenever $U \in \tau_X$, we have $\paren {g \circ f} \sqbrk U \in \tau_Z$.
So $g \circ f : X \to Z$ is an open mapping.
{{qed}}
Category:Open Mappings
n4gifvca8krw3cgb2b6mfmx006eayno
Theorem: Factorization of Open Linear Transformation between Topological Vector Spaces

Let $K$ be a topological field.
Let $\struct {X, \tau_X}$ and $\struct {Y, \tau_X}$ be topological vector spaces over $K$.
Let $T : X \to Y$ be a linear transformation.
Let $N$ be a vector subspace of $X$ with $N \subseteq \ker T$. 
Let $\struct {X/N, \tau_N}$ be the quotient topological vector space of $X$ modulo $N$.
Let $\pi : X \to X/N$ be the quotient mapping.
Then $T$ is open {{iff}}:
:there exists a open linear transformation $\Lambda : X/N \to Y$ such that:
::$T x = \map \Lambda {\map \pi x}$
:for each $x \in X$.

Proof:
=== Necessary Condition ===
Suppose that $T$ is open.
From Condition for Mapping from Quotient Vector Space to be Well-Defined, there exists a linear transformation $\Lambda : X/N \to Y$ such that $T x = \map \Lambda {\map \pi x}$ for each $x \in X$.
It remains to show that $\Lambda$ is open.
Let $E \subseteq X/N$. 
We want to show that:
:$\Lambda \sqbrk E = T \sqbrk {\pi^{-1} \sqbrk E}$
Let $y \in \Lambda \sqbrk E$.
So there exists $\map \pi x \in E$ such that $\Lambda {\map \pi x} = y$. 
That is, $T x = y$. 
Since $\map \pi x \in E$, we have $x \in \pi^{-1} \sqbrk E$.
So we have $y \in T \sqbrk {\pi^{-1} \sqbrk E}$. 
Hence we have $\Lambda \sqbrk E \subseteq T \sqbrk {\pi^{-1} \sqbrk E}$.
Now let $z \in T \sqbrk {\pi^{-1} \sqbrk E}$.
Then there exists $x \in \pi^{-1} \sqbrk E$ such that $T x = z$. 
Then we have $z = \map \Lambda {\map \pi x}$.
Since $x \in \pi^{-1} \sqbrk E$, we have $\map \pi x \in E$.
So, since $z = \map \Lambda {\map \pi x}$, we have $z \in \Lambda \sqbrk E$.
So we have $T \sqbrk {\pi^{-1} \sqbrk E} \subseteq \Lambda \sqbrk E$.
So we conclude that $\Lambda \sqbrk E = T \sqbrk {\pi^{-1} \sqbrk E}$.
Now let $E$ be an open set in $\struct {X/N, \tau_N}$. 
By the definition of the quotient topology, $\pi$ is continuous.
So $\pi^{-1} \sqbrk E$ is open in $\struct {X, \tau_X}$. 
Since $T$ is open, we have that $T \sqbrk {\pi^{-1} \sqbrk E}$ is open in $\struct {Y, \tau_Y}$.
That is, $\Lambda \sqbrk E$ is open in $\struct {Y, \tau_Y}$.
Since $E$ was an arbitrary open set in $\struct {X/N, \tau_N}$, we have that $\Lambda$ is open.
{{qed|lemma}}
Theorem: First Isomorphism Theorem/Vector Spaces

Let $K$ be a field.
Let $X$ and $Y$ be vector spaces over $K$.
Let $T : X \to Y$ be a linear transformation.
Let $\ker T$ be the kernel of $T$.
Let $X/\ker T$ be the quotient vector space of $X$ modulo $\ker T$.
Then $X/\ker T$ is isomorphic to $\Img T$ as a vector space.

Proof:
From Image of Linear Transformation is Submodule, we assure ourselves that $\Img T$ is indeed a vector space over $K$.
Let $\pi : X \to X/\ker T$ be the quotient mapping. 
From Condition for Mapping from Quotient Vector Space to be Well-Defined, there exists a linear transformation $\Lambda : X/\ker T \to \Img T$ such that:
:$\map \Lambda {\map \pi x} = T x$ for each $x \in X$.
To finish, we need to show that $\Lambda$ is injective and surjective.
From Linear Transformation is Injective iff Kernel Contains Only Zero, to show $\Lambda$ is injective it suffices to show that:
:$\ker \Lambda = \set { {\mathbf 0}_{X/\ker T} }$
Suppose that $\map \Lambda {\map \pi x} = {\mathbf 0}_Y$.
Then $T x = {\mathbf 0}_Y$.
So $x \in \ker T$. 
That is, by Kernel of Quotient Mapping, we have $\map \pi x = {\mathbf 0}_{X/\ker T}$.
So we have $\ker \Lambda = \set { {\mathbf 0}_{X/\ker T} }$, and so $\ker \Lambda$ is injective by Linear Transformation is Injective iff Kernel Contains Only Zero.
Now let $y \in \Img T$.
Then there exists $x \in X$ such that $y = T x$.
Then, we have $\map \Lambda {\map \pi x} = T x = y$. 
So $\Img T \subseteq \Img \Lambda$.
Since we already have $\Img \Lambda \subseteq \Img T$, we obtain $\Img \Lambda = \Img T$.
So $\Lambda : X/\ker T \to \Img T$ is a vector space isomorphism.
{{qed}}
Category:First Isomorphism Theorem
Category:Vector Spaces
879ny8gs9mprnylpk0xgv2p1acid17j
Theorem: Open Ball of Point Inside Open Ball/Pseudometric Space

Let $M = \struct {A, d}$ be a pseudometric space.
Let $\map {B_\epsilon} x$ be an open $\epsilon$-ball in $M = \struct {A, d}$.
Let $y \in \map {B_\epsilon} x$.
Then:
:$\exists \delta \in \R: \map {B_\delta} y \subseteq \map {B_\epsilon} x$
That is, for every point in an open $\epsilon$-ball in a pseudometric space, there exists an open $\delta$-ball of that point entirely contained within that open $\epsilon$-ball.

Proof:
Let $\delta = \epsilon - \map d {x, y}$.
From the definition of open ball, this is strictly positive, since $y \in \map {B_\epsilon} x$.
If $z \in \map {B_\delta} y$, then $\map d {x, y} < \delta$.
So:
:$\map d {x, z} \le \map d {x, y} + \map d {y, z} < \map d {x, y} + \delta = \epsilon$
Thus $z \in \map {B_\epsilon} x$.
So $\map {B_\delta} y \subseteq \map {B_\epsilon} x$.
{{qed}}
Category:Open Balls
Category:Open Ball of Point Inside Open Ball
kvievf77nma2lhs5vtskpe2uzim8lly
Theorem: Vector Subspace of Hausdorff Topological Vector Space is Hausdorff Topological Vector Space

Let $\struct {K, +_K, \circ_K, \tau_K}$ be a topological field.
Let $\struct {\struct {X, +_X, \circ_X}_K, \tau_X}$ be a Hausdorff topological vector space over $K$.
Let $\struct {Y, +_Y, \circ_Y}_K$ be a vector subspace of $X$. 
where:
:$+_Y : Y \times Y \to Y$ is the restriction of $+_X$ to $Y \times Y$
:$\circ_Y : K \times Y \to Y$ is the restriction of $\circ_X$ to $K \times Y$.
Let $\tau_Y$ be the subspace topology on $Y$ induced by $\tau_X$.
Then $\struct {\struct {Y, +_Y, \circ_Y}_K, \tau_Y}$ is a Hausdorff topological vector space over $K$.

Proof:
From Vector Subspace of Topological Vector Space is Topological Vector Space, $\struct {\struct {Y, +_Y, \circ_Y}_K, \tau_Y}$ is a topological vector space over $K$.
Since $\struct {\struct {X, +_X, \circ_X}_K, \tau_X}$ is a Hausdorff topological vector space over $K$, it is {{apriori}} Hausdorff.
We are given that $\struct {Y, +_Y, \circ_Y}_K$ is a vector subspace of $X$.
We are also given that $\tau_Y$ is the subspace topology on $Y$ induced by $\tau_X$.
So $\struct {\struct {Y, +_Y, \circ_Y}_K, \tau_Y}$ is a topological subspace of $\struct {\struct {X, +_X, \circ_X}_K, \tau_X}$ over $K$.
By Subspace of Hausdorff Space is Hausdorff, we have that $\struct {\struct {Y, +_Y, \circ_Y}_K, \tau_Y}$ is Hausdorff.
So $\struct {\struct {Y, +_Y, \circ_Y}_K, \tau_Y}$ is a Hausdorff topological vector space over $K$.
{{qed}}
Category:Hausdorff Topological Vector Spaces
9fwh5nhx97cxi4018e7yy4gsle5nogr
Theorem: Dimension of Bohr Radius

The '''Bohr radius''' has the dimension $\mathsf L$.

Proof:
By definition, the Bohr radius is:
:$a_0 = \dfrac {\varepsilon_0 h^2} {\pi \E^2 m_\E}$
where:
:$\varepsilon_0$ denotes the vacuum permittivity
:$h$ denotes Planck's constant
:$\E$ denotes the elementary charge
:$m_\E$ denotes the electron rest mass
We have:
{{begin-eqn}}
{{eqn | l = \varepsilon_0
      | o = \text {has dimension}
      | r = \mathsf {M^{-1} L^{-3} T^4 I^2}
      | c = {{Defof|Vacuum Permittivity|subdef = Dimension}}
}}
{{eqn | l = h
      | o = \text {has dimension}
      | r = \mathsf {M L^2 T^{-1} }
      | c = {{Defof|Planck's Constant|subdef = Dimension}}
}}
{{eqn | l = \E
      | o = \text {has dimension}
      | r = \mathsf {I T}
      | c = {{Defof|Elementary Charge}}
}}
{{eqn | l = m_\E
      | o = \text {has dimension}
      | r = \mathsf M
      | c = {{Defof|Mass of Electron}}
}}
{{eqn | ll= \leadsto
      | l = a_0
      | o = \text {has dimension}
      | r = \dfrac {\mathsf {M^{-1} L^{-3} T^4 I^2} \cdot \paren {\mathsf {M L^2 T^{-1} } }^2} {\paren {\mathsf {I T} }^2 \cdot \mathsf M}
      | c = 
}}
{{eqn | r = \dfrac {\mathsf {M L T^2 I^2} } {\mathsf {M I^2 T^2} }
      | c = 
}}
{{eqn | r = \mathsf L
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Bohr Radius
Category:Dimensions of Measurement
jvt7fggspo6e6je3luxmzu15lb8jrhj
Theorem: Interior of Translation of Set in Topological Vector Space is Translation of Interior

Let $K$ be a topological field.
Let $\struct {X, \tau}$ be a topological vector space over $K$.
Let $E \subseteq X$. 
Let $x \in X$.
Then:
:$\paren {E + x}^\circ = E^\circ + x$

Proof:
Let $y \in \paren {E + x}^\circ$.
Then there exists an open neighborhood $U$ of $y$ such that $U \subseteq E + x$.
Then from Translation of Open Set in Topological Vector Space is Open, $U - x$ is an open neighborhood of $y - x$ such that $U - x \subseteq E$.
Hence $y - x \in E^\circ$.
So $y \in E^\circ + x$.
We therefore obtain $\paren {E + x}^\circ \subseteq E^\circ + x$.
Now let $y \in E^\circ + x$.
Then $y - x \in E^\circ$.
So there exists an open neighborhood $U$ of $y - x$ such that $U \subseteq E$.
Then from Translation of Open Set in Topological Vector Space is Open, $U + x$ is an open neighborhood of $y$ such that $U + x \subseteq E + x$. 
Hence $y \in \paren {E + x}^\circ$.
We therefore obtain $E^\circ + x \subseteq \paren {E + x}^\circ$.
So $\paren {E + x}^\circ = E^\circ + x$.
{{qed}}
Category:Translation of Subsets of Vector Spaces
Category:Set Interiors
Category:Topological Vector Spaces
26u99fbhqo5ca9cccioik6sm0j2w97w