avewright/proofwiki-math huggingface dataset:
Theorem: Combination Theorem for Continuous Mappings/Topological Division Ring/Inverse Rule

:$g^{-1}: \struct {U, \tau_{_U} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
Let $R^* = R \setminus \set 0$.
Let $\tau^*$ be the subspace topology on $R^*$.
By definition of a topological division ring:
:$\phi: \struct {R^*, \tau^*} \to \struct {R, \tau_{_R} }$ such that $\forall x \in R^*: \map \phi x = x^{-1}$ is a continuous mapping
Let $g^*: \struct {U, \tau_{_U} } \to \struct {R^*, \tau^*}$ be the restriction of $g$ to $U \subseteq R$.
From Restriction of Continuous Mapping is Continuous, $g^*$ is a continuous mapping.
From Composite of Continuous Mappings is Continuous, the composition $\phi \circ g^* : \struct {U, \tau_{_U} } \to \struct {R, \tau_{_R} }$ is continuous.
Now:
{{begin-eqn}}
{{eqn | q = \forall x \in U
      | l = \map {\paren {g^{-1} } } x
      | r = \map g x^{-1}
      | c = Definition of $g^{-1}$
}}
{{eqn | r = \map \phi {\map g x}
      | c = Definition of $\phi$
}}
{{eqn | r = \map \phi {\map {g^*} x}
      | c = Since $\map g x \ne 0$ 
}}
{{eqn | r = \map {\paren {\phi \circ g^*} } x
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
From Equality of Mappings:
:$g^{-1} = \phi \circ g^*$
The result follows.
{{qed}}
Category:Combination Theorem for Continuous Mappings to Topological Division Ring
o3z73zmek5mmxbcr17up0wwlvwcsphz
Theorem: Combination Theorem for Continuous Mappings/Topological Division Ring/Negation Rule

:$-g: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
By definition of a topological division ring:
:$\struct {R, +, *, \tau_{_R} }$ is a topological ring.
From Negation Rule for Continuous Mappings to Topological Ring:
:$-g: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Combination Theorem for Continuous Mappings/Topological Ring/Translation Rule

:$\lambda + f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
By definition of a topological ring:
:$\struct {R, +, \tau_{_R} }$ is a topological group.
From Multiple Rule for Continuous Mappings to Topological Group:
:$\lambda + f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Combination Theorem for Continuous Mappings/Topological Division Ring/Translation Rule

:$\lambda + f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
By definition of a topological division ring:
:$\struct {R, +, *, \tau_{_R} }$ is a topological ring.
From Translation Rule for Continuous Mappings to Topological Ring:
:$\lambda + f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Pointwise Operation is Composite of Operation with Mapping to Cartesian Product

Let $S$ be a set.
Let $\struct {T, *}$ be an algebraic structure.
Let $T^S$ be the set of all mappings from $S$ to $T$.
Let the algebraic structure $\struct {T^S, \oplus}$ be the algebraic structure on $T^S$ induced by $*$.
Let $f, g \in T^S$, that is, let $f: S \to T$ and $g: S \to T$ be mappings.
Let $f \times g : S \to T \times T$ be the mapping from $S$ to the cartesian product $T \times T$ defined by:
:$\forall x \in S : \map {\paren {f \times g}} x = \tuple {\map f x, \map g x}$
Then:
:$f \oplus g = * \circ \paren {f \times g}$
That is, $f \oplus g$ is the composition of the binary operation $*$ with the mapping $f \times g: S \to T \times T$.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = \map {\paren {* \circ \paren {f \times g} } } x
      | r = \map * {\map {\paren {f \times g} } x}
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map * {\tuple {\map f x, \map g x} }
      | c = Definition of $f \times g$
}}
{{eqn | r = \map f x * \map g x
      | c = Definition of $*$
}}
{{eqn | r = \map {\paren {f \oplus g} } x
      | c = Definition of $f \oplus g$
}}
{{end-eqn}}
From Equality of Mappings:
:$* \circ \paren {f \times g} = f \oplus g$
{{qed}}
Category:Abstract Algebra
Category:Pointwise Operations
7n5qzybytb7hrspzohw2ucjxtjf4tde
Theorem: Integral Representation of Bessel Function of the First Kind/Integer Order

Let $n \in \Z$ be an integer.
Then:
:$\ds \map {J_n} x = \dfrac 1 \pi \int_0^\pi \map \cos {n \theta - x \sin \theta} \rd \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \map \exp {\dfrac x 2 \paren {t - \dfrac 1 t} }
      | r = \sum_{m \mathop = -\infty}^\infty \map {J_m} x t^m
      | c = Generating Function for Bessel Function of the First Kind of Order n of x
}}
{{eqn | l = \dfrac 1 {2 \pi i} \int_C t^{-n - 1} \map \exp {\dfrac x 2 \paren {t - \dfrac 1 t} } \rd t
      | r = \dfrac 1 {2 \pi i} \int_C t^{-n - 1} \sum_{n \mathop = - \infty}^\infty \map {J_m} x t^m \rd t
      | c = where $C$ denotes a contour encircling the origin once 
}}
{{eqn | r = \sum_{n \mathop = - \infty}^\infty \dfrac {\map {J_m} x} {2 \pi i} \int_C t^{m - n - 1} \rd t
      | c = 
}}
{{eqn | r = \dfrac {\map {J_n} x} {2 \pi i} 2 \pi i
      | c = Cauchy's Residue Theorem
}}
{{eqn | r = \map {J_n} x
      | c = 
}}
{{end-eqn}}
Take $C$ to be the unit circle.
Write $t = e^{-i \theta}$ and let $\theta$ be decreasing from $\pi$ to $-\pi$, so that we integrate along $C$ anticlockwise.
Then:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = \map {J_n} x
      | r = \dfrac 1 {2 \pi i} \int_\pi^{-\pi} e^{-i \theta \paren {-n - 1} } \map \exp {\dfrac x 2 \paren {e^{-i \theta} - e^{i \theta} } } \rd e^{-i \theta}
      | c = 
}}
{{eqn | r = \dfrac 1 {2 \pi} \int_{-\pi}^\pi \map \exp {- x i \sin \theta + i n \theta} \rd \theta
      | c = Sine in terms of Hyperbolic Sine
}}
{{eqn | r = \dfrac 1 {2 \pi} \paren {\int_0^\pi \map \exp {i n \theta - i x \sin \theta} \rd \theta + \int_{-\pi}^0 \map \exp {i n \theta - i x \sin \theta} \rd \theta}
      | c = 
}}
{{eqn | r = \dfrac 1 {2 \pi} \paren {\int_0^\pi \map \exp {i n \theta - i x \sin \theta} \rd \theta - \int_\pi^0 \map \exp {i n \paren {-\theta} - i x \map \sin {-\theta} } \rd \theta}
      | c = substitution of $-\theta$
}}
{{eqn | r = \dfrac 1 {2 \pi} \paren {\int_0^\pi \map \exp {i n \theta - i x \sin \theta} \rd \theta + \int_0^\pi \map \exp {-\paren {i n \theta - i x \sin \theta} } \rd \theta}
      | c =
}}
{{eqn | r = \dfrac 1 \pi \int_0^\pi \map \cos {n \theta - x \sin \theta} \rd \theta
      | c = Cosine in terms of Hyperbolic Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Integral Representation of Bessel Function of the First Kind/Non-Integer Order

Let $n \in \Z$ be an integer.
Then:
:$\ds \map {J_n} x = \dfrac {x^n} {2^n \sqrt \pi \map \Gamma {n + \frac 1 2} } \int_0^\pi \map \cos {x \sin \theta} \cos^{2 n} \theta \rd \theta$

Proof:
{{ProofWanted|big job}}
Theorem: Combination Theorem for Continuous Mappings/Normed Division Ring/Translation Rule

:$\lambda + f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is continuous.

Proof:
From {{Corollary|Normed Division Ring Operations are Continuous}}:
:$\struct{R, +, *, \tau_{_R} }$ is a topological division ring.
From Translation Rule for Continuous Mappings to Topological Division Ring:
:$\lambda + f: \struct {S, \tau_{_S} } \to \struct {R, \tau_{_R} }$ is a continuous mapping.
{{qed}}
Theorem: Combination Theorem for Continuous Mappings/Normed Division Ring/Negation Rule

:$- g : \struct{S, \tau_{_S}} \to \struct{R, \tau_{_R}}$ is continuous.

Proof:
From {{Corollary|Normed Division Ring Operations are Continuous}}, $\struct{R, +, *, \tau_{_R}}$ is a topological division ring.
From Negation Rule for Continuous Mappings to Topological Division Ring, $- g : \struct{S, \tau_{_S}} \to \struct{R, \tau_{_R}}$ is a continuous mapping.
{{qed}}
Theorem: Legendre Transform of Strictly Convex Real Function is Strictly Convex

Let $\map f x$ be a strictly convex real function.
Then the function $\map {f^*} p$ acquired through the Legendre Transform is also strictly convex.

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\d f^*} {\d p}
      | r = -\frac {\d \map f {\map x p} } {\d p} + \frac {\map \d {p \map x p} } {\d p}
      | c = {{Defof|Legendre Transform}}
}}
{{eqn | r = -f' \frac {\d x} {\d p} + x + p \frac {\d x} {\d p}
      | c = Product Rule for Derivatives
}}
{{eqn | r = -p \frac {\d x} {\d p} + x + p \frac {\d x} {\d p}
      | c = Definition of $p$
}}
{{eqn | r = x
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \frac {\d^2 f^*} {\d p^2}
      | r = \map {x'} p
}}
{{eqn | r = \frac 1 {\map {p'} x}
      | c = Derivative of Inverse Function
}}
{{eqn | r = \frac 1 {\map {f''} x}
      | c = Definition of $p$
}}
{{end-eqn}}
We have that $\map f x$ is real and strictly convex.
Hence, by Real Function is Strictly Convex iff Derivative is Strictly Increasing, $\map {f'} x$ is strictly increasing.
Then:
:$\map {f''} x > 0$
Therefore, the first derivative of $f^*$ is strictly increasing.
By Real Function is Strictly Convex iff Derivative is Strictly Increasing, $f^*$ is strictly convex.
{{qed}}
Theorem: Additive Regular Representations of Topological Ring are Homeomorphisms

Let $\struct {R, + , \circ, \tau}$ be a topological ring.
Let $x \in R$.
Let $\lambda_x$ and $\rho_x$ be the left and right regular representations of $\struct {R, +}$ with respect to $x$.
Then $\lambda_x, \,\rho_x: \struct {R, \tau} \to \struct {R, \tau}$ are homeomorphisms with inverses $\lambda_{-x}, \,\rho_{-x}: \struct {R, \tau} \to \struct {R, \tau}$ respectively.

Proof:
By definition of a topological ring, $ \struct {R, + , \tau}$ is a topological group.
From Right and Left Regular Representations in Topological Group are Homeomorphisms:
:$\lambda_x, \,\rho_x: \struct {R, \tau} \to \struct {R, \tau}$ are homeomorphisms with inverses $\,\lambda_{-x}, \,\rho_{-x}: \struct {R, \tau} \to \struct {R, \tau}$ respectively.
{{qed}}
Category:Topological Rings
0imlmciqm2d3kw2gprai012lniwq176
Theorem: Multiplicative Regular Representations of Units of Topological Ring are Homeomorphisms

Let $\struct{R, + , \circ, \tau}$ be a topological ring with unity $1_R$.
For all $y \in R$, let $\lambda_y$ and $\rho_y$ denote the left and right regular representations of $\struct{R, \circ}$ with respect to $y$.
Let $x \in R$ be a unit of $R$ with product inverse $x^{-1}$.
Then $\lambda_x, \, \rho_x: \struct{R, \tau} \to \struct{R, \tau}$ are homeomorphisms with inverse mappings $\lambda_{x^{-1} }, \, \rho_{x^{-1} }: \struct{R, \tau} \to \struct{R, \tau}$ respectively.

Proof:
Let $I_{_R} : R \to R$ be the identity mapping on $R$.
For all $y \in R$, let $y * I_{_R} : R \to R$ be the mapping defined by:
:$\forall z \in R: \map {\paren {y * I_{_R} } } z = y * \map {I_{_R}} z$
For all $y \in R$, let $I_{_R} * y : R \to R$ be the mapping defined by:
:$\forall z \in R: \map {\paren {I_{_R} * y}} z = \map {I_{_R}} z * y$
Theorem: Multiplicative Regular Representations of Units of Topological Ring are Homeomorphisms/Lemma 1

:$\forall y \in R: \lambda_y = y * I_{_R} \text { and } \rho_y = I_{_R} * y$

Proof:
Let $y \in R$.
{{begin-eqn}}
{{eqn | q = \forall z \in R
      | l = \map {\paren {y * I_{_R} } } z
      | r = y * \map {I_{_R} } z
      | c = Definition of $y * I_{_R}$
}}
{{eqn | r = y * z
      | c = {{Defof|Identity Mapping}} $I_{_R}$
}}
{{eqn | r = \map {\lambda_y} z
      | c = {{Defof|Left Regular Representation}} $\lambda_y$
}}
{{end-eqn}}
From Equality of Mappings:
:$\lambda_y = y * I_{_R}$
{{begin-eqn}}
{{eqn | q = \forall z \in R
      | l = \map {\paren {I_{_R} * y} } z
      | r = \map {I_{_R} } z * y
      | c = Definition of $I_{_R} * y$
}}
{{eqn | r = z * y
      | c = {{Defof|Identity Mapping}} $I_{_R}$
}}
{{eqn | r = \map {\rho_y} z
      | c = {{Defof|Right Regular Representation}} $\rho_y$
}}
{{end-eqn}}
From Equality of Mappings:
:$\rho_y = I_{_R} * y$
{{qed}}
Category:Multiplicative Regular Representations of Units of Topological Ring are Homeomorphisms
9kq73tknbz2yxbnyjv2muumocskpyh2
Theorem: Multiplicative Regular Representations of Units of Topological Ring are Homeomorphisms/Lemma 2

:$x * I_R$ is a bijection and $x^{-1} * I_R$ is the inverse of $x * I_R$
:$I_R * x$ is a bijection and $I_R * x^{-1}$ is the inverse of $I_R * x$

Proof:
Consider the composite of $x * I_R$ with $x^{-1} * I_R$.
{{begin-eqn}}
{{eqn | q = \forall y \in R
      | l = \map {\paren {\paren {x * I_R} \circ \paren {x^{-1} * I_R} } } y
      | r = \map {\paren {x * I_R} } {\map {\paren {x^{-1} * I_R} } y}
      | c = 
}}
{{eqn | r = \map {\paren {x * I_R} } {x^{-1} * y}
      | c = 
}}
{{eqn | r = x * \paren {x^{-1} * y}
      | c = 
}}
{{eqn | r = \paren {x * x^{-1} } * y
      | c = 
}}
{{eqn | r = y
      | c = 
}}
{{eqn | r = \map {I_R} y
      | c = 
}}
{{end-eqn}}
From Equality of Mappings, $\paren {x * I_R} \circ \paren {x^{-1} * I_R} = I_R$.
Consider the composite of $x^{-1} * I_R$ with $x * I_R$.
{{begin-eqn}}
{{eqn | q = \forall y \in R
      | l = \map {\paren {\paren {x^{-1} * I_R} \circ \paren {x * I_R} } } y
      | r = \map {\paren {x^{-1} * I_R} } {\map {\paren {x * I_R} } y}
      | c = 
}}
{{eqn | r = \map {\paren {x^{-1} * I_R} } {x * y}
      | c = 
}}
{{eqn | r = x^{-1} * \paren {x * y}
      | c = 
}}
{{eqn | r = \paren {x^{-1} * x} * y
      | c = 
}}
{{eqn | r = y
      | c = 
}}
{{eqn | r = \map {I_R} y
      | c = 
}}
{{end-eqn}}
From Equality of Mappings, $\paren {x^{-1} * I_R} \circ \paren {x * I_R} = I_R$.
Hence $x * I_R$ has a left inverse and a right inverse.
From definition 2 of bijection, $x * I_R$ is a bijection and the inverse is $x^{-1} * I_R$.
Similarly, $I_R * x$ is a bijection and the inverse is $I_R * x^{-1}$.
{{qed}}
Category:Multiplicative Regular Representations of Units of Topological Ring are Homeomorphisms
tm90xp65yum1x7wxoh07ib3vc4nptxw
Theorem: Open Balls of P-adic Number

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$, let $\map {B_\epsilon} a$ denote the open ball of $a$ of radius $\epsilon$. 
Then:
:$\forall n \in Z : \map {B_{p^{-n} } } a = a + p^{n + 1} \Z_p$

Proof:
Let $n \in \Z$.
From Open Ball in P-adic Numbers is Closed Ball:
:$\map {B_{p^{-n} } } a = \map {B^{\,-}_{p^{-\paren {n + 1} } } } a$
From Closed Balls of P-adic Number:
:$\map { B^{\,-}_{p^{-\paren {n + 1} } } } a = a + p^{n + 1} \Z_p$
The result follows.
{{qed}}
Theorem: Local Basis of P-adic Number

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Then the set of open balls $\set {\map {B_{p^{-n} } } a : n \in Z}$ is a local basis of $a$ consisting of clopen sets.

Proof:
Let $\BB_a$ be the set of all open balls of $Q_p$ centered on $a$.
That is:
:$\BB_a = \set{\map {B_\epsilon} a : \epsilon \in \R_{>0}}$
From Open Balls Centered on P-adic Number is Countable:
:$\BB_a = \set {\map {B_{p^{-n} } } a : n \in Z}$
From Open Balls form Local Basis for Point of Metric Space, $\BB_a$ is a local basis of $a$.
From P-adic Numbers form Non-Archimedean Valued Field:
:the $p$-adic numbers is a non-Archimedean division ring.
From Open Balls are Clopen In Non-Archimedean Division Ring:
:the set $\BB_a = \set {\map {B_{p^{-n} } } a : n \in \Z}$ is a local basis of clopen sets.
{{qed}}
Category:Topology of P-adic Numbers
kwn2boa5tgve0r09lpsvuhu827mf5wd
Theorem: Closed Ball of P-adic Number

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ denote the $p$-adic integers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$, let $\map { {B_\epsilon}^-} a$ denote the closed ball of $a$ of radius $\epsilon$. 
Then:
:$\forall n \in Z : \map {B^-_{p^{-n} } } a = a + p^n \Z_p$
where $a + p^n \Z_p$ denotes the left coset of the principal ideal $p^n \Z_p$ containing $a$ in the subring $\Z_p$.
That is, the closed ball $\map { {B_\epsilon}^-} a$ is the set:
:$a + p^n \Z_p = \set{a + p^n z : z \in \Z_p}$

Proof:
Let $n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \map {B^{\,-}_{p^{-n} } } a
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \norm {x - a}_p
      | o = \le
      | r = p^{-n}
      | c = {{Defof|Closed Ball in P-adic Numbers}}
}}
{{eqn | ll= \leadstoandfrom
      | l = p^n \norm {x - a}_p
      | o = \le
      | r = 1
      | c = Multiply both sides of equation by $p^n$
}}
{{eqn | ll= \leadstoandfrom
      | l = \norm {p^{-n} }_p \norm {x - a}_p
      | o = \le
      | r = 1
      | c = {{Defof|P-adic Norm|$p$-adic norm}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \norm {p^{-n} \paren {x - a} }_p
      | o = \le
      | r = 1
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | ll= \leadstoandfrom
      | l = p^{-n} \paren {x - a}
      | o = \in
      | r = \Z_p
      | c = {{Defof|P-adic Integer|$p$-adic integers}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x - a
      | o = \in
      | r = p^n \Z_p
      | c = {{Defof|Principal Ideal}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = a + p^n \Z_p
      | c = {{Defof|Left Coset}}
}}
{{end-eqn}}
From set equality:
:$\map {B^-_{p^{-n} } } a = a + p^n \Z_p$
The result follows.
{{qed}}
Theorem: Closed Ball is Disjoint Union of Open Balls in P-adic Numbers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$:
:let $\map { {B_\epsilon}^-} a$ denote the closed $\epsilon$-ball of $a$
and:
:let $\map {B_\epsilon} a$ denote the open $\epsilon$-ball of $a$. 
Then:
:$(1): \quad \forall n \in Z : \map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p - 1} \map {B_{p^{-n} } } {a + i p^n}$
:$(2): \quad \forall n \in Z : \set {\map {B_{p^{-n} } } {a + i p^n} : i = 0, \dotsc, p - 1}$ is a set of pairwise disjoint open balls.

Proof:
Let $n \in \Z$.
From Closed Ball is Disjoint Union of Smaller Closed Balls in P-adic Numbers:
:$\map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p - 1} \map {B^-_{p^{-\paren {n + 1} } } } {a + i p}$
where $\set {\map {B^-_{p^{-\paren {n + 1 } } } } {a + i p^n} : i = 0, \dots, p - 1}$ is a set of pairwise disjoint closed balls.
From Open Ball in P-adic Numbers is Closed Ball:
:$\map {B^-_{p^{-n} } } a = \ds \bigcup_{i \mathop = 0}^{p - 1} \map {B_{p^{-n} } } {a + i p}$
where $\set {\map {B_{p^{-n} } } {a + i p^n} : i = 0, \dots, p - 1}$ is a set of pairwise disjoint Open balls.
The result follows.
{{qed}}
Theorem: Sphere is Disjoint Union of Open Balls in P-adic Numbers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $a \in \Q_p$.
For all $\epsilon \in \R_{>0}$:
:let $\map {S_\epsilon} a$ denote the sphere of $a$ of radius $\epsilon$. 
:let $\map {B_\epsilon} a$ denote the open ball of $a$ of radius $\epsilon$. 
Then:
:$\ds \forall n \in Z: \map {S_{p^{-n} } } a = \bigcup_{i \mathop = 1}^{p - 1} \map {B_{p^{-n} } } {a + i p^n}$

Proof:
For all $\epsilon \in \R_{>0}$:
:let $\map {B^-_\epsilon} a$ denote the closed ball of $a$ of radius $\epsilon$. 
Let $n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = \map {S_{p^{-n} } } a
      | r = \map {B^-_{p^{-n} } } a \setminus \map {B_{p^{-n} } } a
      | c = Sphere is Set Difference of Closed and Open Ball in P-adic Numbers
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 0}^{p - 1} \map {B_{p^{-n} } } {a + i p^n} } \setminus \map {B_{p^{-n} } } a
      | c = Closed Ball is Disjoint Union of Open Balls in P-adic Numbers
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^{p - 1} \map {B_{p^{-n} } } {a + i p^n} \cup \map {B_{p^{-n} } } {a + 0 \cdot p^n} } \setminus \map {B_{p^{-n} } } a
      | c = Union is Associative and commutative
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^{p - 1} \map {B_{p^{-n} } } {a + i p^n} \cup \map {B_{p^{-n} } } a } \setminus \map {B_{p^{-n} } } a
      | c = $a + 0 \cdot p^n = a$
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^{p-1} \map {B_{p^{-n} } } {a + i p^n} } \setminus \map {B_{p^{-n} } } a
      | c = Set Difference with Union is Set Difference
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{p - 1} \paren {\map {B_{p^{-n} } } {a + i p^n} \setminus \map {B_{p^{-n} } } a }
      | c = Set Difference is Right Distributive over Union
}}
{{end-eqn}}
From Closed Ball is Disjoint Union of Open Balls in P-adic Numbers:
:$\set {\map {B_{p^{-n} } } {a + i p^n}: i = 0, \dots, p - 1}$ is a set of pairwise disjoint open balls.
Continuing from above:
{{begin-eqn}}
{{eqn | l = \map {S_{p^{-n} } } a
      | r = \bigcup_{i \mathop = 1}^{p - 1} \paren {\map {B_{p^{-n} } } {a + i p^n} \setminus \map {B_{p^{-n} } } a}
      | c = 
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{p - 1} \map {B_{p^{-n} } } {a + i p^n} 
      | c = Set Difference with Disjoint Set
}}
{{end-eqn}}
{{qed}}
Theorem: Null Sequence induces Local Basis in Metric Space

