avewright/proofwiki-math huggingface dataset:
Theorem: Product Space is T3 iff Factor Spaces are T3/Necessary Condition

Let $\mathbb S = \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} = \ds \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\mathbb S$.
For each $\alpha \in I$, let $\struct {S_\alpha, \tau_\alpha}$ be a $T_3$ space.
Then $T$ is a $T_3$ space.

Proof:
For each $\alpha \in I$, let $\struct {S_\alpha, \tau_\alpha}$ be a $T_3$ space.
Let $U$ be open in $T$ and $x \in U$.
From Natural Basis of Product Topology, there exists $\ds U' = \prod_{\alpha \mathop \in I} U'_\alpha$ such that:
:for all $\alpha \in I : U_\alpha \in \tau_\alpha$
:$J = \set {\alpha \in I: U_\alpha \ne X_\alpha}$ is finite
:$x \in U'$
:$U' \subseteq U$
By definition of a $T_3$ space, for all $\alpha \in J$:
:$\exists V_\alpha \in \tau_\alpha : x_\alpha \in V_\alpha$ and $V^-_\alpha \subseteq U'_\alpha$
For $\alpha \notin J$ let:
:$V_\alpha = X_\alpha$
and let:
:$\ds V = \prod_{\alpha \mathop \in I} V_\alpha$
By definition of the Cartesian product V:
:$x \in V$
From Natural Basis of Product Topology:
:$V$ open in $T$.
Now consider the Cartesian product of closed sets:
:$\ds \prod_{\alpha \mathop \in I} V^-_\alpha$
From Product of Closed Sets is Closed, $\ds \prod_{\alpha \mathop \in I} V^-_\alpha$ is closed.
From Underlying Set of Topological Space is Closed, for $\alpha \notin J$:
:$V^-_\alpha = X^-_\alpha = X_\alpha$
From Cartesian Product of Family of Subsets, it follows that:
:$\ds V = \prod_{\alpha \mathop \in I} V_\alpha \subseteq \prod_{\alpha \mathop \in I} V^-_\alpha \subseteq \prod_{\alpha \mathop \in I} U'_\alpha \subseteq U$
It follows that $T$ is a $T_3$ space by definition.
Theorem: Mittag-Leffler Expansion for Cosecant Function/Real Domain

:$\pi \cosec \pi \alpha = \dfrac 1 \alpha + \ds 2 \sum_{n \mathop \ge 1} \paren {-1}^n \dfrac {\alpha} {\alpha^2 - n^2}$

Proof:
From Half-Range Fourier Cosine Series for $\cos \alpha x$ over $\openint 0 \pi$:
:$\ds \cos \alpha x \sim \frac {2 \alpha \sin \alpha \pi} \pi \paren {\frac 1 {2 \alpha^2} + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {\cos n x} {\alpha^2 - n^2} }$
Setting $x = 0$:
{{begin-eqn}}
{{eqn | l = \cos 0
      | r = \frac {2 \alpha \sin \alpha \pi} \pi \paren {\frac 1 {2 \alpha^2} + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {\cos 0} {\alpha^2 - n^2} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = \frac {2 \alpha \sin \alpha \pi} \pi \paren {\frac 1 {2 \alpha^2} + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} {\alpha^2 - n^2} }
      | c = Cosine of Zero is One
}}
{{eqn | ll= \leadsto
      | l = \frac \pi {2 \alpha \sin \alpha \pi}
      | r = \frac 1 {2 \alpha^2} + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n} {\alpha^2 - n^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \pi \cosec \pi \alpha
      | r = \dfrac 1 \alpha + 2 \sum_{n \mathop \ge 1} \paren {-1}^n \dfrac {\alpha} {\alpha^2 - n^2}
      | c = {{Defof|Cosecant|subdef = Real Function}} and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Mittag-Leffler Expansion for Real Cotangent Function

:$\ds \dfrac 1 \alpha + \sum_{n \mathop \ge 1} \dfrac {2 \alpha} {\alpha^2 - n^2} = \pi \cot \pi \alpha$

Proof:
Corollary of Sum over Integers of $\dfrac {\cos \paren {n + \alpha} \theta} {n + \alpha}$
{{ProofWanted|fill in details}}
{{qed}}
Theorem: Sum of Complex Exponentials of i times Arithmetic Sequence of Angles/Formulation 1

:$\ds \sum_{k \mathop = 0}^n e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} } \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} }$

