avewright/proofwiki-math huggingface dataset:
Theorem: Continuity Test for Real-Valued Functions/Everywhere Continuous

Let $\struct{S, \tau}$ be a topological space.
Let $f: S \to \R$ be a real-valued function.
Then $f$ is everywhere continuous {{iff}}:
:$\forall x \in S : \forall \epsilon \in \R_{>0} : \exists U \in \tau : x \in U : \map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$

Proof:
By definition, $f$ is everywhere continuous {{iff}} $f$ is continuous at every point $x \in S$.
From Continuity Test for Real-Valued Functions, $f$ is continuous at every point $x \in S$ {{iff}}:
:$\forall x \in S : \forall \epsilon \in \R_{>0} : \exists U \in \tau : x \in U : \map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$
{{qed}}
Category:Continuity Test for Real-Valued Functions
bb6rmo9cdjehak1ju8nm3if157p2jru
Theorem: Definite Integral of Fourier Series at Ends of Interval

Let $f: \R \to \R$ be a real function defined in the open interval $\openint {-\pi} \pi$.
Let $f$ fulfil the Dirichlet conditions in $\openint {-\pi} \pi$.
Let $a_0, a_1, \dotsc; b_1, \dotsc$ be the Fourier coefficients of $f$ in $\openint {-\pi} \pi$.
Consider the real function:
:$\map F x = \ds \int_{-\pi}^x \map f t \rd t - \dfrac {a_0} 2 x$
Then:
:$\map F \pi = \map F {-\pi} = \dfrac {a_0 \pi} 2$

Proof:
From Definite Integral on Zero Interval:
{{begin-eqn}}
{{eqn | l = \map F {-\pi}
      | r = \int_{-\pi}^{-\pi} \map f t \rd t - \dfrac {a_0} 2 \paren {-\pi}
      | c = 
}}
{{eqn | r = 0 - \dfrac {a_0} 2 \paren {-\pi}
      | c = 
}}
{{eqn | r = \dfrac {a_0 \pi} 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map F \pi
      | r = \int_{-\pi}^\pi \map f t \rd t - \dfrac {a_0} 2 \pi
      | c = 
}}
{{eqn | r = \int_{-\pi}^\pi \paren {\dfrac {\map {f^+} t + \map {f^-} t} 2} \rd t - \dfrac {a_0} 2 \pi
      | c = Fourier's Theorem
}}
{{end-eqn}}
{{finish}}
Theorem: Group/Examples/x+y over 1+xy/Isomorphic to Real Numbers/Proof 1

Let $G := \set {x \in \R: -1 < x < 1}$ be the set of all real numbers whose absolute value is less than $1$.
Let $\circ: G \times G \to G$ be the binary operation defined as:
:$\forall x, y \in G: x \circ y = \dfrac {x + y} {1 + x y}$
{{:Group/Examples/x+y over 1+xy/Isomorphic to Real Numbers}}

Proof:
To prove $G$ is isomorphic to $\struct {\R, +}$, we need to find a bijective homorphism $\phi: \openint {-1} 1 \to \R$:
:$\forall x, y \in G: \map \phi {x \circ y} = \map \phi x + \map \phi y$
From Group Examples: $\dfrac {x + y} {1 + x y}$:
:the identity element of $G$ is $0$
:the inverse of $x$ in $G$ is $-x$.
This also holds for $\struct {\R, +}$.
This hints at the structure of a possible isomorphism, namely:
:$(1): \quad$ that it is an odd function
:$(2): \quad$ that it passes through $0$
:$(3): \quad$ that it is defined on the open interval $\openint {-1} 1$.
One such function is the inverse hyperbolic arctangent function $\tanh^{-1}$, which is indeed defined on $\openint {-1} 1$ and has the above properties.
Hence:
{{begin-eqn}}
{{eqn | l = \map {\tanh^{-1} } x
      | r = \frac 1 2 \map \ln {\frac {x + 1} {x - 1} }
      | c = {{Defof|Inverse Hyperbolic Tangent|subdef = Real|index = 2}}
}}
{{eqn | ll= \leadsto
      | l = \map {\tanh^{-1} } {x \circ y}
      | r = \frac 1 2 \map \ln {\frac {\frac {x + y} {1 + x y} + 1} {\frac {x + y} {1 + x y} - 1} }
      | c = Definition of $\struct {G, \circ}$
}}
{{eqn | r = \frac 1 2 \map \ln {\frac {x + y + 1 + x y} {x + y - 1 - x y} }
      | c = 
}}
{{eqn | r = \frac 1 2 \map \ln {\frac {\paren {x + 1} \paren {y + 1} } {\paren {x - 1} \paren {y - 1} } }
      | c = 
}}
{{eqn | r = \frac 1 2 \map \ln {\frac {x + 1} {x - 1} } + \frac 1 2 \map \ln {\frac {y + 1} {y - 1} }
      | c = 
}}
{{eqn | r = \tanh^{-1} x + \tanh^{-1} y
      | c = 
}}
{{end-eqn}}
This demonstrates the homorphism between $\struct {G, \circ}$ and $\struct {\R,  +}$.
We have that Real Inverse Hyperbolic Tangent Function is Strictly Increasing over $\openint {-1} 1$.
Hence from Strictly Monotone Real Function is Bijective, $\tanh^{-1}: \openint {-1} 1 \to \R$ is a bijection.
Hence the result that $\struct {G, \circ} \cong \struct {\R,  +}$.
{{Qed}}
Theorem: Group/Examples/x+y over 1+xy/Isomorphic to Real Numbers/Proof 2

