avewright/proofwiki-math huggingface dataset:
Theorem: Relation Between First and Second Form of Binet Form

Let $m \in \R$.
Define:
{{begin-eqn}}
{{eqn | l = \Delta
      | r = \sqrt {m^2 + 4}
}}
{{eqn | l = \alpha
      | r = \frac {m + \Delta} 2
}}
{{eqn | l = \beta
      | r = \frac {m - \Delta} 2
}}
{{end-eqn}}

Proof:
Proof by induction:
Let $\map P n$ be the proposition:
:$U_{n - 1} + U_{n + 1} = V_n$
Theorem: Iteration of Ruelle-Perron-Frobenius Operator/One-Sided Shift Space of Finite Type

Let $\struct {X_\mathbf A ^+, \sigma}$ be a one-sided shift of finite type.
Let $\map C {X _\mathbf A ^+}$ be the complex-valued continuous mapping space.
Let $f \in \map C {X _\mathbf A ^+}$.
Let $\LL_f$ be the Ruelle-Perron-Frobenius operator.
For all $w \in \map C {X _\mathbf A ^+}$, $n \in \N$ and $x \in X _\mathbf A ^+$, we have:
:$\ds \map {\LL_f^n w} x = \sum_{y \mathop \in \map {\sigma^{-n} } x} e^{\map {f_n} y} \map w y $
where
:$f_n := f + f \circ \sigma + \cdots + f \circ \sigma ^{n-1}$
:$\map {\sigma ^{-n} } x$ denotes the preimage of $x$ under $\sigma^n$, i.e.:
::$\map {\sigma^{-n} } x = \set {\sequence {i_1, i_2, \ldots , i_n, x_0, x_1, \ldots} : \map {\mathbf A} {i_1, i_2} = \cdots = \map {\mathbf A} {i_{n-1}, i_n} = \map {\mathbf A} {i_n, x_0} = 1}$

Proof:
{{ProofWanted}}
Category:Ergodic Theory
Category:Functional Analysis
9bc7b9n5md2vlapnejy9oubspavkczu
Theorem: Neighborhood in Open Subspace

Let $T = \struct{S, \tau}$ be a topological space.
Let $U \subseteq S$ be an open subset.
Let $\tau_U$ denote the subspace topology on $U$.
Let $s \in U$
Let $N \subseteq U$ be a subset.
Then:
:$N$ is a neighborhood of $s$ in $\struct{U, \tau_U}$ 
{{iff}}
:$N$ is a neighborhood of $s$ in $\struct{S, \tau}$

Proof:
=== Necessary Condition ===
Let $N$ be a neighborhood of $s$ in $\struct{U, \tau_U}$.
By definition of neighborhood:
:$\exists V \in \tau_U : x \in V \subseteq N$
From Open Set in Open Subspace:
:$V \in \tau$
Hence:
:$\exists V \in \tau : x \in V \subseteq N$
It follows that $N$ is a neighborhood of $s$ in $\struct{S, \tau}$ by definition.
{{qed|lemma}}
Theorem: Derivative of Matrix Exponential

:$\dfrac \d {\d t} e^{\mathbf A t} = \mathbf A e^{\mathbf A t}$

Proof:
From the definition of the matrix exponential, $e^{\mathbf A t}$ is defined as being the square matrix $X$ with the properties:
:$(1): \quad \map {\dfrac \d {\d t} } X = \mathbf A X$
:$(2): \quad \map X {\mathbf 0_n} = \mathbf I_n$
The result follows directly;
{{qed}}
Category:Matrix Exponential
Category:Derivatives
7fw40r9rivpj9wt9h1snb8qjcijxr16
Theorem: Determinant of Matrix Exponential is Non-Zero

:$\det e^{\mathbf A t} \ne 0$
where $\det$ denotes the determinant.

