avewright/proofwiki-math huggingface dataset:
Theorem: Recurrence Formula for Chebyshev Polynomials of the First Kind

Let $\map {T_n} x$ denote the Chebyshev polynomials of the first kind of order $n$.
Then:
:$\map {T_n} x = \begin {cases} 1 & : n = 0 \\ x & : n = 1 \\ 2 x \, \map {T_{n - 1} } x - \map {T_{n - 2} } x & : n > 1 \end {cases}$

Proof:
From the {{Defof|Chebyshev Polynomials/First Kind|Chebyshev Polynomials of the First Kind}}, we have:
:$\map {T_n} x = \map \cos {n \arccos x}$
For $n = 0$, we have:
{{begin-eqn}}
{{eqn | l = \map {T_0} x
      | r = \map \cos {0 \arccos x}
      | c = {{Defof|Chebyshev Polynomials/First Kind|Chebyshev Polynomials of the First Kind}} at $n = 0$
}}
{{eqn | ll = \leadsto
      | l = \map {T_0} x
      | r = 1
      | c = Cosine of Zero is One
}}
{{end-eqn}}
For $n = 1$, we have:
{{begin-eqn}}
{{eqn | l = \map {T_1} x
      | r = \map \cos {\arccos x}
      | c = {{Defof|Chebyshev Polynomials/First Kind|Chebyshev Polynomials of the First Kind}} at $n = 1$
}}
{{eqn | ll = \leadsto
      | l = \map {T_1} x
      | r = x
      | c = 
}}
{{end-eqn}}
For $n > 1$, let $x = \cos \theta$.
Then:
{{begin-eqn}}
{{eqn | l = \map {T_n} x
      | r = \map \cos {n \arccos x}
      | c = {{Defof|Chebyshev Polynomials/First Kind|Chebyshev Polynomials of the First Kind}}
}}
{{eqn | ll = \leadsto
      | l = \map {T_n} {\cos \theta}
      | r = \map \cos {n \arccos \cos \theta}
      | c = $x \to \cos \theta$
}}
{{eqn | ll = \leadsto
      | l = \map {T_n} {\cos \theta}
      | r = \map \cos {n \theta}
      | c = 
}}
{{end-eqn}}
From {{Formulation|Cosine of Integer Multiple of Argument|4}}, we have:
:$\ds \map \cos {n \theta} = \paren {2 \cos \theta} \map \cos {\paren {n - 1} \theta}  - \map \cos {\paren {n - 2} \theta}$
Therefore:
{{begin-eqn}}
{{eqn | l = \map {T_n} {\cos \theta}
      | r = \map \cos {n \theta}
      | c = 
}}
{{eqn | r = \paren {2 \cos \theta} \map \cos {\paren {n - 1} \theta}  - \map \cos {\paren {n - 2} \theta}
      | c = {{Formulation|Cosine of Integer Multiple of Argument|4}}
}}
{{eqn | r = \paren {2 \cos \theta} \map {T_{n - 1} } {\cos \theta}  - \map {T_{n - 2} } {\cos \theta} 
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \map {T_n} x
      | r = 2 x \map {T_{n - 1} } x - \map {T_{n - 2} } x
      | c = $\cos \theta \to x$
}}
{{end-eqn}}
{{qed}}
Theorem: Category of Semilattices is Category

Let $\mathbf{SLat}$ denote the category of semilattices.
Then:
:$\mathbf{SLat}$ is a metacategory

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two semilattice homomorphisms their composition (in the usual set theoretic sense) is again a semilattice homomorphism by Composite Semilattice Homomorphisms is Semilattice Homomorphism.
For any semilattice $\struct{S, \circ}$, we have the identity mapping $\operatorname{id}_S$.
From Identity Mapping is Semilattice Homomorphism we have $\operatorname{id}_S$ is a semilattice homomorphism.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $\struct{S, \circ}$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{SLat}$ is a metacategory.
{{qed}}
Theorem: Composite Semilattice Homomorphisms is Semilattice Homomorphism