Let $G := \set {x \in \R: -1 < x < 1}$ be the set of all real numbers whose absolute value is less than $1$.
Let $\circ: G \times G \to G$ be the binary operation defined as:
:$\forall x, y \in G: x \circ y = \dfrac {x + y} {1 + x y}$
{{:Group/Examples/x+y over 1+xy/Isomorphic to Real Numbers}}

Proof:
To prove $G$ is isomorphic to $\struct {\R, +}$, it is sufficient to find a bijective homorphism $\phi: \to \R \to G$:
:$\forall x, y \in G: \map \phi {x + y} = \map \phi x \circ \map \phi y$
From Group Examples: $\dfrac {x + y} {1 + x y}$:
:the identity element of $G$ is $0$
:the inverse of $x$ in $G$ is $-x$.
This also holds for $\struct {\R, +}$.
This hints at the structure of a possible such $\phi$:
:$(1): \quad$ that it is an odd function
:$(2): \quad$ that it passes through $0$
:$(3): \quad$ that its image is the open interval $\openint {-1} 1$.
One such function is the hyperbolic tangent function $\tanh$, which indeed has the above properties on $\R$.
Then we have that:
{{begin-eqn}}
{{eqn | l = \map {\tanh } {x + y}
      | r = \dfrac {\tanh x + \tanh y} {1 + \tanh x \tanh y}
      | c = Hyperbolic Tangent of Sum
}}
{{eqn | r = \tanh x \circ \tanh y
      | c = 
}}
{{end-eqn}}
This demonstrates the homorphism between $\struct {\R,  +}$ and $\struct {G, \circ}$.
We have that Real Hyperbolic Tangent Function is Strictly Increasing over $\R$.
Hence from Strictly Monotone Real Function is Bijective, $\tanh: \R \to \openint {-1} 1$ is a bijection.
Hence the result that $\struct {\R,  +} \cong \struct {G, \circ}$.
{{Qed}}
Theorem: Triangle Inequality for Complex Numbers/Corollary 2

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ be the modulus of $z$.
Then:
:$\cmod {z_1 + z_2} \ge \cmod {\cmod {z_1} - \cmod {z_2} }$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 + z_2}
      | o = \ge
      | r = \cmod {z_1} - \cmod {z_2}
      | c = {{Corollary|Triangle Inequality for Complex Numbers|1}}
}}
{{eqn | l = \cmod {z_1 + z_2}
      | o = \ge
      | r = \cmod {z_2} - \cmod {z_1}
      | c = {{Corollary|Triangle Inequality for Complex Numbers|1}}
}}
{{eqn | r = -\paren {\cmod {z_1} - \cmod {z_2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {z_1 + z_2}
      | o = \ge
      | r = \cmod {\cmod {z_1} - \cmod {z_2} }
      | c = {{Corollary|Negative of Absolute Value|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Continuity Test for Real-Valued Functions/Necessary Condition

Let $\struct {S, \tau}$ be a topological space.
Let $f: S \to \R$ be a real-valued function.
Let $x \in S$.
Let $f$ be continuous at $x$
Then:
:$\forall \epsilon \in \R_{>0} : \exists U \in \tau : x \in U : \map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$

Proof:
Let $f$ be continuous at $x$.
Then by definition:
:For every neighborhood $N$ of $\map f x$ in $\R$, there exists a neighborhood $M$ of $x$ in $S$ such that $\map {f^\to} M \subseteq N$.
From:
:Open Ball in Real Number Line is Open Interval
:Open Ball of Metric Space is Open Set
:Set is Open iff Neighborhood of all its Points 
it follows that:
:For every $\epsilon \in \R_{>0}$, there exists a neighborhood $M$ of $x$ in $S$ such that $\map {f^\to} M \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$
By definition of a neighborhood in $\struct {S, \tau}$:
:for all neighborhoods $M$ there exists $U \in \tau$ such that $z \in U \subseteq M$
Thus:
:For every $\epsilon \in \R_{>0}$, there exists $U \in \tau$ with $x \in U$ such that $\map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$
Theorem: Continuity Test for Real-Valued Functions/Sufficient Condition

Let $\struct {S, \tau}$ be a topological space.
Let $f: S \to \R$ be a real-valued function.
Let $x \in S$.
Let $f$ satisfy:
:$\forall \epsilon \in \R_{>0} : \exists U \in \tau : x \in U : \map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$
Then $f$ is continuous at $x$

Proof:
Let $f$ satisfy:
:$\forall \epsilon \in \R_{>0} : \exists U \in \tau : x \in U : \map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$
Let $N$ be a neighborhood of $\map f x$.
By definition of a neighborhood of $\map f x$:
:there exists $U$ such that $z \in U \subseteq N$
By definition of the topology induced by the Euclidean Metric on Real Number Line:
:there exists an open $\epsilon$-ball $\map {B_\epsilon} {\map f x}$ such that $x \in \map {B_\epsilon} {\map f x} \subseteq U$
From Open Ball in Real Number Line is Open Interval:
:$\map {B_\epsilon} {\map f x} = \openint {\map f x - \epsilon} {\map f x + \epsilon}$
Thus:
:$\exists U \in \tau : x \in U : \map {f^\to} U \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$
From Set is Open iff Neighborhood of all its Points, $U$ is a neighborhood of $x$.
Since $N$ was an arbitrary neighborhood of $\map f x$ it follows that $f$ is continuous at $x$.
Theorem: Max is Half of Sum Plus Absolute Difference

For all numbers $a, b$ where $a, b$ in $\N, \Z, \Q$ or $\R$:
:$\max \set {a, b} = \dfrac 1 2 \paren {a + b + \size {a - b} }$

Proof:
From the Trichotomy Law for Real Numbers exactly one of the following holds:
{{begin-itemize}}
{{item||$x < y$ and so $\max \set {x, y} {{=}} y$}}
{{item||$x {{=}} y$ and so $\max \set {x, y} {{=}} x {{=}} y$}}
{{item||$y < x$ and so $\max \set {x, y} {{=}} x$}}
{{end-itemize}}
By the definition of the absolute value function for each case respectively we have:
{{begin-eqn}}
{{eqn | l = \size {x - y}
      | r = y - x
}}
{{eqn | l = \size {x - y}
      | r = 0
}}
{{eqn | l = \size {x - y}
      | r = x - y
}}
{{end-eqn}}
Thus the equation holds by $+$ being commutative and associative as for each case:
{{begin-eqn}}
{{eqn | l = \dfrac 1 2 \paren {x + y + y - x}
      | r = y
      | c = 
}}
{{eqn | l = \dfrac 1 2 \paren {x + y + 0}
      | r = x = y
      | c = 
}}
{{eqn | l = \dfrac 1 2 \paren {x + y + x - y}
      | r = x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Maximum Rule for Continuous Functions

Let $\struct {S, \tau}$ be a topological space.
Let $f, g: S \to \R$ be continuous real-valued functions.
Let $\max \set {f, g}: S \to \R$ denote the pointwise maximum of $f$ and $g$.
Then:
:$\max \set {f, g}$ is continuous.

Proof:
From Sum Less Minimum is Maximum:
:$\forall x \in S : \max \set {\map f x, \map g x} = \map f x + \map g x - \min \set {\map f x, \map g x}$
Thus: 
:$\max \set {f, g} = f + g - \min \set{f, g}$
From Minimum Rule for Continuous Functions:
:$\min \set {f, g}$ is continuous
From Multiple Rule for Continuous Mappings into Topological Ring:
:$-\min \set {f, g}$ is continuous 
From Sum Rule for Continuous Mappings into Topological Ring:
:$f + g - \min \set {f, g}$ is continuous 
Thus:
:$\max \set {f, g}$ is continuous 
{{qed}}
Theorem: Equivalence of Definitions of T2.5 Space

{{TFAE|def = T2.5 Space|view = a $T_{2 \frac 1 2}$ space}}
Let $T = \struct {S, \tau}$ be a topological space.

Proof:
=== Definition 1 implies Definition 2 ===
Let $\struct {S, \tau}$ satisfy:
:$\forall x, y \in S, x \ne y: \exists U, V \in \tau: x \in U, y \in V: U^- \cap V^- = \O$ 
Let $x, y \subseteq S , x \ne y $ be arbitrary.
Then:
:$\exists U, V \in \tau: x \in U, y \in V: U^- \cap V^- = \O$ 
Let $N_x = U$ and $N_y = V$.
From Set is Subset of Itself then:
:$\exists N_x, N_y \subseteq S: \exists U, V \in \tau: x \in U \subseteq N_x, y \in V \subseteq N_y: N_x^- \cap N_y^- = \O$
Because $x, y \in S$ were arbitrary:
:$\forall x, y \in S, x \ne y : \exists N_x, N_y \subseteq S: \exists U, V \in \tau: x \subseteq U \subseteq N_x, y \subseteq V \subseteq N_y: N_x^- \cap N_y^- = \O$
{{qed|lemma}}
Theorem: Product Space is T2.5 iff Factor Spaces are T2.5/Sufficient Condition

Let $\SS = \family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an indexed family of non-empty topological spaces for $\alpha$ in some indexing set $I$.
Let $\ds T = \struct {S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\SS$.
Let $T$ be a $T_{2 \frac 1 2}$ space.
Then for each $\alpha \in I$, $\struct {S_\alpha, \tau_\alpha}$ is a $T_{2 \frac 1 2}$ space.

Proof:
Let $T$ be a $T_{2 \frac 1 2}$ space.
As $S_\alpha \ne \O$ we also have $S \ne \O$ by the axiom of choice.
Let $\alpha \in I$.
From Subspace of Product Space is Homeomorphic to Factor Space, $\struct {S_\alpha, \tau_\alpha}$ is homeomorphic to a subspace $T_\alpha$ of $T$.
From $T_{2 \frac 1 2}$ property is hereditary, $T_\alpha$ is a $T_{2 \frac 1 2}$ space.
From $T_{2 \frac 1 2}$ Property is Preserved under Homeomorphism, $\struct {S_\alpha, \tau_\alpha}$ is a $T_{2 \frac 1 2}$ space.
As $\alpha \in I$ was arbitrary, it follows that each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_{2 \frac 1 2}$ space.
Theorem: Metric Space is T4

A metric space $M = \struct {A, d}$ is a $T_4$ space.

Proof:
Let $H$ and $K$ be disjoint closed sets of $M$.
Let $g: A \to \R$ be defined as:
:$g = f_K - f_H$
where:
:$\forall x \in A: \map {f_K} x = \map d {x, K}$
:$\forall x \in A: \map {f_H} x = \map d {x, H}$
where $\map d {x, K}$, $\map d {x, H}$ denotes the distance from $x$ to $K$ and from $x$ to $H$ respectively.
From Distance from Point to Subset is Continuous Function, both $\map {f_K} x$ and $\map {f_H} x$ are continuous mappings.
Hence $g$ itself is a continuous mapping.
Consider the disjoint open intervals $\openint 0 \to$ and $\openint \gets 0$.
Because $g$ is continuous, it follows that $g^{-1} \sqbrk {\openint 0 \to}$ and $g^{-1} \sqbrk {\openint \gets 0}$ are open in $M$ and disjoint.
Let $x \in H$.
Then:
:$\map {f_H} x = 0$
Because $H$ and $K$ are disjoint:
:$H \cap K = \O$
and so:
:$x \notin K$
Because $K$ is closed sets in $M$, it follows from Point at Distance Zero from Closed Set is Element that:
:$\map {f_K} x > 0$
It follows that:
:$\map g x > 0$
that is:
:$H \subseteq g^{-1} \sqbrk {\openint 0 \to}$
Similarly:
:$K \subseteq g^{-1} \sqbrk {\openint \gets 0}$
The result follows.
{{qed}}
Theorem: Metric Space is T4

A metric space $M = \struct {A, d}$ is a $T_4$ space.

Proof:
We have that a metric space is fully $T_4$.
Then we have that a fully $T_4$ space is $T_4$.
{{qed}}
Theorem: Product Space is T2.5 iff Factor Spaces are T2.5/Necessary Condition

Let $\SS = \family {\struct {S_\alpha, \tau_\alpha} }$ be an indexed family of non-empty topological spaces for $\alpha$ in some indexing set $I$.
Let $\ds T = \struct {S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\SS$.
Let each of $\struct {S_\alpha, \tau_\alpha}$ for $\alpha \in I$ be a $T_{2 \frac 1 2}$ space.
Then $T$ is a $T_{2 \frac 1 2}$ space.

Proof:
Let each of $\struct {S_\alpha, \tau_\alpha}$ for $\alpha \in I$ be a $T_{2 \frac 1 2}$ space.
Let $x, y \in S : x \ne y$ be arbitrary.
Then $x_\alpha \ne y_\alpha$ for some $\alpha \in I$.
Since $\struct {S_\alpha, \tau_\alpha}$ is a $T_{2 \frac 1 2}$ space then:
:$\exists U, V \in \tau_\alpha: x_\alpha \in U, y_\alpha \in V : U^- \cap V^- = \O$
Let $\pr_\alpha: S \to S_\alpha$ be the projection of $S$ to $S_\alpha$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\pr_\alpha^\gets} {U^-} \cap \map {\pr_\alpha^\gets} {V^-}
      | r = \map {\pr_\alpha^\gets} {U^- \cap V^-}
      | c = Preimage of Intersection under Mapping
}}
{{eqn | r = \map {\pr_\alpha^\gets} \O
}}
{{eqn | r = \O
}}
{{end-eqn}} 
From Preimage of Subset is Subset of Preimage:
:$\map {\pr_\alpha^\gets} U \subseteq \map {\pr_\alpha^\gets} {U^-}$
and
:$\map {\pr_\alpha^\gets} V \subseteq \map {\pr_\alpha^\gets} {V^-}$
From Projection from Product Topology is Open and Continuous:General Result
:$\pr_\alpha: S \to S_\alpha$ is continuous.
From Continuity Defined from Closed Sets:
:$\map {\pr_\alpha^\gets} {U^-}, \map {\pr_\alpha^\gets} {V^-}$ are closed in $T$
From Set Closure is Smallest Closed Set in Topological Space:
:$\paren {\map {\pr_\alpha^\gets} U}^- \subseteq \map {\pr_\alpha^\gets} {U^-}$
and
:$\paren {\map {\pr_\alpha^\gets} V}^- \subseteq \map {\pr_\alpha^\gets} {V^-}$
From Subsets of Disjoint Sets are Disjoint:
:$\paren {\map {\pr_\alpha^\gets} U}^- \cap \paren {\map {\pr_\alpha^\gets} V}^- = \O$
By definition of the projection $\pr_\alpha$:
:$\map {\pr_\alpha} x = x_\alpha \in U$
By definition of the preimage under $\pr_\alpha$:
:$x \in \map {\pr_\alpha^\gets} U$
Similarly:
:$y \in \map {\pr_\alpha^\gets} V$
By definition of the product topology $\tau$:
:$\map {\pr_\alpha^\gets} U, \map {\pr_\alpha^\gets} V \in \tau$
As $x, y \in S$ were arbitrary, it follows that $T$ is a $T_{2 \frac 1 2}$ space by definition.
Theorem: P-adic Expansion Less Initial Zero Terms Represents Same P-adic Number

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a$ be a $p$-adic number, that is left coset, in $\Q_p$.
Let $\ds \sum_{i \mathop = m}^\infty d_i p^i$ be a $p$-adic expansion that represents $a$.
Let $l$ be the first index $i \ge m$ such that $d_i \ne 0$
Then the series:
:$\ds \sum_{i \mathop = l}^\infty d_i p^i$
also represents $a$.

Proof:
Let $\sequence {\alpha_n}$ be the sequence of partial sums:
:$\ds \forall n \in \N: \alpha _n = \sum_{i \mathop = 0}^n d_{n + m} p^{n + m}$
Let $\sequence {\beta_n}$ be the sequence of partial sums:
:$\ds \forall n \in \N: \beta _n = \sum_{i \mathop = 0}^n d_{n + l} p^{n + l}$
Then:
{{begin-eqn}}
{{eqn | l = \beta_n
      | r = \sum_{i \mathop = 0}^n d_{n + l} p^{n + l}
}}
{{eqn | r = \sum_{i \mathop = l}^{n + l} d_n p^n
}}
{{eqn | r = \sum_{i \mathop = m}^{l - 1} d_n p^n  +  \sum_{i \mathop = l}^{n + l} d_n p^n
}}
{{eqn | r = \sum_{i \mathop = m}^{n + l} d_n p^n
}}
{{eqn | r = \sum_{i \mathop = 0}^{n + l - m} d_{n + m} p^{n + m}
}}
{{eqn | r = \alpha_{n + l - m}
}}
{{end-eqn}}
By definition of $l$:
:$m \le l$
So:
:$\forall n \in \N : n + l - m \ge n$
Thus $\sequence {\beta_n}$ is a subsequence of $\sequence {\alpha_n}$ by definition.
From Subsequence of Cauchy Sequence in Normed Division Ring is Cauchy Sequence:
:$\ds \sum_{i \mathop = l}^\infty d_i p^i$ is a Cauchy Sequence in $\Q$.
From Subsequence is Equivalent to Cauchy Sequence:
:$\ds \lim_{n \mathop \to \infty} {\alpha_n - \beta_n} = 0$
That is, the sequence $\sequence {\alpha_n - \beta_n}$ is a null sequence.
By definition of $p$-adic number:
:$\sequence {\alpha_n}$ and $\sequence {\beta_n}$ represent the same $p$-adic number
Since $\sequence {\alpha_n}$ represents $a$, it follows that $\sequence {\beta_n}$ represents $a$.
{{qed}}
Category:P-adic Number Theory
q8g14tjzyqbnazwksini1n08d19bokk
Theorem: Subsequence is Equivalent to Cauchy Sequence

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\sequence {x_n}$ be a Cauchy sequence in $R$.
Let $\sequence {x_{m_n} }$ be a subsequence of $\sequence {x_n}$.
Then:
:$\ds \lim_{n \mathop \to \infty} {x_n - x_{m_n} } = 0$

Proof:
From Subsequence of Cauchy Sequence in Normed Division Ring is Cauchy Sequence:
:$\sequence {x_{m_n} }$ is a Cauchy sequence
Let $\epsilon > 0$.
By definition of a Cauchy sequence:
:$\exists N: \forall n, m > N: \norm {x_n - x_m } < \epsilon$
From Index of Subsequence not Less than its Index:
$\forall n \in \N : m_n \ge n$
Thus:
:$\exists N: \forall n > N: \norm {x_n - x_{m_n} } < \epsilon$
By definition of convergence:
:$\ds \lim_{n \mathop \to \infty} {x_n - x_{m_n} } = 0$
{{qed}}
Category:Cauchy Sequences
Category:Normed Division Rings
p0yekvz773c82fjska54il4vag3np2u
Theorem: Derivative of Generating Function/General Result/Corollary

Let the coefficient of $z^n$ extracted from $\map G z$ be denoted:
:$\sqbrk {z^n} \map G z := a_n$
Then:
:$\sqbrk {z^m} \map G z = \dfrac 1 {m!} \map {G^{\paren m} } 0$
where $G^{\paren m}$ denotes the $m$th derivative of $G$.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^m} {\d z^m} \map G z 
      | r = \sum_{k \mathop \ge 0} \dfrac {\paren {k + m}!} {k!} a_{k + m} z^k
      | c = Derivative of Generating Function: General Result
}}
{{eqn | r = \dfrac {m!} {0!} a_m + \sum_{k \mathop \ge 1} \dfrac {\paren {k + m}!} {k!} a_{k + m} z^k
      | c = 
}}
{{eqn | r = m! a_m + \sum_{k \mathop \ge 1} \dfrac {\paren {k + m}!} {k!} a_{k + m} z^k
      | c = Factorial of Zero
}}
{{eqn | ll= \leadsto
      | l = \map {G^{\paren m} } 0
      | r = m! a_m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 {m!} \map {G^{\paren m} } 0
      | r = a_m
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Generating Functions
olu9mfz3kbo57heaq3f4n6sybnxawtz
Theorem: Derivative of Generating Function/General Result

Let $m$ be a positive integer.
Then:
:$\ds \dfrac {\d^m} {\d z^m} \map G z = \sum_{k \mathop \ge 0} \dfrac {\paren {k + m}!} {k!} a_{k + m} z^k$
=== Corollary ===
{{:Derivative of Generating Function/General Result/Corollary}}

Proof:
Proof by induction:
Theorem: D'Alembert's Formula

Let $t$ be time.
Let $x$ be position.
Let $\tuple {t, x} \stackrel u {\longrightarrow} \map u {t, x}: \R^2 \to \R$ be a twice-differentiable function in both variables. 
Let $x \stackrel \phi {\longrightarrow} \map \phi x: \R \to \R$ be a differentiable function. 
Let $x \stackrel \psi {\longrightarrow} \map \psi x: \R \to \R$ be a Riemann integrable function.
Let $c \in \R_{> 0}$ be a constant.
Then the solution to the partial differential equation:
:$\dfrac {\partial^2} {\partial t^2} \map u {x, t} = c^2 \dfrac {\partial^2} {\partial x^2} \map u {x, t}$
with initial conditions:
{{begin-eqn}}
{{eqn | l = \map u {x, 0}
      | r = \map \phi x
}}
{{eqn | l = \valueat {\dfrac {\partial} {\partial t} \map u {x, t} } {t \mathop = 0}
      | r = \map \psi x
}}
{{end-eqn}}
is given by:
:$\ds \map u {x, t} = \dfrac 1 2 \paren {\map \phi {x + c t} + \map \phi {x - c t} } + \dfrac 1 {2 c} \int_{x - c t}^{x + c t} \map \psi s \rd s$
The above solution formula is called '''d'Alembert's formula'''.

Proof:
The general solution to the $1$-D wave equation:
:$\dfrac {\partial^2} {\partial t^2} \map u {x, t} = c^2 \dfrac {\partial^2} {\partial x^2} \map u {x, t}$
is given by:
:$\map u {x, t} = \map f {x + c t} + \map g {x - c t}$
where $f, g$ are arbitrary twice-differentiable functions.
From initial conditions we have:
{{begin-eqn}}
{{eqn | l = \map \phi x
      | m = \map u {x, 0}
      | mo= = 
      | r = \map f x + \map g x
}}
{{eqn | l = \map \psi x
      | m = \valueat {\dfrac \partial {\partial t} \map u {x, t} } {t \mathop = 0}
      | mo= =
      | r = c \map {f'} x - c \map {g'} x
      | c = Chain Rule for Partial Derivatives
}}
{{end-eqn}}
So we have:
{{begin-eqn}}
{{eqn | l = \map {\phi'} x
      | r = \map {f'} x + \map {g'} x
      | c = Sum Rule for Derivatives
}}
{{eqn | l = \dfrac {\map \psi x} c
      | r = \map {f'} x - \map {g'} x
}}
{{end-eqn}}
Solving the equations give:
{{begin-eqn}}
{{eqn | l = \map {f'} x
      | r = \dfrac 1 2 \paren {\map {\phi'} x + \dfrac {\map \psi x} c}
}}
{{eqn | l = \map {g'} x
      | r = \dfrac 1 2 \paren {\map {\phi'} x - \dfrac {\map \psi x} c}
}}
{{end-eqn}}
Integrating both equations and using Fundamental Theorem of Calculus:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \dfrac 1 2 \map \phi x + \dfrac 1 {2 c} \int_0^x \map \psi s \rd s + A
}}
{{eqn | l = \map g x
      | r = \dfrac 1 2 \map \phi x - \dfrac 1 {2 c} \int_0^x \map \psi s \rd s + B
}}
{{end-eqn}}
for some constants $A, B$.
From $\map \phi x = \map f x + \map g x$, we have $A + B = 0$. 
Therefore:
{{begin-eqn}}
{{eqn | l = \map u {x, t}
      | r = \map f {x + c t} + \map g {x - c t}
}}
{{eqn | r = \dfrac 1 2 \map \phi {x + c t} + \dfrac 1 {2 c} \int_0^{x + c t} \map \psi s \rd s + A + \dfrac 1 2 \map \phi {x - c t} - \dfrac 1 {2 c} \int_0^{x - c t} \map \psi s \rd s + B
      | c = substitution
}}
{{eqn | r = \dfrac 1 2 \paren {\map \phi {x + c t} + \map \phi {x - c t} } + \dfrac 1 {2 c} \int_{x - c t}^{x + c t} \map \psi s \rd s
      | c = simplification
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Jean le Rond d'Alembert|cat = d'Alembert}}