Let $M = \struct {A, d}$ be a metric space.
Let $a \in A$.
Let $\sequence {x_n}$ be a real null sequence such that:
:$\forall n \in N: x_n > 0$
Let $\map {B_\epsilon} a$ denote the open $\epsilon$-ball of $a$ in $M$.
Then:
:$\BB_{\sequence {x_n} } = \set{\map {B_{x_n} } a : n \in \N}$ is a local basis at $a$.

Proof:
By Open Ball of Metric Space is Open Set, every element of $\BB_{\sequence {x_n} }$ is an open neighborhood of $a$.
Let $U$ be an open neighborhood of $a$.
By definition of an open set, there exists a strictly positive real number $\epsilon$ such that $\map {B_\epsilon} a \subseteq U$.
By definition of a real null sequence:
:$\exists N \in \N : \forall n > N : \size {x_n} < \epsilon$
Let $m = N + 1$.
Then $\size {x_m} < \epsilon$.
Since $x_m > 0$ then $x_m = \size {x_m} < \epsilon$, and so $\map {B_{x_m} } a \subseteq \map {B_\epsilon} a \subseteq U$.
The result follows from Subset Relation is Transitive.
{{qed}}
Category:Metric Spaces
bkp1g2uwp87xu11028c4digkjdvk29e
Theorem: Null Sequence induces Local Basis in Metric Space/Sequence of Reciprocals