Proof:
First note that if $\alpha = 2 \pi k$ for $k \in \Z$, then $e^{i \alpha} = 1$.
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n e^{i \paren {\theta + k \alpha} }
      | r = e^{i \theta} \sum_{k \mathop = 0}^n e^{i k \alpha}
      | c = factorising $e^{i \theta}$
}}
{{eqn | r = e^{i \theta} \paren {\frac {e^{i \paren {n + 1} \alpha} - 1} {e^{i \alpha} - 1} }
      | c = Sum of Geometric Sequence: only when $e^{i \alpha} \ne 1$
}}
{{eqn | r = \frac {e^{i \theta} e^{i \paren {n + 1} \alpha / 2} } {e^{i \alpha / 2} } \paren {\frac {e^{i \paren {n + 1} \alpha / 2} - e^{-i \paren {n + 1} \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = extracting factors
}}
{{eqn | r = e^{i \paren {\theta + n \alpha / 2} } \paren {\frac {e^{i \paren {n + 1} \alpha / 2} - e^{-i \paren {n + 1} \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = Exponential of Sum and some algebra
}}
{{eqn | r = \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} } \paren {\frac {e^{i \paren {n + 1} \alpha / 2} - e^{-i \paren {n + 1} \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = Euler's Formula
}}
{{eqn | r = \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} } \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} }
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Category:Sum of Complex Exponentials of i times Arithmetic Sequence of Angles
ghql7on4mtrrppnu0947q5xcbk0d3jq
Theorem: Sum of Complex Exponentials of i times Arithmetic Sequence of Angles/Formulation 2

:$\ds \sum_{k \mathop = 1}^n e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$

Proof:
First note that if $\alpha = 2 \pi k$ for $k \in \Z$, then $e^{i \alpha} = 1$.
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n e^{i \paren {\theta + k \alpha} }
      | r = e^{i \theta} e^{i \alpha} \sum_{k \mathop = 0}^{n - 1} e^{i k \alpha}
      | c = factorising $e^{i \theta} e^{i \alpha}$
}}
{{eqn | r = e^{i \theta} e^{i \alpha} \paren {\frac {e^{i n \alpha} - 1} {e^{i \alpha} - 1} }
      | c = Sum of Geometric Sequence: only when $e^{i \alpha} \ne 1$
}}
{{eqn | r = e^{i \theta} e^{i \alpha} \paren {\frac {e^{i n \alpha / 2} \paren {e^{i n \alpha / 2} - e^{-i n \alpha / 2} } } {e^{i \alpha / 2} \paren {e^{i \alpha / 2} - e^{-i \alpha / 2} } } }
      | c = extracting factors
}}
{{eqn | r = e^{i \paren {\theta + \paren {n + 1} \alpha / 2} } \paren {\frac {e^{i n \alpha / 2} - e^{-i n \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = Exponential of Sum and some algebra
}}
{{eqn | r = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \paren {\frac {e^{i n \alpha / 2} - e^{-i n \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = Euler's Formula
}}
{{eqn | r = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sines of Arithmetic Sequence of Angles/Formulation 1

{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n \map \sin {\theta + k \alpha}
      | r = \sin \theta + \map \sin {\theta + \alpha} + \map \sin {\theta + 2 \alpha} + \map \sin {\theta + 3 \alpha} + \dotsb
}}
{{eqn | r = \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} } \map \sin {\theta + \frac {n \alpha} 2}
}}
{{end-eqn}}

Proof:
From Sum of Complex Exponentials of i times Arithmetic Sequence of Angles: Formulation 1:
:$\ds \sum_{k \mathop = 0}^n e^{i \paren {\theta + k \alpha} } =  \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} } \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} }$
It is noted that, from Sine of Multiple of Pi, when $\alpha = 2 \pi k$ for $k \in \Z$, $\map \sin {\alpha / 2} = 0$ and the {{RHS}} is not defined.
From Euler's Formula, this can be expressed as:
:$\ds \sum_{k \mathop = 0}^n \paren {\map \cos {\theta + k \alpha} + i \map \sin {\theta + k \alpha} } = \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} } \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} }$
Equating imaginary parts:
:$\ds \sum_{k \mathop = 0}^n \map \sin {\theta + k \alpha} = \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} } \map \sin {\theta + \frac {n \alpha} 2}$
{{qed}}
Theorem: Sum of Sines of Arithmetic Sequence of Angles/Formulation 2

