avewright/proofwiki-math huggingface dataset:
Theorem: Chain Rule for Partial Derivatives

Let $F: \R^2 \to \R$ be a real-valued function of $2$ variables.
Let $X: \R^2 \to \R$ and $Y: \R^2 \to \R$ also be real-valued functions of $2$ variables.
Let $F = \map f {x, y}$ be such that:
{{begin-eqn}}
{{eqn | l = x
      | r = \map X {u, v}
}}
{{eqn | l = y
      | r = \map Y {u, v}
}}
{{end-eqn}}
Then:
:$F = \map F {u, v}$
and:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial F} {\partial u}
      | r = \dfrac {\partial f} {\partial x} \dfrac {\partial X} {\partial u} + \dfrac {\partial f} {\partial y} \dfrac {\partial Y} {\partial u}
      | c = 
}}
{{eqn | l = \dfrac {\partial F} {\partial v}
      | r = \dfrac {\partial f} {\partial x} \dfrac {\partial X} {\partial v} + \dfrac {\partial f} {\partial y} \dfrac {\partial Y} {\partial v}
      | c = 
}}
{{end-eqn}}

Proof:
{{ProofWanted|Discussed here: https://www.ma.imperial.ac.uk/~jdg/AECHAIN.PDF which is appropriate considering this result I'm reading from a reference book written by staff at Imperial.<br/>Use Cauchy-Riemann Equations (a special case) as a basis for this, and make that page dependent upon this.}}
Theorem: Almost Convergent Sequence/Examples/Sequence of alternating zeros and ones converges almost to one half

Let $\sequence {x_n}_{n \in \N}$ be the sequence defined by:
:$x_n = \begin{cases} 0 & : n \equiv 0 \pmod 2 \\ 1 & : n \equiv 1 \pmod 2 \end{cases}$
where $\bmod$ denotes the congruence modulo.
Then $\sequence {x_n}_{n \in \N}$ almost converges to $1/2$.

Proof:
Let $\phi$ be a Banach limit.
Let $S$ be the left shift operator on $\map {\ell^\infty} \R$.
Let $\mathbf 1 := \sequence {1, 1, 1, \ldots}$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf 1
      | r = \sequence {1, 0, 1, 0, \ldots} + \sequence {0, 1, 0, 1, \ldots}
}}
{{eqn | r = \map S {\sequence {x_n} } + \sequence {x_n}
      | n = 1
}}
{{end-eqn}}
Thus by definition of Banach limit:
{{begin-eqn}}
{{eqn | l = 1
      | r = \map \phi {\mathbf 1}
}}
{{eqn | r = \map \phi {\map S {\sequence {x_n} } + \sequence {x_n} }
      | c = by $(1)$
}}
{{eqn | r = \map \phi {\map S {\sequence {x_n} } } + \map \phi {\sequence {x_n} }
}}
{{eqn | r = 2 \map \phi {\sequence {x_n} }
}}
{{end-eqn}}
That is:
:$\ds \map \phi {\sequence {x_n} } = \frac 1 2$
As $\phi$ is an arbitrary Banach limit, the claim follows.
{{qed}}
{{mistake|category}}
Category:Definitions/Banach Limits
8f90lq87wyoj7jmkrjytlt0foxzl3rx
Theorem: Meet Semilattice Filter iff Ordered Set Filter

Let $\struct {S, \wedge, \preceq}$ be a meet semilattice.
Let $F \subseteq S$ be a non-empty subset of $S$.
Then:
:$F$ is a meet semilattice filter of $\struct {S, \wedge, \preceq}$ {{iff}} $F$ is an ordered set filter of $\struct {S, \preceq}$.

Proof:
=== Necessary Condition ===
Let $F$ be a meet semilattice filter of $\struct {S, \wedge, \preceq}$.
To show that $F$ is an ordered set filter of $\struct {S, \preceq}$ it is sufficient to show:
{{begin-axiom}}
{{axiom | q = \forall x, y \in F: \exists z \in F
        | m = z \preceq x \text{ and } z \preceq y
}}
{{end-axiom}}
Let $x, y \in F$.
Let $z = x \wedge y$.
By definition of meet semilattice filter, $F$ is a subsemilattice, so:
:$z \in F$
By definition of Meet:
:$z \preceq x \text{ and } z \preceq y$
The result follows.
{{qed|lemma}}
Theorem: Equivalence of Definitions of Lattice Filter