Let $S_1 = \struct{A_1, \circ_1}$, $S_2 = \struct{A_2, \circ_2}$ and $S_3 = \struct{A_3, \circ_3}$ be semilattices.
Let $\phi_1: S_1 \to S_2$ and $\phi_2: S_2 \to S_3$ be semilattice homomorphisms.
Let $\phi_2 \circ \phi_1 : A_1 \to A_3$ be the composite mapping of $\phi_1$ and $\phi_2$  
Then:
:$\phi_2 \circ \phi_1$ is a semilattice homomorphism of $S_1$ to $S_3$

Proof:
Follows immediately from Composite of Homomorphisms is Homomorphism
{{qed}}
Category:Semilattice Homomorphisms
1et9giqbcjvdauvmpsn69utj7xxx85j
Theorem: Identity Mapping is Semilattice Homomorphism

Let $S = \struct{A, \circ}$ be a semilattice.
Let $\operatorname{id}_A$ denote the identity mapping on $A$.
Then:
:$\operatorname{id}_A$ is a semilattice homomorphism of $S$ to $S$

Proof:
Follows immediately from Identity Mapping is Automorphism.
{{qed}}
Category:Semilattice Homomorphisms
npgqu71tccimkqe5gc43a4q5ky38tmm
Theorem: Scalene Triangle Tessellates the Plane

Let $T$ be a triangle, which can be any shape at all, even scalene.
Then $T$ can tessellate the plane.

Proof:
By placing $2$ copies of $T$ together so their corresponding sides coincide, it is possible to form a quadrilateral.
The result follows from Quadrilateral Tessellates the Plane.
{{qed}}
Theorem: Surface Area of Torus/Formulation 1

Let $\TT$ be a torus.
Let $r$ be the radius of the generating circle of $\TT$.
Let $R$ be the distance of the center of the generating circle from the axis of revolution of $\TT$.
Then the area $\AA$ of $\TT$ is given by:
:$\AA = 4 \pi^2 r R$