{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \map \sin {\theta + k \alpha}
      | r = \map \sin {\theta + \alpha} + \map \sin {\theta + 2 \alpha} + \map \sin {\theta + 3 \alpha} + \dotsb
}}
{{eqn | r = \map \sin {\theta + \frac {n + 1} 2 \alpha}\frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }
}}
{{end-eqn}}

Proof:
From Sum of Complex Exponentials of i times Arithmetic Sequence of Angles: Formulation 2:
:$\ds \sum_{k \mathop = 1}^n e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
It is noted that, from Sine of Multiple of Pi, when $\alpha = 2 \pi k$ for $k \in \Z$, $\map \sin {\alpha / 2} = 0$ and the {{RHS}} is not defined.
From Euler's Formula, this can be expressed as:
:$\ds \sum_{k \mathop = 1}^n \paren {\map \cos {\theta + k \alpha} + i \map \sin {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
Equating imaginary parts:
:$\ds \sum_{k \mathop = 1}^n \map \sin {\theta + k \alpha} = \map \sin {\theta + \frac {n + 1} 2 \alpha} \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
{{qed}}
Theorem: Sum of Cosines of Arithmetic Sequence of Angles/Formulation 1

{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n \map \cos {\theta + k \alpha}
      | r = \cos \theta + \map \cos {\theta + \alpha} + \map \cos {\theta + 2 \alpha} + \map \cos {\theta + 3 \alpha} + \dotsb
}}
{{eqn | r = \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} } \map \cos {\theta + \frac {n \alpha} 2}
}}
{{end-eqn}}

Proof:
From Sum of Complex Exponentials of i times Arithmetic Sequence of Angles: Formulation 1:
:$\ds \sum_{k \mathop = 0}^n e^{i \paren {\theta + k \alpha} } =  \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} } \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} }$
It is noted that, from Sine of Multiple of Pi, when $\alpha = 2 \pi k$ for $k \in \Z$, $\map \sin {\alpha / 2} = 0$ and the {{RHS}} is not defined.
From Euler's Formula, this can be expressed as:
:$\ds \sum_{k \mathop = 0}^n \paren {\map \cos {\theta + k \alpha} + i \map \sin {\theta + k \alpha} } = \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} } \paren {\map \cos {\theta + \frac {n \alpha} 2} + i \map \sin {\theta + \frac {n \alpha} 2} }$
Equating real parts:
:$\ds \sum_{k \mathop = 0}^n \map \cos {\theta + k \alpha} = \frac {\map \sin {\alpha \paren {n + 1} / 2} } {\map \sin {\alpha / 2} } \map \cos {\theta + \frac {n \alpha} 2}$
{{qed}}
Theorem: Sum of Cosines of Arithmetic Sequence of Angles/Formulation 2