Let $\struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $F \subseteq S$ be a non-empty subset of $S$.
{{TFAE|def = Lattice Filter}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $F$ satisify the lattice filter axioms.
To show that $F$ is a meet semilattice filter it is sufficient to show:
{{begin-axiom}}
{{axiom | lc= $F$ is a upper section of $S$:
        | q = \forall x \in F: \forall y \in S
        | m = x \preceq y \implies y \in F
}}
{{end-axiom}}
Let $x \in F, y \in S : x \preceq y$.
By the lattice filter axioms, $F$ is a sublattice of $\struct {S, \vee, \wedge, \preceq}$, so:
:$x \vee y \in F$
From Preceding iff Join equals Larger Operand:
:$y = x \vee y$
Hence:
:$y \in F$
The result follows.
{{qed|lemma}}
Theorem: Root is Commutative

Let $x \in \R_{> 0}$ be a (strictly) positive real number.
Let $a$ and $b$ be nonzero integers.
Then:
:$\sqrt [a] {\sqrt [b] x} = \sqrt [b] {\sqrt [a] x}$

Proof:
Let $y = \sqrt [a] {\sqrt [b] x}$.
Then
{{begin-eqn}}
{{eqn | l = \sqrt [a] {\sqrt [b] x}
      | r = y
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = \sqrt [b] x
      | r = y^a
      | c = {{Defof|Root of Number}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \paren {y^a}^b
      | c = {{Defof|Root of Number}}
}}
{{eqn | r = y^{a b}
      | c = Product of Indices of Real Number
}}
{{eqn | r = y^{b a}
      | c = Integer Multiplication is Commutative
}}
{{eqn | r = \paren {y^b}^a
      | c = Product of Indices of Real Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [a] x
      | r = y^b
      | c = Existence and Uniqueness of Positive Root of Positive Real Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [b] {\sqrt [a] x}
      | r = y
      | c = Existence and Uniqueness of Positive Root of Positive Real Number
}}
{{eqn | ll= \leadsto
      | l = \sqrt [b] {\sqrt [a] x}
      | r = \sqrt [a] {\sqrt [b] x}
      | c = Definition of $y$
}}
{{end-eqn}}
{{qed}}
Category:Roots of Numbers
ay62d6y9n9wekpcdbmpvjbzpfx795ie
Theorem: Force between Infinite Parallel Straight Conductors carrying Steady Current

Let $s_1$ and $s_2$ be wires in a vacuum carrying steady currents $I_1$ and $I_2$.
Let $s_1$ and $s_2$ be parallel and (effectively) infinitely long.
Then the magnitude of the force per unit distance between $s_1$ and $s_2$ is given by:
:$\dfrac {\d F} {\d l} = \dfrac {\mu_0 I_1 I_2} {2 \pi r}$
where:
:$r$ denotes the distance between $s_1$ and $s_2$
:$\mu_0$ denotes the vacuum permeability
:$\d l$ is an infinitesimal distance along one of the wires.
Furthermore, if the currents are in the same direction, the force is attractive.
Otherwise, it is repulsive.

Proof:
Let $s_1$ lie along the $z$ axis.
Define $I_1$ and $I_2$ to be positive when flowing in the positive $z$ direction and negative otherwise.
Let $s_2$ pass through the point $\tuple {r, 0, 0}$.
From Magnetic Field of Infinite Straight Conductor carrying Steady Current, we have:
:$\map {\mathbf B} {\mathbf r} = \dfrac {\mu_0 I} {2 \pi \rho} \paren {-\sin \theta \, \mathbf i + \cos \theta \, \mathbf j}$
At $s_2$:
{{begin-eqn}}
{{eqn | l = \rho
      | r = \sqrt {x^2 + y^2}
}}
{{eqn | r = r
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \theta
      | r = \arctan \paren {\frac y \rho}
}}
{{eqn | r = 0
}}
{{end-eqn}}
Thus, the magnetic field at $s_2$ due to $I_1$ is:
:$\map {\mathbf B} {s_2} = \dfrac {\mu_0 I_1} {2 \pi r} \mathbf j$
Thus:
{{begin-eqn}}
{{eqn | l = \d \mathbf F_2
      | r = I_2 \d \mathbf l_2 \times \map {\mathbf B} {s_2}
      | c = Magnetic Force on Conductor carrying Steady Current
}}
{{eqn | r = I_2 \d \mathbf l_2 \times \frac {\mu_0 I_1} {2 \pi r} \mathbf j
}}
{{eqn | r = \frac {\mu_0 I_1 I_2} {2 \pi r} \d l_2 \paren {\mathbf k \times \mathbf j}
      | c = $\d \mathbf l_2 = \d l_2 \, \mathbf k$
}}
{{eqn | r = -\frac {\mu_0 I_1 I_2} {2 \pi r} \d l_2 \mathbf i
      | c = $\mathbf k \times \mathbf j = -\mathbf i$
}}
{{end-eqn}}
By Newton's Third Law,
:$\d \mathbf F_1 = \dfrac {\mu_0 I_1 I_2} {2 \pi r} \d l_1 \mathbf i$
Notice that, if $I_1$ and $I_2$ have the same sign (that is, their currents are in the same direction), then the magnetic forces are attractive.
If $I_1$ and $I_2$ have opposite signs (their currents are in opposite direction), the the magnetic forces are repulsive.
The magnitude of the force per unit length between the wires is:
{{begin-eqn}}
{{eqn | l = \frac {\d F} {\d l}
      | r = \size {\frac {\mu_0 I_1 I_2} {2 \pi r} \mathbf i}
}}
{{eqn | r = \frac {\mu_0 I_1 I_2} {2 \pi r}
}}
{{end-eqn}}
{{qed}}
Category:Magnetic Field of Infinite Straight Conductor carrying Steady Current
Category:Electric Current
Category:Magnetic Forces
Category:Electromagnetism
5xytge2bfs9ed1l4rrv327sk78f1bv4
Theorem: Symmetry of Invariant Metric on Vector Space

<onlyinclude>
Let $K$ be a field.
Let $X$ be a vector space over $K$. 
Let $d$ be an invariant metric on $X$. 
Then we have:
:$\map d {x, y} = \map d {-x, -y}$
for each $x, y \in X$.

Proof:
Let $x, y \in X$.
We have:
{{begin-eqn}}
{{eqn	| l = \map d {x, y}
		| r = \map d {x + \paren {-y - x}, y + \paren {-y - x} }
		| c = {{Defof|Invariant Metric on Vector Space}}
}}
{{eqn	| r = \map d {-y, -x}
}}
{{eqn	| r = \map d {-x, -y}
		| c = {{Metric-space-axiom|3}}
}}
{{end-eqn}}
{{qed}}
Category:Invariant Metrics on Vector Spaces
ajx2afjxks36nnjpwfbi8l36jhvni7y
Theorem: Subadditivity of Invariant Metric on Vector Space

Let $K$ be a field.
Let $X$ be a vector space over $K$.
Let $d$ be an invariant metric on $X$.
Then:
:$\map d {n x, {\mathbf 0}_X} \le n \map d {x, {\mathbf 0}_X}$
for each $n \in \N$ and $x \in X$.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \map d {n x, {\mathbf 0}_X}
		| r = \sum_{k \mathop = 1}^n \map d {k x, \paren {k - 1} x}
		| c = {{Metric-space-axiom|2}}
}}
{{eqn	| o = \le 
		| r = \sum_{k \mathop = 1}^n \map d {k x - \paren {k - 1} x, \paren {k - 1} x - \paren {k - 1} x}
		| c = {{Defof|Invariant Metric on Vector Space}}
}}
{{eqn	| r = \sum_{k \mathop = 1}^n \map d {x, {\mathbf 0}_X}
}}
{{eqn	| r = n \map d {x, {\mathbf 0}_X}
}}
{{end-eqn}}
{{qed}}
Theorem: Quotient Metric on Vector Space is Well-Defined