Proof:
Recall Pappus's Centroid Theorem for Surface Area:
{{:Pappus's Centroid Theorem for Surface Area}}
In this context:
:$C$ is the generating circle of $\TT$, which has radius $r$
:the centroid of $C$ is the center of $C$, which is at a distance $R$ from the axis of revolution.
From Perimeter of Circle, the perimeter of $C$ is $2 \pi r$.
Also from Perimeter of Circle, the distance travelled by the center of $C$ is $2 \pi R$.
Hence:
:$\AA = \paren {2 \pi r} \paren {2 \pi R}$
Hence the result.
{{qed}}
Theorem: Volume of Torus/Formulation 1

Let $\TT$ be a torus.
Let $r$ be the radius of the generating circle of $\TT$.
Let $R$ be the distance of the center of the generating circle from the axis of revolution of $\TT$.
Then the volume $\VV$ enclosed by $\TT$ is given by:
:$\VV = 2 \pi^2 r^2 R$

Proof:
Recall Pappus's Centroid Theorem for Volume:
{{:Pappus's Centroid Theorem for Volume}}
In this context:
:$C$ is the generating circle of $\TT$, which has radius $r$
:the centroid of $C$ is the center of $C$, which is at a distance $R$ from the axis of revolution.
From Area of Circle, the area of $C$ is $\pi r^2$.
From Perimeter of Circle, the distance travelled by the center of $C$ is $2 \pi R$.
Hence:
:$\VV = \paren {\pi r^2} \paren {2 \pi R}$
Hence the result.
{{qed}}
Theorem: Equivalence of Definitions of Embedding of Categories

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F : \mathbf C \to \mathbf D$ be a functor.
{{TFAE|def=Embedding of Categories}}
=== Definition 1 ===
{{:Definition:Embedding of Categories/Definition 1}}
=== Definition 2 ===
{{:Definition:Embedding of Categories/Definition 2}}
=== Definition 3 ===
{{:Definition:Embedding of Categories/Definition 3}}

Proof:
{{ProofWanted}}
Category:Embeddings of Categories
masz0f4irqjpkki8dub7whs14e559da
Theorem: Transpose of Column Matrix is Row Matrix

Let $\mathbf x = \sqbrk x_{1 n} = \begin {bmatrix} x_1 & x_2 & \cdots & x_n \end {bmatrix}$ be a column matrix.
Then $\mathbf x^\intercal$, the transpose of $\mathbf x$, is a row matrix:
:$\begin {bmatrix} x_1 \\ x_2 \\ \vdots \\ x_n \end{bmatrix}^\intercal = \begin {bmatrix} x_1 & x_2 & \cdots & x_n \end {bmatrix}$

Proof:
Self-evident.
{{Qed}}
Theorem: Cotangent is Cosecant divided by Secant

Let $\theta$ be an angle such that $\sin \theta \ne 0$.
Then:
:$\cot \theta = \dfrac {\cosec \theta} {\sec \theta}$
where $\cot$, $\cosec$ and $\sec$ mean cotangent, cosecant and secant respectively.

Proof:
{{begin-eqn}}
{{eqn | l = \cot \theta
      | r = \dfrac {\cos \theta} {\sin \theta}
      | c = Cotangent is Cosine divided by Sine, which holds when $\sin \theta \ne 0$
}}
{{eqn | r = \dfrac {1 / \sec \theta} {1 / \cosec \theta}
      | c = Secant is Reciprocal of Cosine, Cosecant is Reciprocal of Sine
}}
{{eqn | r = \dfrac {\dfrac 1 {\sec \theta} \cosec \theta \sec \theta} {\dfrac 1 {\cosec \theta} \cosec \theta \sec \theta}
      | c = multiplying top and bottom by $\cosec \theta \sec \theta$
}}
{{eqn | r = \dfrac {\cosec \theta} {\sec \theta}
      | c = after simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Obtuse Angle is Positive

Let $\theta$ be an obtuse angle.
Then:
:$\sin \theta > 0$
where $\sin$ denotes the sine function.

Proof:
{{ProofWanted|trivial but I don't want to be distracted.}}
Theorem: Cosine of Obtuse Angle is Negative

Let $\theta$ be an obtuse angle.
Then:
:$\cos \theta < 0$
where $\cos$ denotes the cosine function.

Proof:
Let $\theta$ be an obtuse angle.
By definition of obtuse angle:
:$90 \degrees < \theta < 180 \degrees$
Let us align $\theta$ in a Cartesian plane such that:
:$\theta$ itself is at the origin
:one arm of $\theta$ is aligned with the positive $x$-axis.
Then the other arm of $\theta$ is in either the second quadrant or the third quadrant.
The result follows from Cosine of Angle in Cartesian Plane.
{{qed}}
Theorem: Tangent of Obtuse Angle is Negative

Let $\theta$ be an obtuse angle.
Then:
:$\tan \theta < 0$
where $\tan$ denotes the tangent function.

Proof:
{{ProofWanted|trivial but I don't want to be distracted.}}
Theorem: Scalar Triple Product as Product of Magnitudes

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be vectors in a Cartesian $3$-space:
{{begin-eqn}}
{{eqn | l = \mathbf a
      | r = a_i \mathbf i + a_j \mathbf j + a_k \mathbf k
}}
{{eqn | l = \mathbf b
      | r = b_i \mathbf i + b_j \mathbf j + b_k \mathbf k
}}
{{eqn | l = \mathbf c
      | r = c_i \mathbf i + c_j \mathbf j + c_k \mathbf k
}}
{{end-eqn}}
where $\tuple {\mathbf i, \mathbf j, \mathbf k}$ is the standard ordered basis of $\mathbf V$.
Let $\sqbrk {\mathbf a, \mathbf b, \mathbf c}$ be the scalar triple product of $\mathbf a$, $\mathbf b$ and $\mathbf c$.
Then:
:$\sqbrk {\mathbf a, \mathbf b, \mathbf c} = \size {\mathbf a} \size {\mathbf b} \size {\mathbf c} \sin \theta \cos \alpha$
where:
:$\theta$ is the angle between $\mathbf b$ and $\mathbf c$
:$\alpha$ is the angle between $\mathbf b \times \mathbf c$ and $\mathbf a$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \sqbrk {\mathbf a, \mathbf b, \mathbf c}
      | r = \mathbf a \cdot \paren {\mathbf b \times \mathbf c}
      | c = {{Defof|Scalar Triple Product}}
}}
{{eqn | r = \size {\mathbf a} \size {\mathbf b \times \mathbf c} \cos \alpha
      | c = {{Defof|Dot Product}} in real Euclidean space
}}
{{eqn | r = \size {\mathbf a} \size {\mathbf b} \size {\mathbf c} \sin \theta \cos \alpha
      | c = {{Defof|Cross Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Velocity of Point in Straight Line

Let $\mathbf v$ be the velocity of a particle $P$ in space.
Let $P$ be moving along a straight line $\LL$ whose positive direction has been established.
Then the motion of $P$ can be defined by:
:$\mathbf v = \dfrac {\d s} {\d t} \mathbf i$
where $\mathbf i$ denotes the unit vector in the positive direction of $\LL$.

Proof:
We have {{hypothesis}} that $P$ moves along a straight line $\LL$.
Then the rate of change of displacement perpendicular to $\LL$ is zero.
Let the $\LL$ be embedded in a Cartesian space $\CC$.
From the components of velocity vector, we have:
:$\mathbf v = \dfrac {\d \mathbf r} {\d t}$
where $\mathbf r$ is the displacement of $P$ at time $t$ expressed as a position vector from a given origin.
Thus:
:$\mathbf v = \dfrac {\d x} {\d t} \mathbf i + \dfrac {\d x} {\d t} \mathbf j + \dfrac {\d x} {\d t} \mathbf k$
where:
:$\mathbf r = x \mathbf i + y \mathbf j + z \mathbf k$
Let us define $\CC$ such that $\LL$ is parallel to the $x$-axis of $\CC$.
Then we have:
{{begin-eqn}}
{{eqn | l = \mathbf v
      | r = \dfrac {\d x} {\d t} \mathbf i + \dfrac {\d y} {\d t} \mathbf j + \dfrac {\d z} {\d t} \mathbf k 
      | c = {{Defof|Velocity}}
}}
{{eqn | r = \dfrac {\d x} {\d t} \mathbf i + 0 \mathbf j + 0 \mathbf k
      | c = as the $y$-axis and $z$-axis are perpendicular to $\LL$
}}
{{end-eqn}}
{{qed}}
Theorem: Draft:Union of Set of Sets is Greatest Element under Subset Relation

Let $M$ be a set.
Let $\bigcup M \in M$.
Let $(M, \subseteq)$ be the ordered set formed on $M$ by the subset relation (see Subset Relation is Ordering).
Then $\bigcup M$ is the greatest set by set inclusion ($M$ corresponds to $\TT$) of $(M, \subseteq)$.

Proof:
By Set is Subset of Union:
:$\forall \paren {N \in M}: N \subseteq \bigcup M$. 
Therefore, $\bigcup M$ is the greatest element under the subset relation.
{{qed}}
Category:Set Union
t8lxntmh3eyvirjlfrkqmh01w7u7mtb
Theorem: Binomial Coefficient over Power Not Greater than Reciprocal of Factorial

Let $r > 0$.
Let $k \in \N$ such that $k \le 2r + 1$.
Then:
:$\dfrac {\dbinom r k} {r^k} \le \dfrac 1 {k!}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\binom r k} {r^k}
      | r = \frac 1 {k !} \cdot \frac {r^{\underline k} } {r^k}
      | c = {{Defof|Binomial Coefficient/Real Numbers|Binomial Coefficient}}
}}
{{eqn | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \frac {r - j} r
      | c = {{Defof|Falling Factorial}}, {{Defof|Integer Power}}
}}
{{eqn | ll = \leadsto
      | l = \size {\frac {\binom r k} {r^k} }
      | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \frac {\size {r - j} } r
      | c = Absolute Value Function is Completely Multiplicative
}}
{{end-eqn}}
For each $j = 0, 1, \dotsc, k - 1$, we have:
:$0 \le j \le 2r$
and thus:
:$-r \le j - r \le r$
Hence:
:$\dfrac {\size {r - j} } r \le 1$
Therefore, by Negative of Absolute Value:
:$\dfrac {\binom r k} {r^k} \le \size {\dfrac {\binom r k} {r^k}} \le \dfrac 1 {k!}$
{{qed}}
Category:Binomial Coefficients
Category:Factorials
tf9egfgqt06hw6wfqsfviujlzvvr0ow
Theorem: Exponential Sequence Converges Compactly

For each $n \in \N$, let $f_n : \C \to \C$ be defined as:
:$\map {f_n} z = \paren {1 + \dfrac z n}^n$
Then, $\sequence {f_n}$ converges compactly to the complex exponential function.

Proof:
Let $D$ be a compact subset of $\C$.
By definition, $D$ is bounded, so there is some $M \in \R$ such that:
:$\forall z \in D: \size z \le M$
Let $\epsilon > 0$ be arbitrary.
By definition of the exponential function, there is some $N \in \N$ such that:
:$\forall n \ge N: \map \exp M - \paren {1 + \dfrac M n}^n < \epsilon$
Now, for any $z \in D$ and $n \ge N$:
{{begin-eqn}}
{{eqn | l = \size {\map \exp z - \map {f_n} z}
      | r = \size {\sum_{k \mathop = 0}^\infty \frac {z^k} {k!} - \sum_{k \mathop = 0}^n \binom n k \frac {z^k} {n^k} }
      | c = {{Defof|Complex Exponential Function}}, Binomial Theorem for Integral Index
}}
{{eqn | r = \size {\sum_{k \mathop = 0}^n \paren {\frac 1 {k!} - \frac 1 {n^k} \binom n k} z^k + \sum_{k \mathop = n + 1}^\infty \frac {z^k} {k!} }
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 0}^n \size {\frac 1 {k!} - \frac 1 {n^k} \binom n k} \size z^k + \sum_{k \mathop = n + 1}^\infty \frac {\size z^k} {k!}
      | c = Triangle Inequality for Complex Numbers
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = 0}^n \paren {\frac 1 {k!} - \frac 1 {n^k} \binom n k} M^k + \sum_{k \mathop = n + 1}^\infty \frac {M^k} {k!}
      | c = Binomial Coefficient over Power Not Greater than Reciprocal of Factorial, $\size z \le M$
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \frac {M^k} {k!} - \sum_{k \mathop = 0}^n \binom n k \frac {M^k} {n^k}
}}
{{eqn | r = \exp M - \paren {1 + \frac M n}^n
      | c = {{Defof|Real Exponential Function}}, Binomial Theorem for Integral Index
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
As $\epsilon > 0$ was arbitrary, $\sequence {f_n}$ converges uniformly to $\exp$ on $D$.
But as $D$ was also arbitrary, $\sequence {f_n}$ converges compactly.
{{qed}}
Category:Compact Convergence
Category:Exponential Function
qsgm8fmp9pdd00owe12k9fuvrnb95ic
Theorem: Wald's Equation

Let $\sequence {X_n}_{n \ge 0}$ be a sequence of i.i.d. real-valued random variables.
Let $\sequence {\FF_n}_{n \ge 0}$ be the filtration generated by $\sequence {X_i}_{n \ge 0}$, that is:
:$\FF_n := \map \sigma {X_0, \ldots, X_n}$
the $\sigma$-algebra generated by $X_0, \ldots ,X_n$.
Let $T$ be a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.
For $n \ge 0$, let:
:$S_n := X_0 + \cdots + X_n$ 
Suppose $\expect {\size {X_0} } < \infty$.
Suppose $\expect T < \infty$.
Then:
:$\expect {S_T} = \expect {X_0} \expect T$

Proof:
Let $M,N > 0$.
Let $\mathbb I = \closedint {-M} N$.
Let $\map {\phi_\mathbb{I} }x := \begin{cases} x & : x \in \mathbb I \\ 0 & : x \notin \mathbb I \end{cases}$.
For $n\ge 0$, let:
:$X^\mathbb{I}_n := \map {\phi_\mathbb{I} } {X_n}$
:$S^\mathbb{I}_n := X^\mathbb{I}_0 + \cdots + X^\mathbb{I}_n$
:$M^\mathbb{I}_n := S^\mathbb{I}_n - \paren {n+1} \mu^\mathbb{I}$
Let $\mu^\mathbb{I} := \expect {X^\mathbb{I}_0}$.
Then $\sequence {M^\mathbb{I}_n}_{n\ge 0}$ is a martingale, since:
{{begin-eqn}}
{{eqn | l = \cmod {M^\mathbb{I}_n}
      | o = \le
      | r = \sum_{i\mathop = 0}^n \cmod {X^\mathbb{I}_i} + \paren {n+1} \mu^\mathbb{I}
}}
{{eqn | o = \le
      | r = 2 \paren {n+1} \max\set {M,N}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \expect {M^\mathbb{I}_{n+1}\mid \FF_n }
      | r = \expect {M^\mathbb{I}_n\mid \FF_n } + \expect {X^\mathbb{I}_{n+1} - \mu^\mathbb{I} \mid \FF_n }
}}
{{eqn | r = M^\mathbb{I}_n + \expect {X^\mathbb{I}_{n+1} - \mu^\mathbb{I} }
}}
{{eqn | r = M^\mathbb{I}_n
}}
{{end-eqn}}
Moreover:
:$\cmod {M^\mathbb{I}_{n+1} - M^\mathbb{I}_n} = \cmod {X^\mathbb{I}_n} \le \max \set {M,N}$
Thus by Doob's Optional Stopping Theorem:
:$\expect {M^\mathbb{I}_T} = \expect {M^\mathbb{I}_0} = 0$
That is:
:$\expect {S^\mathbb{I}_T} = \expect {X^\mathbb{I}_0} \expect T$
Consider first $M\to +\infty$ and then $N\to +\infty$.
Applying Monotone Convergence Theorem twice, we obtain:
:$\expect {S_T} = \expect {X_0} \expect T$
{{finish|More details}}
{{Namedfor|Abraham Wald|cat = Wald}}
Theorem: Convergent Sequences Characterize Metrizable Topology

Let $X$ be a set. 
Let $\tau_1$ and $\tau_2$ be metrizable topologies induced by metrics $d_1$ and $d_2$ respectively.
Suppose that:
:a sequence $\sequence {x_n}_{n \in \N} \subseteq X$ converges to $x \in X$ in $\struct {X, d_1}$ {{iff}} it converges to $x$ in $\struct {X, d_2}$. 
Then $\tau_1 = \tau_2$.

Proof:
Let $U$ be open in $\struct {X, d_1}$. 
Then $X \setminus U$ is closed in $\struct {X, d_1}$.
That is, from the definition of closedness in a metric space, for each $x \in X \setminus U$ there exists a sequence $\sequence {x_n}_{n \in \N}$ in $X \setminus U$ converging to $x$ in $\struct {X, d_1}$.
By hypothesis, each such $\sequence {x_n}_{n \in \N}$ also converges to $x$ in $\struct {X, d_2}$.
Hence $X \setminus U$ is also cloesd in $\struct {X, d_2}$.
Hence $U$ is open in $\struct {X, d_2}$.
So $\tau_1 \subseteq \tau_2$.
Swapping $d_1$ and $d_2$ in the above we get $\tau_2 \subseteq \tau_1$ and hence $\tau_1 = \tau_2$. 
{{qed}}
Category:Metric Spaces
Category:Convergent Sequences (Metric Space)
9domdsm47ztg7yabz7iq69i26xsbawl
Theorem: Open Subspace of Polish Space is Polish Space

Let $\struct {X, \tau}$ be a Polish space.
Let $d$ be a metric on $X$ that induces $\tau$ and is such that $\struct {X, d}$ is a complete metric space.
Let $U \subseteq X$ be open.
Let $\tau_U$ be the subspace topology on $U$ induced by $\tau$.
Then $\struct {U, \tau_U}$ is a Polish space.

Proof:
From Subspace of Separable Metric Space is Separable, $\struct {U, \tau_U}$ is separable.
Next, we have that $X \setminus U$ is closed in $\struct {X, \tau}$. 
Define $f : U \to \hointr 0 \infty$ by:
:$\map f x = \map d {x, X \setminus U}$
for each $x \in U$.
From Point at Distance Zero from Closed Set is Element, we have $\map f x > 0$ for each $x \in U$.
We can therefore define $\widetilde d : U \times U \to \hointr 0 \infty$ by:
:$\ds \map {\widetilde d} {x, y} = \map d {x, y} + \size {\frac 1 {\map f x} - \frac 1 {\map f y} }$
for each $x, y \in U$.
We need to show that $\widetilde d$ is a metric, is complete and induces $\tau_U$.
Theorem: Primitive of Arccosine of a x

:$\ds \int \arccos a x \rd x = x \arccos a x - \dfrac 1 a \sqrt {1 - a^2 x^2} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \arccos x \rd x
      | r = x \arccos x - \sqrt {1 - x^2} + C
      | c = Primitive of $\arccos x$
}}
{{eqn | ll= \leadsto
      | l = \int \arccos a x \rd x
      | r = \dfrac 1 a \paren {\paren {a x} \arccos a x - \sqrt {1 - \paren {a x}^2} } + C
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = x \arccos a x - \dfrac 1 a \sqrt {1 - a^2 x^2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sequence of Mappings Converges Pointwise iff Converges at Each Point

Let $D$ be a set.
Let $T$ be a topological space.
For each $n \in \N$, let $f_n : D \to T$ be a mapping.
Let $f : D \to T$ also be a mapping.
Then:
:$\sequence {f_n}$ converges pointwise to $f$
{{iff}}
:for every $x \in D$, $\sequence {\map {f_n} x}$ converges to $\map f x$

Proof:
Follows from Sequence on Product Space Converges to Point iff Projections Converge to Projections of Point, with:
:$I = D$
:$\forall i \in D: T_i = T$
{{qed}}
Theorem: Center of Mass of Uniform Solid Hemisphere

Let $\BB$ be a solid hemisphere of radius $r$ of uniform density.
Then the center of mass of $\BB$ is the point $\dfrac {3 r} 8$ from the center of $\BB$ along the radius of $\BB$ perpendicular to the base of $\BB$.

Proof:
Let $V$ be the volume of $\BB$.
Let the density $\map \rho {\mathbf r}$ of $\BB$ be a constant $\rho$.
Let $M = \rho V$ be the total mass of $\BB$.
Let $\mathbf r$ be a position within $V$.
Let the base of the hemisphere lie in the $x y$ plane centered at the origin with all of $\BB$ in the $z \geq 0$ region.
Let $\d V$ be a volume element of $V$ that consists of a disc parallel to and a distance $z$ from the $x y$ plane and centered on the $z$ axis.
Let $r_d$ be the radius of $\d V$.
From Pythagoras' Theorem:
{{begin-eqn}}
{{eqn | l = z^2 + r_d^2
      | r = r^2
}}
{{eqn | ll= \leadsto
      | l = r_d^2
      | r = r^2 - z^2
}}
{{end-eqn}}
By rotational symmetry, the center of mass of $\d V$ is at its center: $\tuple {0, 0, z}$.
So, the center of mass $\bar {\mathbf r}$ of $\BB$ will lie along the $z$ axis.
Let $\bar z$ be the $z$ coordinate of $\bar {\mathbf r}$.
From the definition of the center of mass of a continuous body:
{{begin-eqn}}
{{eqn | l = \bar z
      | r = \frac 1 M \int_V \map \rho z z \rd V
}}
{{eqn | r = \frac 1 {\frac 2 3 \pi r^3 \rho} \int_V \rho z \rd V
      | c = $M = $ half the volume of a sphere times the density
}}
{{eqn | r = \frac 3 {2 \pi r^3} \int_V z \rd V
}}
{{eqn | r = \frac 3 {2 \pi r^3} \int_0^r z \pi r_d^2 \rd z
      | c = Area of Circle
}}
{{eqn | r = \frac 3 {2 r^3} \int_0^r z \paren {r^2 - z^2} \rd z
}}
{{eqn | r = \frac 3 {2 r^3} \int_{r^2}^0 u \paren {-\frac 1 2} \rd u
      | c = $u = r^2 - z^2$ and $\d u = -2 z \rd z$
}}
{{eqn | r = \frac 3 {4 r^3} \int_0^{r^2} u \rd u
      | c = Reversal of Limits of Definite Integral
}}
{{eqn | r = \frac 3 {4 r^3} \intlimits {\frac 1 2 u^2} 0 {r^2}
      | c = Primitive of Power
}}
{{eqn | r = \frac 3 {8 r^3} r^4
}}
{{eqn | r = \frac 3 8 r
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Lattice Isomorphism

Let $L_1 = \struct {A_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ be lattices.
{{TFAE|def=Lattice Isomorphism}}
=== Definition 1 ===
{{:Definition:Lattice Isomorphism/Definition 1}}
=== Definition 2 ===
{{:Definition:Lattice Isomorphism/Definition 2}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\phi : L_1 \to L_2$ be a bijective lattice homomorphism.
{{:Equivalence of Definitions of Lattice Isomorphism/Definition 1 Implies Definition 2}}{{qed|lemma}}