{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^n \map \cos {\theta + k \alpha}
      | r = \map \cos {\theta + \alpha} + \map \cos {\theta + 2 \alpha} + \map \cos {\theta + 3 \alpha} + \dotsb
}}
{{eqn | r = \map \cos {\theta + \frac {n + 1} 2 \alpha} \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }
}}
{{end-eqn}}

Proof:
From Sum of Complex Exponentials of i times Arithmetic Sequence of Angles: Formulation 2:
:$\ds \sum_{k \mathop = 1}^n e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
It is noted that, from Sine of Multiple of Pi, when $\alpha = 2 \pi k$ for $k \in \Z$, $\map \sin {\alpha / 2} = 0$ and the {{RHS}} is not defined.
From Euler's Formula, this can be expressed as:
:$\ds \sum_{k \mathop = 1}^n \paren {\map \cos {\theta + k \alpha} + i \map \sin {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {n + 1} 2 \alpha} + i \map \sin {\theta + \frac {n + 1} 2 \alpha} } \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
Equating real parts:
:$\ds \sum_{k \mathop = 1}^n \map \cos {\theta + k \alpha} = \map \cos {\theta + \frac {n + 1} 2 \alpha} \frac {\map \sin {n \alpha / 2} } {\map \sin {\alpha / 2} }$
{{qed}}
Theorem: Sum of Complex Exponentials of i times Arithmetic Sequence of Angles/Formulation 3

:$\ds \sum_{k \mathop = p}^q e^{i \paren {\theta + k \alpha} } = \paren {\map \cos {\theta + \frac {\paren {p + q} \alpha} 2} + i \map \sin {\theta + \frac {\paren {p + q} \alpha} 2} } \frac {\map \sin {\paren {q - p + 1} \alpha / 2} } {\map \sin {\alpha / 2} }$