:$\BB = \set {\map {B_{1/n}} a : n \in \N}$ is a local basis at $a$.

Proof:
Let $\sequence {x_n}$ be the sequence in $\R$ defined as:
:$x_n = \dfrac 1 n$
From Sequence of Reciprocals is Null Sequence, $\sequence {x_n}$ is a real null sequence.
From Null Sequence induces Local Basis in Metric Space:
:$\BB = \set {\map {B_{1/n} } a : n \in \N}$ is a local basis at $a$.
{{qed}}
Category:Metric Spaces
izl7o4tyt1w48tu1kgy49jpo3j5huj2
Theorem: Consecutive Integers which are Powers of 2 or 3

The only pairs of consecutive positive integers which are powers of $2$ or $3$ are:
:$\tuple {1, 2}$, $\tuple {2, 3}$, $\tuple {3, 4}$, $\tuple {8, 9}$

Proof:
Let $a$ and $b$ be two arbitrary consecutive positive integers.
Theorem: Kinetic Energy of Classical Particle

Let $\MM$ be an $n$-dimensional Euclidean manifold.
Let $P$ be a particle with an inertial mass $m_i$.
Let $t$ be the time variable of $P$.
Suppose the position of $P$ is a real differentiable $n$-dimensional vector-valued mapping $\mathbf x = \map {\mathbf x} t$.
Then the '''kinetic energy''' of a '''classical particle''' $P$ is:
:$T = \dfrac {m_i} 2 \paren {\dfrac {\d \mathbf x} {\d t} }^2$
where $\paren {\dfrac {\d \mathbf x} {\d t} }^2$ is the dot product of the vector $\dfrac {\d \mathbf x} {\d t}$ with itself.

Proof:
{{ProofWanted|dependent upon the axiomatic framework}}