Proof:
{{ProofWanted|The below outlines an approach. Details need to be completed.}}
The linear system $x' = \mathbf A x$ has $n$ linearly independent solutions.
Putting together these solutions as columns in a matrix creates a matrix solution to the differential equation, considering the initial conditions for the matrix exponential.
From Existence and Uniqueness Theorem for 1st Order IVPs, this solution is unique.
By linear independence of its columns:
:$\det e^{\mathbf A t} \ne 0$
{{refactor|The following is a separate proof and would need to be added to another transcluded page.|level = basic}}
The nonzero determinant property also follows as a corollary to Liouville's Theorem (Differential Equations).
Category:Matrix Exponential
Category:Determinants
lwtw322zx44z6vijl8ov1mnere846tg
Theorem: Same-Matrix Product of Matrix Exponentials

:$e^{\mathbf A t} e^{\mathbf A s} = e^{\mathbf A \paren {t + s} }$

Proof:
Let
:$\map \Phi t = e^{\mathbf A t} e^{\mathbf A s} - e^{\mathbf A \paren {t + s} }$
for some fixed $s \in \R$.
From Derivative of Matrix Exponential:
{{begin-eqn}}
{{eqn | l = \map {\Phi'} t
      | r = \mathbf A e^{\mathbf A t} e^{\mathbf A s} - \mathbf A e^{\mathbf A \paren {t + s} }
      | c = 
}}
{{eqn | r = \mathbf A \paren {e^{\mathbf A t} e^{\mathbf A s} - e^{\mathbf A \paren {t + s} } }
      | c = 
}}
{{eqn | r = \mathbf A \map \Phi t
      | c = 
}}
{{end-eqn}}
Since $\map \Phi 0 = e^{\mathbf A s} - e^{\mathbf A s} = 0$, it follows that:
:$\map \Phi t = e^{\mathbf A t} \map \Phi 0 = 0$
independent of $s$.
Hence the result.
{{qed}}
Category:Matrix Exponential
7i91wrnctthnkg2rfseiaqtur6q235q
Theorem: Inverse of Matrix Exponential

:$\paren {e^{\mathbf A t} }^{-1} = e^{-\mathbf A t}$
where $\paren {e^{\mathbf A t} }^{-1}$ denotes the inverse of $e^{\mathbf A t}$.

Proof:
{{begin-eqn}}
{{eqn | l = e^{\mathbf A t} e^{-\mathbf A t}
      | r = e^{\mathbf A \paren {t - t} }
      | c = Same-Matrix Product of Matrix Exponentials
}}
{{eqn | r = e^{\mathbf 0}
      | c = {{Defof|Matrix Scalar Product}}: $\mathbf A 0 = \mathbf 0$
}}
{{eqn | r = \mathbf I
      | c = Matrix Exponential of Zero Matrix
}}
{{end-eqn}}
where:
:$\mathbf 0$ denotes the zero matrix of the appropriate order
:$\mathbf I$ denotes the identity matrix of the appropriate order.
{{explain|We need to establish that $e^{\mathbf 0} {{=}} \mathbf I$}}
Similarly:
:$e^{-\mathbf A t} e^{\mathbf A t} = \mathbf I$
Hence the result by definition of inverse matrix.
{{qed}}
Category:Matrix Exponential
Category:Inverse Matrices
qc9xaizscwvx796iwbzjr65vkri6ari
Theorem: Product with Matrix Exponential of Commutative Matrices

Let $\mathbf A \mathbf B = \mathbf B \mathbf A$.
Then:
:$e^{\mathbf A t} \mathbf B = \mathbf B e^{\mathbf A t}$

Proof:
Let:
:$\map \Phi t = e^{\mathbf A t} \mathbf B - \mathbf B e^{\mathbf A t}$
{{ProofWanted|and then follow the same program outlined in the Same-Matrix Product of Matrix Exponentials proof.}}
Category:Matrix Exponential
Category:Commutativity
r8p9y8xiyh8n22f197qlkg6cgyx4ly3
Theorem: Matrix Exponential of Sum of Commutative Matrices

Let $\mathbf A \mathbf B = \mathbf B \mathbf A$.
Then:
:$e^{\mathbf A t} e^{\mathbf B t} = e^{\paren {\mathbf A + \mathbf B} t}$

Proof:
Let:
:$\map \Phi t = e^{\mathbf A t} e^{\mathbf B t} - e^{\paren {\mathbf A + \mathbf B} t}$
{{ProofWanted|and then follow the same program outlined in the Same-Matrix Product of Matrix Exponentials proof.}}
Theorem: Series Expansion of Matrix Exponential

:$\ds e^{\mathbf A t} = \sum_{n \mathop = 0}^\infty \frac {t^n} {n!} \mathbf A^n$

Proof:
{{ProofWanted|Differentiating the series term-by-term and evaluating at $t {{=}} 0$ proves the series satisfies the same definition as the matrix exponential, and hence by uniqueness is equal.}}
{{finish|It needs to be shown that it converges and can be differentiated termwise}}
Theorem: Algebra of Sets is Closed under Intersection

Let $S$ be a set.
Let $\RR$ be an algebra of sets on $S$.
Then:
:$\forall A, B \in S: A \cap B \in \RR$

Proof:
By definition $2$ of Algebra of Sets:
:$\RR$ is a ring of sets with a unit.
By definition $1$ of Ring of Sets:
{{begin-axiom}}
{{axiom | n = \text {RS} 2_1
        | lc= Closure under Intersection:
        | q = \forall A, B \in \RR
        | m = A \cap B \in \RR
}}
{{end-axiom}}
{{qed}}
Theorem: Algebra of Sets is Closed under Intersection

Let $S$ be a set.
Let $\RR$ be an algebra of sets on $S$.
Then:
:$\forall A, B \in S: A \cap B \in \RR$

Proof:
By definition $1$ of algebra of sets, we have that:
{{begin-axiom}}
{{axiom | n = \text {AS} 2
        | lc= Closure under Union:
        | q = \forall A, B \in \RR
        | m = A \cup B \in \RR
}}
{{axiom | n = \text {AS} 3
        | lc= Closure under Complement Relative to $S$:
        | q = \forall A \in \RR
        | m = \relcomp S A \in \RR
}}
{{end-axiom}}
Thus:
{{begin-eqn}}
{{eqn | l = A, B
      | o = \in
      | r = \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \relcomp S A \cup \relcomp S B
      | o = \in
      | r = \RR
      | c = {{Defof|Algebra of Sets}}: $\text {AS} 2$ and $\text {AS} 3$
}}
{{eqn | ll= \leadsto
      | l = \relcomp S {A \cap B}
      | o = \in
      | r = \RR
      | c = De Morgan's Laws: Complement of Intersection
}}
{{eqn | ll= \leadsto
      | l = A \cap B
      | o = \in
      | r = \RR
      | c = {{Defof|Algebra of Sets}}: $\text {AS} 3$
}}
{{end-eqn}}
{{qed}}
Theorem: Algebra of Sets is Closed under Set Difference

Let $S$ be a set.
Let $\RR$ be an algebra of sets on $S$.
Then:
:$\forall A, B \in S: A \setminus B \in \RR$

Proof:
By definition $1$ of algebra of sets, we have that:
{{begin-axiom}}
{{axiom | n = \text {AS} 3
        | lc= Closure under Complement Relative to $S$:
        | q = \forall A \in \RR
        | m = \relcomp S A \in \RR
}}
{{end-axiom}}
Thus:
{{begin-eqn}}
{{eqn | l = A, B
      | o = \in
      | r = \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A \cap \relcomp S B
      | o = \in
      | r = \RR
      | c = {{Defof|Algebra of Sets}}: $\text {AS} 3$ and Algebra of Sets is Closed under Intersection
}}
{{eqn | ll= \leadsto
      | l = A \setminus B
      | o = \in
      | r = \RR
      | c = Set Difference as Intersection with Relative Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Algebra of Sets contains Underlying Set

Let $S$ be a set.
Let $\RR$ be an algebra of sets on $S$.
Then:
:$S \in \RR$

Proof:
By definition $1$ of algebra of sets, we have that:
{{begin-axiom}}
{{axiom | n = \text {AS} 1
        | lc= Unit:
        | m = S \in \RR
}}
{{end-axiom}}
The result is hence immediate.
{{qed}}
Theorem: Algebra of Sets contains Underlying Set

Let $S$ be a set.
Let $\RR$ be an algebra of sets on $S$.
Then:
:$S \in \RR$

Proof:
By definition $1$ of algebra of sets, we have that:
{{begin-axiom}}
{{axiom | n = \text {AS} 2
        | lc= Closure under Union:
        | q = \forall A, B \in \RR
        | m = A \cup B \in \RR
}}
{{axiom | n = \text {AS} 3
        | lc= Closure under Complement Relative to $S$:
        | q = \forall A \in \RR
        | m = \relcomp S A \in \RR
}}
{{end-axiom}}
We have that $\RR \ne \O$ and so:
:$\exists A \subseteq S: A \in \RR$
Then:
{{begin-eqn}}
{{eqn | l = \relcomp S A
      | o = \in
      | r = \RR
      | c = {{Defof|Algebra of Sets}}: $\text {AS} 3$
}}
{{eqn | ll= \leadsto
      | l = \relcomp S A \cup A
      | o = \in
      | r = \RR
      | c = {{Defof|Algebra of Sets}}: $\text {AS} 2$
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \in
      | r = \RR
      | c = Union with Relative Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Generator of Module

Let $R$ be a ring.
Let $M$ be an $R$-module.
Let $S \subseteq M$ be a subset of $M$.
{{TFAE|def = Generator of Module}}

Proof:
=== Definition 1 implies Definition 2 ===
By definition of generated submodule, it follows that:
:$\ds M := \bigcap \set { M' \subseteq M : S \subseteq M', \textrm {$M'$ is a submodule of $M$} }$
Suppose that $M'$ is a proper submodule of $M$ such that $S \subseteq M'$.
It follows that there exists $x \in M \setminus M'$.
Hence, $x \notin M'$.
By definition of intersection, it follows that:
:$\ds x \notin \bigcap \set { M' \subseteq M : S \subseteq M', \textrm {$M'$ is a submodule of $M$} } = M$
This is a contradiction.
Hence, the condition of Definition 2 is satisfied.
{{qed|lemma}}
Theorem: Null Sequence induces Neighborhood Basis of Closed Sets 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 closed $\epsilon$-ball of $a$ in $M$.
Then:
:$\NN_{\sequence {x_n} } = \set{\map {B^-_{x_n} } a : n \in \N}$ is a neighborhood basis of $a$ consisting of closed sets.

Proof:
From Closed Ball in Metric Space is Closed Neighborhood:
:every element of $\NN_{\sequence {x_n} }$ is an closed neighborhood of $a$.
By definition of closed neighborhood of $a$:
:every element of $\NN_{\sequence {x_n} }$ is an neighborhood of $a$ and a closed set.
Let $U$ be an open neighborhood of $a$.
By definition of an open set, there exists a strictly positive real number $\epsilon$:
:$\map {B_\epsilon} a \subseteq U$
From Open Ball contains Strictly Smaller Closed Ball:
:$\map {B_{\epsilon/2}^-} a \subseteq \map {B_\epsilon} a$
By definition of a real null sequence:
:$\exists N \in \N : \forall n > N : \size {x_n} < \dfrac \epsilon 2$
Let $m = N + 1$.
Then $\size {x_m} < \dfrac \epsilon 2$.
Since $x_m > 0$ then $x_m = \size {x_m} < \dfrac \epsilon 2 $, and so:
:$\map {B_{x_m}^- } a \subseteq \map {B_{\epsilon/2}^-} a \subseteq \map {B_\epsilon} a \subseteq U$
The result follows from Subset Relation is Transitive.
{{qed}}
Category:Metric Spaces
qvfds3lrj95i3kmc7wibphg1ammya7v
Theorem: Closed Ball is Simply Connected

Let $\struct {V, \norm {\,\cdot\,} }$ be a normed vector space over $\R$ or $\C$.
Let $d: V \times V \to \R_{\ge 0}$ be the metric induced by the norm $\norm {\,\cdot\,}$ on $V$.
Let $\tau$ be the the topology on $V$ induced by the metric $d$.
Let $v \in V$ and $\epsilon \in \R_{>0}$.
Let $\map {B_\epsilon^-} v$ be the closed $\epsilon$-ball of $v$.
Let $\tau_B$ be the subspace topology on $\map {B_\epsilon} v$ induced by $\tau$.
Then $\struct{ \map {B_\epsilon^-} v, \tau_B }$ is simply connected.

Proof:
Normed Vector Space is Hausdorff Topological Vector Space shows that $\struct {V, \tau}$ is a topological vector space.
The result now follows from Closed Ball is Convex Set and Convex Set is Simply Connected.
{{qed}}
Category:Normed Vector Spaces
Category:Closed Balls
Category:Simply Connected Spaces
axs5o7vf121ocwb09obc6gn4fn60cbc
Theorem: Closed Ball in Metric Space is Closed Neighborhood

Let $M = \struct {A, d}$ be a metric space.
Let $x \in A$.
Let $\epsilon \in \R_{>0}$.
Let $\map {B_\epsilon^-} x$ be the closed $\epsilon$-ball of $x$ in $M$.
Then $\map {B_\epsilon^-} x$ is a closed neighborhood of $x$ in $M$.

Proof:
From Closed Ball contains Smaller Open Ball:
:$\map {B_\epsilon} x \subseteq \map {B_\epsilon^-} x$
where $\map {B_\epsilon} x$ denotes the open $\epsilon$-ball of $x$ in $M$.
Hence $\map {B_\epsilon^-} x$ is a neighborhood of $x$ by definition.
From Closed Ball is Closed in Metric Space:
:$\map {B_\epsilon^-} x$ is closed in $M$
It follows that $\map {B_\epsilon^-} x$ is a closed neighborhood of $x$ in $M$ by definition.
{{qed}}
Category:Closed Sets (Metric Spaces)
Category:Neighborhoods
7w8crp6h9vzqv1gmf9zs3pyiwixcxs4
Theorem: Koopman Operator is Isometry

Let $\struct {X, \BB, \mu, T}$ be a measure-preserving dynamical system.
Let $\map {L^2_\C} \mu$ be the complex-valued $L^2$ space of $\mu$.
Let $U_T : \map {L^2_\C} \mu \to \map {L^2_\C} \mu$ of $T$ be the Koopman operator.
Let $\innerprod \cdot \cdot$ denote the inner product on $\map {L^2_\C} \mu$, i.e.
:$\ds \forall f, g \in \map {L^2_\C} \mu : \innerprod f g := \int \overline f g \rd \mu$
where $\overline f$ denotes the complex conjugate of $f$.
Then $U_T$ is isometry on the $L^2$ Hilbert space $\struct {\map {L^2_\C} \mu, \innerprod \cdot \cdot}$.
That is:
:$\ds \forall f, g \in \map {L^2_\C} \mu : \innerprod {U_T f} {U_T g} = \innerprod f g$

Proof:
Let $f, g \in \map {L^2_\C} \mu $.
Then:
{{begin-eqn}}
{{eqn | l = \innerprod {U_T f} {U_T g}
      | r = \int  {\overline {U_T f} } \; {U_T g} \rd \mu
}}
{{eqn | r = \int {\overline {f \circ T} } \; {g \circ T} \rd \mu
      | c = {{Defof|Koopman Operator on Complex L-2 Space|Koopman operator}}
}}
{{eqn | r = \int {\overline f} \circ T \; {g \circ T} \rd \mu
      | c = as $\map {\overline {f \circ T} } x = \overline {\map f {T x} } = \map {\overline f} {T x} = \map { {\overline f} \circ T} x$
}}
{{eqn | r = \int \paren { {\overline f} g} \circ T \rd \mu
}}
{{eqn | r = \int {\overline f} g \rd \mu
      | c = {{Defof|Measure-Preserving Transformation}}
}}
{{eqn | r = \innerprod f g
}}
{{end-eqn}}
{{qed}}
Category:Operator Theory
2x5tfrule2bx82wnz7umpa945ahd3rx
Theorem: Locally Euclidean Space is Locally Connected

Let $M$ be a locally Euclidean space of some dimension $d$.
Then $M$ is locally connected.

Proof:
Follows from:
* Locally Euclidean Space is Locally Path-Connected
* Locally Path-Connected Space is Locally Connected
{{qed}}
Category:Locally Euclidean Spaces
ku9zokev8ccp0o5fjm382r1uxhhdij5
Theorem: Open Ball in Normed Vector Space is Path-Connected

Let $V$ be a normed vector space with norm $\norm {\,\cdot\,}$ over $\R$ or $\C$.
An open ball in the metric induced by $\norm {\,\cdot\,}$ is path-connected.

Proof:
Follows from:
* Open Ball is Convex Set
* Normed Vector Space is Hausdorff Topological Vector Space
* Convex Set is Path-Connected
{{qed}}
Category:Normed Vector Spaces
Category:Open Balls
Category:Path-Connected Spaces
5ide26bnfbtclec4vej8504r9z9jdg6
Theorem: Closed Ball is Path-Connected

Let $V$ be a normed vector space with norm $\norm {\,\cdot\,}$ over $\R$ or $\C$.
A closed ball in the metric induced by $\norm {\,\cdot\,}$ is path-connected.

Proof:
Follows from:
* Closed Ball is Convex Set
* Normed Vector Space is Hausdorff Topological Vector Space
* Convex Set is Path-Connected
{{qed}}
Category:Normed Vector Spaces
Category:Closed Balls
Category:Path-Connected Metric Spaces
8pek86aqhq85ffzxuuvbnyel1hy3rvq
Theorem: Open Ball in Normed Vector Space is Connected

Let $V$ be a normed vector space with norm $\norm {\,\cdot\,}$ over $\R$ or $\C$.
An open ball in the metric induced by $\norm {\,\cdot\,}$ is connected.

Proof:
Follows from:
:Open Ball in Normed Vector Space is Path-Connected
:Path-Connected Space is Connected.
{{qed}}
Category:Open Balls
Category:Connected Topological Spaces
Category:Normed Vector Spaces
t90k3juviw6h8incconezi6gs4n82xp
Theorem: Closed Ball is Connected

Let $V$ be a normed vector space with norm $\norm {\,\cdot\,}$ over $\R$ or $\C$.
A closed ball in the metric induced by $\norm {\,\cdot\,}$ is connected.

Proof:
Follows from:
* Closed Ball is Path-Connected
* Path-Connected Space is Connected
{{qed}}
Category:Closed Balls
Category:Connected Topological Spaces
Category:Normed Vector Spaces
5jupmxqpzk0kxg1xwz3jkxk79c8u3xo
Theorem: Topological Manifold is Locally Connected

Let $M$ be a topological manifold.
Then $M$ is a locally connected space.

Proof:
By definition of manifold:
:$M$ is a locally Euclidean space
The result follows from Locally Euclidean Space is Locally Connected
{{qed}}
Category:Topological Manifolds
Category:Locally Connected Spaces
cj89v0cgwqy7p3ezbnqjx60klfmgtbe
Theorem: Topological Manifold is Locally Compact

Let $M$ be a topological manifold.
Then $M$ is a locally compact space.

Proof:
By definition of manifold:
:$M$ is a locally Euclidean space.
The result follows from Locally Euclidean Space is Locally Compact.
{{qed}}
Category:Topological Manifolds
Category:Locally Compact Spaces
7gi7qvjnqywoyzelaubwtao4f7ts6or
Theorem: Napoleon's Theorem

Let $\triangle ABC$ be an arbitrary triangle.
Let $\triangle ABF$, $\triangle BCD$ and $\triangle ACE$ be equilateral triangles constructed on $AB$, $BC$ and $AC$ respectively on the exterior of $\triangle ABC$.
Let $O_1$, $O_2$ and $O_3$ be the incenters of $\triangle ABF$, $\triangle BCD$ and $\triangle ACE$.
Then $\triangle O_1 O_2 O_3$ is an equilateral triangle.
:400px

Proof:
For simplicity of notation, we relabel the incenters $O_1, O_2, O_3$ as $P, Q, R$.
400px
By Line from Vertex of Triangle to Incenter is Angle Bisector:
:$CQ$ bisects $\angle ACE$
:$CP$ bisects $\angle BCD$
Given:
:$\angle ACE = \angle BCD = 60^{\circ}$
Since $\triangle CBD$ and $\triangle ACE$ are both equilateral, the four smaller angles are all equal to $30^{\circ}$:
:$\angle ACQ = \angle QCE = \angle BCP = \angle PCD = 30^{\circ}$
By addition:
:$\angle BCE = \angle BCA + 60^{\circ}$
But also by addition:
:$\angle PCQ = \angle BCA + 60^{\circ}$
So by Common Notion 1:
:$\angle BCE = \angle PCQ$
Let $\angle BCE = \angle PCQ = \gamma$
By Law of Cosines:
:$(1) \ PQ^2 = CP^2 + CQ^2 - 2 \ CP \cdot CQ \cdot \cos {\gamma}$
By the same argument:
:$\angle BAE = \angle RAQ = \angle BAC + 60^{\circ}$
Let $\angle BAE = \angle RAQ = \alpha$.
We also can obtain $CP$ and $CQ$ in terms of the sides of the original triangle.
Draw the altitude from $Q$ to $AC$.
Since $\angle ACQ = 30^{\circ}$:
:$CA/2 : CQ = \map \cos {30^{\circ}} = \dfrac {\sqrt{3}} 2$
Simplifying:
:$CA = \sqrt{3} CQ$
:$CA^2 = 3 CQ^2$
In the same way:
:$BC/2 : CP = \map \cos {30^{\circ}} = \dfrac {\sqrt{3}} 2$
Simplifying:
:$BC = \sqrt{3} CP$
:$BC^2 = 3 CP^2$
Multiplying:
:$3 CP \cdot CQ = BC \cdot CA$
Multiply (1) by $3$:
:$3PQ^2 = 3CP^2 + 3CQ^2 - 2 \cdot 3 \cdot CP \cdot CQ \cdot \cos {\gamma}$
and substitute:
:$(2) \ 3PQ^2 = BC^2 + CA^2 - 2 BC \cdot CA \cdot \cos {\gamma}$
Recall that $\alpha = \angle BAE$.
We can make all the same arguments for $QR$ so by symmetry:
:$(3) \ 3 QR^2 = AB^2 + AC^2 - 2 AB \cdot AC \cos \alpha$
Finally consider $BE$ as part of $\triangle ABE$.  
By Law of Cosines:
:$BE^2 = AB^2 + AE^2 - 2 AB \cdot AE \cdot \cos \alpha$
But $AE = AC$ so:
:$(4) \ BE^2 = AB^2 + AC^2 - 2 AB \cdot AC \cdot \cos \alpha$
Consider $BE$ as part of $\triangle BCE$.  
By Law of Cosines:
:$BE^2 = BC^2 + CE^2 - 2 BC \cdot CE \cdot \cos \gamma$
Since $AC = CE$:
:$(5) \ BE^2 = BC^2 + AC^2 - 2 BC \cdot AC \cdot \cos \gamma$
By Common Notion 1, since the LHS of (4) and (5) are equal, the RHS are also equal.
The RHS of (4) is the same as the RHS of (3).
The RHS of (5) is the same as the RHS of (2).
So then too by Common Notion 1 the LHS of (2) and (3) are equal:
:$3 \cdot PQ^2 = 3 \cdot QR^2$
Simplifying:
:$PQ = QR$
We can make the same argument for any pair of points from $P, Q, R$.
Therefore:
:$PQ = QR = PR$
$\triangle PQR$ satisfies the definition of an equilateral triangle.
{{qed}}
Theorem: Napoleon's Theorem/Variant 1

Let $\triangle ABC$ be an arbitrary triangle.
Let $\triangle ABF$, $\triangle BCD$ and $\triangle ACE$ be equilateral triangles constructed on $AB$, $BC$ and $AC$ respectively toward the interior of $\triangle ABC$.
Let $O_1$, $O_2$ and $O_3$ be the incenters of $\triangle ABF$, $\triangle ACE$ and $\triangle BCD$ respectively.
Then $\triangle O_1 O_2 O_3$ is an equilateral triangle.
:400px

Proof:
=== {{Lemma|Napoleon's Theorem|1}} ===
{{:Napoleon's Theorem/Lemma 1}}{{qed|lemma}}
Theorem: Suffix of String is Substring

Let $S$ be a string.
Let $T$ be a suffix of $S$.
Then $T$ is a substring of $S$.

Proof:
By definition of substring, there exists a string $T'$ such that:
:$S = T'T$
Hence $S$ is the concatenation of the null string, $T'$, and $T$.
Thus by definition of substring, $T$ is a substring of $S$.
{{qed}}
Category:Collations
m7zl93m6ij10z0sagrr55bea0q06p37
Theorem: Null String is Identity Element for Concatenation Operator

Let $\AA$ be an alphabet of symbols.
Let $\WW$ denote the set of words in $\AA$.
Let $\epsilon$ denote the null string.
Let $C: \WW \times \WW \to \WW$ denote the concatenation operator on $\WW$:
:$\forall A, B \in \WW: \map C {A, B} := A B$
Then $\epsilon$ is the identity element for $C$.

Proof:
As $\epsilon$ is the null string:
:$\map C {\epsilon, A}$
{{begin-eqn}}
{{eqn | q = \forall A \in \WW
      | l = \map C {\epsilon, A}
      | r = \epsilon A
      | c = Definition of $C$
}}
{{eqn | r = A
      | c = {{Defof|Null String}}
}}
{{eqn | r = A \epsilon
      | c = {{Defof|Null String}}
}}
{{eqn | r = \map C {A, \epsilon}
      | c = Definition of $C$
}}
{{end-eqn}}
Hence the result by definition of identity element.
{{qed}}
Theorem: Equivalence of Definitions of Generator of Unitary Module

Let $R$ be a ring with unity.
Let $M$ be a unitary $R$-module.
Let $S \subseteq M$ be a subset.
{{TFAE|def = Generator of Unitary Module}}

Proof:
=== Definition by linear combinations implies Definition by intersection of submodules ===
Theorem: Convex Set is Path-Connected

Let $V$ be a topological vector space over $\R$ or $\C$.
Every convex subset of $V$ is path-connected.

Proof:
The result follows from:
:Convex Set is Star Convex Set
:Star Convex Set is Path-Connected
{{qed}}
Category:Topological Vector Spaces
Category:Convex Sets (Vector Spaces)
Category:Path-Connected Spaces
f54ufyli0mhk8a11ngff8ysyi70ewrb