Proof:
First note that if $\alpha = 2 \pi k$ for $k \in \Z$, then $e^{i \alpha} = 1$.
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = p}^q e^{i \paren {\theta + k \alpha} }
      | r = e^{i \theta} e^{i p \alpha} \sum_{k \mathop = 0}^{q - p} e^{i k \alpha}
      | c = factorising $e^{i \theta} e^{i p \alpha}$
}}
{{eqn | r = e^{i \theta} e^{i p \alpha} \paren {\frac {e^{i \paren {q - p + 1} \alpha} - 1} {e^{i \alpha} - 1} }
      | c = Sum of Geometric Sequence: only when $e^{i \alpha} \ne 1$
}}
{{eqn | r = e^{i \theta} e^{i p \alpha} \frac {e^{i \paren {q - p + 1} \alpha / 2} } {e^{i \alpha / 2} } \paren {\frac {e^{i \paren {q - p + 1} \alpha / 2} - e^{-i \paren {q - p + 1} \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = extracting factors
}}
{{eqn | r = e^{i \paren {\theta + \paren {p + q} \alpha / 2} } \paren {\frac {e^{i \paren {q - p + 1} \alpha / 2} - e^{-i \paren {q - p + 1} \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = Exponential of Sum and some algebra
}}
{{eqn | r = \paren {\map \cos {\theta + \frac {\paren {p + q} \alpha} 2} + i \map \sin {\theta + \frac {\paren {p + q} \alpha} 2} } \paren {\frac {e^{i \paren {q - p + 1} \alpha / 2} - e^{-i \paren {q - p + 1} \alpha / 2} } {e^{i \alpha / 2} - e^{-i \alpha / 2} } }
      | c = Euler's Formula
}}
{{eqn | r = \paren {\map \cos {\theta + \frac {\paren {p + q} \alpha} 2} + i \map \sin {\theta + \frac {\paren {p + q} \alpha} 2} } \frac {\map \sin {\paren {q - p + 1} \alpha / 2} } {\map \sin {\alpha / 2} }
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Category:Sum of Complex Exponentials of i times Arithmetic Sequence of Angles
s4mazxtuw3s46217ioec2yxommxenjv
Theorem: Weierstrass Approximation Theorem/Lemma 1

:$\ds \sum_{k \mathop = 0}^n k \map {p_{n, k} } t = n t$

Proof:
From Binomial Theorem for Integral Index:
{{begin-eqn}}
{{eqn | l = \paren {x + y}^n
      | r = \sum_{k \mathop = 0}^n \binom n k y^k x^{n - k}
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = \sum_{k \mathop = 0}^n \binom n k t^k \paren {1 - t}^{n - k}
      | c = $y = t, ~x = 1 - t$
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \sum_{k \mathop = 0}^n \binom n k \paren {k t^{k - 1} \paren {1 - t}^{n - k} - t^k \paren{n - k} \paren {1 - t}^{n - k - 1} }
      | c = Derivative {{WRT|Differentiation}} $t$
}}
{{eqn | r = \sum_{k \mathop = 0}^n k p_{n,k} \paren {\frac 1 t + \frac 1 {1 - t} } - \frac n {1 - t}
}}
{{eqn | ll= \leadsto
      | l = n t
      | r = \sum_{k \mathop = 0}^n k p_{n,k}
}}
{{end-eqn}}
{{qed}}
Theorem: Weierstrass Approximation Theorem/Lemma 2

:$\ds \sum_{k \mathop = 0}^n \paren {k - n t}^2 \map {p_{n, k} } t = n t \paren {1 - t}$

Proof:
From Binomial Theorem for Integral Index:
:$\ds 1 = \sum_{k \mathop = 0}^n \binom n k t^k \paren {1 - t}^{n - k}$
From {{Lemma|Weierstrass Approximation Theorem|1}}:
{{begin-eqn}}
{{eqn | l = n t
      | r = \sum_{k \mathop = 0}^n \binom n k k t^k \paren {1 - t}^{n - k}
}}
{{eqn | ll= \leadsto
      | l = n
      | r = \sum_{k \mathop = 0}^n \binom n k k \paren {k t^{k - 1} \paren {1 - t}^{n - k} - t^k \paren {n - k} \paren {1 - t}^{n - k - 1} }
      | c = {{Defof|Derivative of Real Function}} {{WRT|Differentiation}} $t$
}}
{{eqn | r = \frac 1 t \sum_{k \mathop = 0}^n k^2 \map {p_{n, k} } t - \frac n {1 - t} \sum_{k \mathop = 0}^n k \map {p_{n, k} } t + \frac 1 {1 - t} \sum_{k \mathop = 0}^n k^2 \map {p_{n, k} } t 
}}
{{eqn | r = \frac 1 {t \paren {1 - t} } \sum_{k \mathop = 0}^n k^2 \map {p_{n, k} } t - \frac n {1 - t} n t
}}
{{eqn | ll= \leadsto 
      | l = \sum_{k \mathop = 0}^n k^2 \map {p_{n, k} } t
      | r = n t \paren {1 - t} + n^2 t^2
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^n \paren {k - n t}^2 \map {p_{n, k} } t
      | r = \sum_{k \mathop = 0}^n \paren {k^2 - 2 n t k + n^2 t^2} \map {p_{n, k} } t
}}
{{eqn | r = n t \paren {1 - t} + n^2 t^2 - 2 n t n t + n^2 t^2
}}
{{eqn | r = n t \paren {1 - t}
}}
{{end-eqn}}
{{qed}}
Theorem: Convergent Sequence in Normed Vector Space has Unique Limit

Let $\struct {X, \norm {\,\cdot\,} }$ be a normed vector space.
Let $\sequence {x_n}$ be a sequence in $\struct {X, \norm {\,\cdot\,} }$.
Then $\sequence {x_n}$ can have at most one limit.

Proof:
{{AimForCont}} $\ds \lim_{n \mathop \to \infty} x_n = L_1$ and $\ds \lim_{n \mathop \to \infty} x_n = L_2$ such that $L_1 \ne L_2$.
Let $\epsilon = \dfrac {\norm {L_1 - L_2} } 3$.
From the norm axioms it follows that $\epsilon > 0$.
By definition:
:$\exists N_1 \in \N : \forall n > N_1 : \norm {x_n - L_1} < \epsilon$
:$\exists N_2 \in \N : \forall n > N_2 : \norm {x_n - L_2} < \epsilon$
Choose $n > N_1 + N_2$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {L_1 - L_2}
      | r = \norm {L_1 - x_n + x_n - L_2}
}}
{{eqn | o = \le
      | r = \norm {L_1 - x_n} + \norm {x_n - L_2}
      | c = Triangle Inequality
}}
{{eqn | o = < 
      | r = \epsilon + \epsilon
}}
{{eqn | r = \frac 2 3 \norm {L_1 - L_2}
}}
{{end-eqn}}
which implies that:
:$1 < \dfrac 2 3$
This is a contradiction.
Hence $L_1 = L_2$.
{{qed}}
Theorem: Product Space is T3.5 iff Factor Spaces are T3.5/Sufficient Condition

Let $\mathbb S = \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 $\mathbb S$.
Let $T$ be a $T_{3 \frac 1 2}$ space.
Then for each $\alpha \in I$, $\struct {S_\alpha, \tau_\alpha}$ is a $T_{3 \frac 1 2}$ space.

Proof:
Let $T$ be a $T_{3 \frac 1 2}$ space.
Since $S_\alpha \ne \O$ we also have $S \ne \O$ by the {{Axiom-link|Choice}}.
Let $\alpha \in I$ be arbitrary.
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_{3 \frac 1 2}$ Property is Hereditary:
:$T_\alpha$ is $T_{3 \frac 1 2}$.
From $T_{3 \frac 1 2}$ Property is Preserved under Homeomorphism:
:$\struct {S_\alpha, \tau_\alpha}$ is $T_{3 \frac 1 2}$.
Because $\alpha \in I$ was arbitrary, it follows that each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_{3 \frac 1 2}$ space.
Theorem: Product Space is T3.5 iff Factor Spaces are T3.5/Necessary Condition

Let $\mathbb S = \family {\struct{S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an indexed family of topological spaces for $\alpha$ in some indexing set $I$ with $S_\alpha \ne \O$ for every $\alpha \in I$.
Let $\ds T = \struct{S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\mathbb S$.
For each $\alpha \in I$, let $\struct{S_\alpha, \tau_\alpha}$ be a $T_{3 \frac 1 2}$ space.
Then $T$ is a $T_{3 \frac 1 2}$ space.

Proof:
Let $\struct {S_\alpha, \tau_\alpha}$ is a $T_{3 \frac 1 2}$ space for each $\alpha \in I$. 
Let $x \in S$.
Let $F$ be a closed subset of $S$ such that $x \notin F$.
By definition of a closed subset:
:$S \setminus F \in \tau$
By definition of the product topology, there exists an open set $B$ of the natural basis containing $x$ which is disjoint from $F$.
By definition of the natural basis, $B$ is of the form:
:$\map {\pr_{\alpha_1}^\gets} {U_1} \cap \dotsb \cap \map {\pr_{\alpha_n}^\gets} {U_n}$
where:
:$\pr_{\alpha_k}$ is the $\alpha_k$-th projection from $S$ 
:$U_k$ is open in $S_{\alpha_k}$ for all $1 \le k \le n$
By definition of a $T_{3 \frac 1 2}$ space, for each $1 \le k \le n$ there exists a continuous mapping:
:$f_k: S_{\alpha_k} \to \closedint 0 1$
such that:
:$\map {f_k} {x_{\alpha_k} } = 1$
and:
:$\map {f_k} {S_{\alpha_k} \setminus U_k} = 0$
Let $g_k = f_k \circ \pr_{\alpha_k}$ be the composite mapping of $f_k$ with $\pr_{\alpha_k}$ for each $1 \le k \le n$.
From Composite of Continuous Mappings is Continuous each $g_k: S \to \closedint 0 1$ is a continuous mapping.
We define $g: S \to \closedint 0 1$ by setting:
:$\map g y = \min \set {\map {g_k} {y_{\alpha_k} }: k = 1, \dotsc, n}$
From Minimum Rule for Continuous Functions:
:$g$ is continuous. 
Now:
{{begin-eqn}}
{{eqn | l = \map g x
      | r = \min \set {\map {g_k} x : k = 1, \dotsc, n}
      | c = Definition of $g$
}}
{{eqn | r = \min \set {\map {f_k} {\map {\pr_{\alpha_k} } x} : k = 1, \dotsc, n}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \min \set {\map {f_k} {x_{\alpha_k} } : k = 1, \dotsc, n}
      | c = {{Defof|Projection}}
}}
{{eqn | r = \min \set {1 : k = 1, \dotsc, n}
      | c = Definition of $f_k$
}}
{{eqn | r = 1
      | c = {{Defof|Minimum}}
}}
{{end-eqn}}
Let $y \in F$.
By definition of disjoint sets:
:$\exists j \in \set {1, \dotsc, n} : y \notin \map {\pr_{\alpha_j}^\gets} {U_j}$
By definition of the inverse image mapping of $\pr_{\alpha_j}$:
:$y_{\alpha_j} \notin U_j$
Thus:
:$\map {f_j} {y_{\alpha_j} } = 0$
So:
{{begin-eqn}}
{{eqn | l = \map g y
      | r = \min \set {\map {g_k} y : k = 1, \dotsc, n}
      | c = Definition of $g$
}}
{{eqn | r = \min \set {\map {f_k} {\map {\pr_{\alpha_k} } y} : k = 1, \dotsc, n}
      | c = {{Defof|Composite Mapping}}
}}
{{eqn | r = \min \set {\map {f_k} {y_{\alpha_k} } : k = 1, \dotsc, n}
      | c = {{Defof|Projection}}
}}
{{eqn | r = 0
      | c = {{Defof|Minimum}} and $\map {f_k} {y_{\alpha_k} } = 0$
}}
{{end-eqn}}
Therefore $T$ is a $T_{3 \frac 1 2}$ space.
Theorem: Minimum Rule for Continuous Functions

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

Proof:
Let $x \in S$.
Let $\epsilon > 0$.
{{WLOG}}, assume that $\map f x \le \map g x$.
Theorem: Min is Half of Sum Less Absolute Difference

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

Proof:
From the definition of min:
:<nowiki>$\map \min {a, b} = \begin{cases}
a: & a \le b \\
b: & b \le a
\end{cases}$</nowiki>
Let $a < b$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac 1 2 \paren {a + b - \size {a - b} }
      | r = \dfrac 1 2 \paren {a + b - \paren {b - a} }
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \dfrac 1 2 \paren {a + b - b + a}
}}
{{eqn | r = \dfrac 1 2 \paren {2 a}
}}
{{eqn | r = a
}}
{{eqn | r = \min \set {a, b}
      | c = {{Defof|Min Operation}}
}}
{{end-eqn}}
{{qed|lemma}}
Let $a \ge b$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac 1 2 \paren {a + b - \size {a - b} }
      | r = \dfrac 1 2 \paren {a + b - \paren {a - b} }
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \dfrac 1 2 \paren {a + b - a + b}
}}
{{eqn | r = \dfrac 1 2 \paren {2 b}
}}
{{eqn | r = b
}}
{{eqn | r = \min \set {a, b}
      | c = {{Defof|Min Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Continuity Test for Real-Valued Functions

Let $\struct{S, \tau}$ be a topological space.
Let $f: S \to \R$ be a real-valued function.
Let $x \in S$.
Then $f$ is continuous at $x$ {{iff}}:
:$\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:
=== Necessary Condition ===
{{:Continuity Test for Real-Valued Functions/Necessary Condition}}{{qed|lemma}}