Let $K$ be a field.
Let $X$ be a vector space over $K$. 
Let $d$ be an invariant metric on $X$.
Let $N$ be a vector subspace of $X$.
Let $X/N$ be the quotient vector space of $X$ modulo $N$.
Let $\pi : X \to X/N$ be the quotient mapping. 
Then the mapping $d_N : X/N \times X/N \to \hointr 0 \infty$ defined by:
:$\ds \map {d_N} {\map \pi x, \map \pi y} = \inf_{z \mathop \in N} \map d {x - y, z}$
for each $\map \pi x, \map \pi y \in X/N$, is well-defined.

Proof:
Let $x, y \in X$.
Then $\map d {x - y, z} \ge 0$ for all $z \in N$, and so:
:$\ds \inf_{z \mathop \in N} \map d {x - y, z}$ exists as a real number.
Let $x', y' \in X$ be such that $\map \pi x = \map \pi {x'}$ and $\map \pi y = \map \pi {y'}$.
We now need to show that if $x', y' \in X$ are such that:
:$\map \pi x = \map \pi {x'}$
and:
:$\map \pi y = \map \pi {y'}$
then:
:$\ds \inf_{z \mathop \in N} \map d {x - y, z} = \inf_{z \mathop \in N} \map d {x' - y', z}$
From Quotient Mapping is Linear Transformation, we have $\map \pi {x' - x} = {\mathbf 0}_{X/N}$ and $\map \pi {y' - y} = {\mathbf 0}_{X/N}$. 
From Kernel of Quotient Mapping, we obtain $x' \in x + N$ and $y' \in y + N$.
Then there exists $z_1, z_2 \in N$ such that $x' = x + z_1$ and $y' = y + z_2$. 
Then we have:
{{begin-eqn}}
{{eqn	| l = \inf_{z \mathop \in N} \map d {x' - y', z}
		| r = \inf_{z \mathop \in N} \map d {x + z_1 - \paren {y + z_2}, z}
}}
{{eqn	| r = \inf_{z \mathop \in N} \map d {\paren {x - y} + \paren {z_1 - z_2}, z}
}}
{{eqn	| r = \inf_{z \mathop \in N} \map d {x - y, z - \paren {z_1 - z_2} }
		| c = {{Defof|Invariant Metric on Vector Space}}
}}
{{eqn	| r = \inf_{z' \mathop \in N - \paren {z_1 - z_2} } \map d {x - y, z'}
}}
{{eqn	| r = \inf_{z' \mathop \in N} \map d {x - y, z'}
		| c = {{Defof|Vector Subspace}}
}}
{{end-eqn}}
as required.
{{qed}}
Category:Quotient Metrics on Vector Spaces
1fy4iwqim5n56zg224ijo06v1ie6s6e
Theorem: Quotient Metric on Vector Space is Invariant Pseudometric

Let $K$ be a field.
Let $X$ be a vector space over $K$. 
Let $d$ be an invariant metric on $X$.
Let $N$ be a vector subspace of $X$.
Let $X/N$ be the quotient vector space of $X$ modulo $N$.
Let $\pi : X \to X/N$ be the quotient mapping.
Let $d_N$ be the quotient metric on $X/N$ induced by $d$.
Then $d_N$ is an invariant pseudometric.

Proof:
=== Proof of {{Metric-space-axiom|1}} ===
Let $x, y \in X$.
Then, we have:
:$\ds \map {d_N} {\map \pi x, \map \pi x} = \inf_{z \mathop \in N} \map d {x - x, z} = \inf_{z \mathop \in N} \map d { {\mathbf 0}_X, z}$
Since $N$ is a vector subspace, we have ${\mathbf 0}_X \in N$.
From {{Metric-space-axiom|1}}, we have $\map d { {\mathbf 0}_X, {\mathbf 0}_X} = 0$, and so:
:$\ds \inf_{z \mathop \in N} \map d { {\mathbf 0}_X, z} \le 0$
Since we also have:
:$\ds \inf_{z \mathop \in N} \map d { {\mathbf 0}_X, z} \ge 0$
we obtain:
:$\ds \inf_{z \mathop \in N} \map d { {\mathbf 0}_X, z} = 0$
Hence we have proved {{Metric-space-axiom|1}} for $d_N$.
{{qed|lemma}}
Theorem: Quotient Metric on Vector Space is Invariant Metric iff Vector Subspace is Closed

Let $K$ be a field.
Let $X$ be a vector space over $K$. 
Let $d$ be an invariant metric on $X$.
Let $N$ be a vector subspace of $X$.
Let $X/N$ be the quotient vector space of $X$ modulo $N$.
Let $\pi : X \to X/N$ be the quotient mapping.
Let $d_N$ be the quotient metric on $X/N$ induced by $d$.
Then $d_N$ is an invariant metric {{iff}} $N$ is closed.

Proof:
From Quotient Metric on Vector Space is Invariant Pseudometric, $d_N$ is an invariant pseudometric.
It remains to show that {{Metric-space-axiom|4}} holds {{iff}} $N$ is closed.
Note that {{Metric-space-axiom|4}} holds {{iff}} for $x, y \in X$:
:$\map {d_N} {\map \pi x, \map \pi y} = 0$
implies that $\map \pi x = \map \pi y$.
That is, {{iff}} for $x, y \in X$:
:$\ds \inf_{z \mathop \in N} \map d {x - y, z} = 0$
implies that $\map \pi x = \map \pi y$. 
That is, {{iff}} for $x, y \in X$:
:$\map d {x - y, N} = 0$
implies that $\map \pi x = \map \pi y$.
From Quotient Mapping is Linear Transformation and Kernel of Quotient Mapping, $\map \pi x = \map \pi y$ is equivalent to $x - y \in N$.
Setting $y = {\mathbf 0}_X$, we can see that:
:for $x, y \in X$:
::$\map d {x - y, N} = 0$
:implies that $x - y \in N$
implies that:
:for all $x \in X$:
::$\map d {x, N} = 0$
:implies that $x \in N$.
Clearly the converse implication also holds.
From Subset of Metric Space is Closed iff contains all Zero Distance Points, we have that:
:for all $x \in X$:
::$\map d {x, N} = 0$
:implies that $x \in N$
holds {{iff}} $N$ is closed.
Hence {{Metric-space-axiom|4}} holds {{iff}} $N$ is closed.
{{qed}}
Category:Quotient Metrics on Vector Spaces
0qdl0r77ykft5sb28dtfgfotyc4122h
Theorem: Generalized Sum Restricted to Non-zero Summands

Let $G$ be a commutative topological semigroup with identity $0_G$.
Let $\family{g_i}_{i \in I}$ be an indexed family of elements of $G$.
Let $J = \set{i \in I : g_i \ne 0_G}$
Let $h \in G$.
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converges to $h$
{{iff}}:
:the generalized sum $\ds \sum_{j \mathop \in J} g_j$ converges to $h$

Proof:
=== Necessary Condition ===
Let the generalized sum $\ds \sum_{i \mathop \in I} g_i$ converge to $h$.
It will be shown that $\ds \sum_{j \mathop \in J} g_j$ converges to $h$.
{{:Generalized Sum Restricted to Non-zero Summands/Necessary Condition}}{{qed|lemma}}
Theorem: Functional Completeness over Finite Number of Arguments

Every truth function is definable from the set of Binary Truth Functions.

Proof:
Let $f : \Bbb B^k \to \Bbb B$ be an arbitrary truth function.
Suppose that $k = 0$.
Then, let:
:$b = \map f {}$
If $b = T$, then let:
:$\map g {p, q} = \map {f_\T} {p, q} = T$
otherwise, if $b = F$:
:$\map g {p, q} = \map {f_\F} {p, q} = F$
Finally, let $\map i {} = \tuple {\F, \F}$.
$i$ is clearly an injection, and:
:$\map g {\map i {}} = b$
Thus, $f = g \circ i$, and $f$ is definable for $k = 0$.
If $k = 1$, then by Unary Truth Functions, $f$ is either:
* Constant $\F$
* Constant $\T$
* Identity
* Logical Not
If $f$ is constant mapping, then the same $g$ definitions work as above.
If $f$ is identity or logical not, then we use:
:$\map g {p, q} = \map {\pr_1} {p, q} = p$
and
:$\map g {p, q} = \map {\overline {\pr_1}} {p, q} = \neg p$
respectively.
We also define:
:$\map i p = \tuple {p, \F}$
As $f = g \circ i$, every $f$ is definable for $k = 1$.
For all remaining $k$, we will proceed by mathematical induction.
Theorem: Translation of Open Ball in Invariant Pseudometric on Vector Space

Let $K$ be a field.
Let $X$ be a vector space over $K$.
Let $d$ be an invariant pseudometric on $X$.
For $x \in X$ and $\epsilon > 0$, let $\map {B_\epsilon} x$ be the open ball centered at $x$ with radius $\epsilon$. 
Let $y \in X$.
Then:
:$\map {B_\epsilon} x + y = \map {B_\epsilon} {x + y}$

Proof:
Let $z \in X$.
Then we have $z \in \map {B_\epsilon} x + y$ {{iff}} $z = u + y$ for $u \in \map {B_\epsilon} x$. 
That is, {{iff}} $z - y \in \map {B_\epsilon} x$. 
This is equivalent to:
:$\map d {z - y, x} < \epsilon$
Since $d$ is invariant, this is equivalent to:
:$\map d {z, x + y} < \epsilon$ 
So, we have $z \in \map {B_\epsilon} x + y$ {{iff}} $z \in \map {B_\epsilon} {x + y}$.
Hence $\map {B_\epsilon} x + y = \map {B_\epsilon} {x + y}$.
{{qed}}
Category:Invariant Pseudometrics on Vector Spaces
qf3cjl9srfj6r00q6vfqonnwtz0cu3o
Theorem: Topological Vector Space over Connected Topological Field is Connected

Let $K$ be a connected topological field.
Let $X$ be a topological vector space over $K$. 
Then $X$ is connected.

Proof:
From the definition of a topological vector space, the mapping $\circ_X : K \times X \to X$ defined by:
:$\map {\circ_X} {\lambda, x} = \lambda x$
for $\tuple {\lambda, x} \in K \times X$ is continuous.
Let $x \in X$. 
From Horizontal Section of Continuous Function is Continuous, the mapping $c_x : K \to X$ defined by:
:$\map {c_x} \lambda = \lambda x$
for $\lambda \in K$ is continuous.
Since $K$ is connected, we have that:
:$c_x \sqbrk K$ is connected
from Continuous Image of Connected Space is Connected. 
That is:
:$K x$ is connected.
Since $x \in K x$ for each $x \in X$, we have:
:$\ds X = \bigcup_{x \in X} K x$
Since $0_K \circ x = {\mathbf 0}_X$ for each $x \in X$, we have that:
:$\ds {\mathbf 0}_X \in \bigcap_{x \in X} K x$
From Union of Connected Sets with Common Point is Connected, we have that:
:$\ds \bigcup_{x \in X} K x$ is connected.
Hence $X$ is connected.
{{qed}}
Category:Topological Vector Spaces
Category:Connected Topological Spaces
qufdbpflpnxfaik37di10jtspqcpz87
Theorem: Quantum-Charge Ratio

The ratio of Planck's constant to the elementary charge is given by:
{{begin-eqn}}
{{eqn | l = \dfrac h \E
      | o = \approx
      | r = 4 \cdotp 13566 \, 7697 \times 10^{-15}
      | c = joule seconds per coulombs
      | cc= {{OEIS|A343571}}
}}
{{eqn | o = \approx
      | r = 4 \cdotp 13566 \, 7697 \times 10^{-7}
      | c = erg seconds per abcoulomb
}}
{{eqn | o = \approx
      | r = 1 \cdotp 37951 \, 0386 \times 10^{-17}
      | c = erg seconds per statcoulomb
}}
{{end-eqn}}

Proof:
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 = \E
      | r = 1 \cdotp 60217 \, 6634 \times 10^{−19} \, \mathrm C
      | c = that is: coulombs
      | cc= {{Defof|Elementary Charge}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac h \E
      | o = \approx
      | r = 4 \cdotp 13566 \, 7697 \times 10^{-15} \, \mathrm {J \, s / C}
      | cc= by calculation
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = h
      | r = 6 \cdotp 62607 \, 015 \times 10^{-27} \, \mathrm {erg \, s}
      | c = that is: erg seconds
      | cc= {{Defof|Planck's Constant|subdef = Value}}
}}
{{eqn | l = \E
      | r = 1 \cdotp 60217 \, 6634 \times 10^{−20} \, \mathrm {abC}
      | c = that is: abcoulombs
      | cc= {{Defof|Elementary Charge}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac h \E
      | o = \approx
      | r = 4 \cdotp 13566 \, 7697 \times 10^{-7} \, \mathrm {erg \, s / abC}
      | c = by calculation
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = h
      | r = 6 \cdotp 62607 \, 015 \times 10^{-27} \, \mathrm {erg \, s}
      | c = that is: erg seconds
      | cc= {{Defof|Planck's Constant|subdef = Value}}
}}
{{eqn | l = \E
      | r = 4 \cdotp 80320 \, 42510 \times 10^{-10} \, \mathrm {statC}
      | c = that is: statcoulombs
      | cc= {{Defof|Elementary Charge}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac h \E
      | o = \approx
      | r = 1 \cdotp 37951 \, 0386 \times 10^{-17} \, \mathrm {erg \, s / statC}
      | c = by calculation
}}
{{end-eqn}}
{{qed}}
Theorem: Birkhoff-Kakutani Theorem/Topological Vector Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Then $\struct {X, \tau}$ is pseudometrizable {{iff}} $\struct {X, \tau}$ is first-countable.
Further, if $\struct {X, \tau}$ is pseudometrizable then there exists an invariant pseudometric $d$ on $X$ such that:
:$(1): \quad$ $d$ induces $\tau$
:$(2): \quad$ the open balls in $\struct {X, d}$ are balanced.

Proof:
=== Sufficient Condition ===
Suppose that $\struct {X, \tau}$ is first-countable and Hausdorff.
Let $\sequence {U_n}_{n \mathop \in \N}$ be a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$.
Let $V_1 = U_1$. 
From Open Neighborhood of Point in Topological Vector Space contains Sum of Open Neighborhoods: Corollary 2:
:for $j \ge 2$, we can inductively pick an open neighborhood $V_j$ of ${\mathbf 0}_X$ such that:
::$V_j + V_j \subseteq V_{j - 1} \cap U_{j - 1}$
:so that $V_j + V_j \subseteq V_{j - 1}$. 
Since $V_j \subseteq U_j$ for each $j \in \N$, and ${\mathbf 0}_X \in V_j$ for each $j \in \N$, $\sequence {V_n}_{n \mathop \in \N}$ is also a local basis for ${\mathbf 0}_X$ in $\struct {X, \tau}$.
Let $D$ be the set of real numbers with a terminating binary notation.
That is, the real numbers $r \in \R$ of the form:
:$\ds r = \sum_{j \mathop = 1}^\infty \map {c_j} r 2^{-j}$ 
with $\map {c_j} r \in \set {0, 1}$ such that:
:there exists $N \in \N$ such that $\map {c_j} r = 0$ for $j > N$.
From the Basis Representation Theorem, the coefficients $\map {c_j} r$ uniquely identify $r$.
Note that if $r, s \in D$ and $r + s < 1$, then $r + s \in D$. 
Now, for $r \ge 1$, set $\map A r = X$. 
For $r \in D$, set:
:$\ds \map A r = \sum_{j \mathop = 1}^\infty \map {c_j} r V_j$
where $\ds \sum_{j \mathop = 1}^\infty$ denotes linear combination.
Note that from Linear Combination of Balanced Sets is Balanced, $\map A r$ is balanced for each $r \in D$.
Since $\map A 1 = X$, we have that:
:$\set {r \in D \cup \hointr 1 \infty : x \in \map A r} \ne \O$
for each $x \in X$. 
Hence:
:$\inf \set {r \in D \cup \hointr 1 \infty : x \in \map A r}$ is finite.
So, we can define $f : X \to \hointr 0 \infty$ by:
:$\map f x = \inf \set {r \in D \cup \hointr 1 \infty : x \in \map A r}$ 
for each $x \in X$.
Define:
:$\map d {x, y} = \map f {x - y}$
We aim to show that $d$ is a pseudometric. 
We require the following lemma:
Theorem: Compton Wavelength of Electron

The Compton wavelength of the electron is:
{{begin-eqn}}
{{eqn | l = \lambda_\E
      | o = \approx
      | r = 2 \cdotp 42631 \, 02386 \, 7(73) \times 10^{-12} \, \mathrm m
}}
{{eqn | o = \approx
      | r = 2 \cdotp 42631 \, 02386 \, 7(73) \times 10^{-10} \, \mathrm {cm}
}}
{{end-eqn}}

Proof:
By definition, the Compton wavelength $\lambda_\E$ of an electron is given as:
:$\lambda_\E = \dfrac h {m_\E c}$
where:
:$m_\E$ denotes the mass of the electron
:$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_\E
      | o = \approx
      | r = 9 \cdotp 10938 \, 37015 \, (28) \times 10^{-31} \, \mathrm {kg}
      | c = that is: kilograms
      | cc= Mass of Electron
}}
{{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_\E
      | o = \approx
      | r = \dfrac {6 \cdotp 62607 \, 015 \times 10^{-34} } {9 \cdotp 10938 \, 37015 \, (28) \times 10^{-31} \times 299 \, 792 \, 458} \, \mathrm m
}}
{{eqn | o = \approx
      | r = 2 \cdotp 42631 \, 02386 \, 7 (73) \times 10^{-12} \, \mathrm m
      | cc= by calculation
}}
{{eqn | o = \approx
      | r = 2 \cdotp 42631 \, 02386 \, 7 (73) \times 10^{-10} \, \mathrm {cm}
      | cc= by calculation
}}
{{end-eqn}}
{{qed}}