avewright/proofwiki-math huggingface dataset:
Theorem: Composition of Symmetric Relation with Itself is Union of Products of Images

Let $\RR$ be a symmetric relation on a set $S$.
Then:
:$\RR \circ \RR = \ds \map {\bigcup_{s \mathop \in S} } {\map \RR s \times \map \RR s}$
where
:$\RR \circ \RR$ is the composition of $\RR$ with itself
:$\map \RR s$ is the image of $s$ under $\RR$
:$\map \RR s \times \map \RR s$ is the Cartesian product of $\map \RR s$ with itself

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \tuple {x, y} \in \RR \circ \RR
      | o = \leadstoandfrom
      | r = \exists s \in S : \tuple {x, s}, \tuple {s, y} \in \RR
      | c = {{Defof|Composite Relation}}
}}
{{eqn | o = \leadstoandfrom
      | r = \exists s \in S : \tuple {s, x}, \tuple {s, y} \in \RR
      | c = {{Defof|Symmetric Relation}}
}}
{{eqn | o = \leadstoandfrom
      | r = \exists s \in S : x, y \in \map \RR s
      | c = {{Defof|Image of Element under Relation}}
}}
{{eqn | o = \leadstoandfrom
      | r = \exists s \in S : \tuple {x, y} \in \map \RR s \times \map \RR s
      | c = {{Defof|Cartesian Product}}
}}
{{eqn | o = \leadstoandfrom
      | r = \tuple{x,y} \in \map {\bigcup_{s \mathop \in S} } {\map \RR s \times \map \RR s}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
{{qed}}
Category:Set Union
Category:Cartesian Product
Category:Symmetric Relations
tbepbthskz4ltshc9iwzqmwx94fry47
Theorem: Intersection of Neighborhood of Diagonal with Inverse is Neighborhood

Let $T = \struct{X, \tau}$ be a topological space.
Let $\tau_{X \times X}$ denote the product topology on the cartesian product $X \times X$.
Let $R$ be a neighborhood of the diagonal $\Delta_X$ of $X \times X$ in the product space $\struct{X \times X, \tau_{X \times X}}$.
Let $R^{-1}$ denote the inverse relation of $R$ where $R$ is viewed as a relation on $X \times X$. 
Then:
:$R \cap R^{-1}$ is a neighborhood of $\Delta_X$ in $\struct{X \times X, \tau_{X \times X}}$.

Proof:
From Set is Neighborhood of Subset iff Neighborhood of all Points of Subset:
:$\forall \tuple{x, x} \in \Delta_X : R$ is a neighborhood of $\tuple{x, x}$
From Inverse of Neighborhood of Diagonal Point is Neighborhood:
:$\forall \tuple{x, x} \in \Delta_X : R^{-1}$ is a neighborhood of $\tuple{x, x}$
From Intersection of Neighborhoods in Topological Space is Neighborhood
:$\forall \tuple{x, x} \in \Delta_X : R \cap R^{-1}$ is a neighborhood of $\tuple{x, x}$
From Set is Neighborhood of Subset iff Neighborhood of all Points of Subset:
:$R \cap R^{-1}$ is a neighborhood of $\Delta_X$ in $\struct{X \times X, \tau_{X \times X}}$
{{qed}}
Category:Neighborhoods
Category:Diagonal Relation
Category:Relations
cex6gk5n1m4nscv54s8m899vaet6gp3
Theorem: Inverse of Neighborhood of Diagonal Point is Neighborhood

Let $T = \struct{X, \tau}$ be a topological Space.
Let $\tau_{X \times X}$ denote the product topology on the cartesian product $X \times X$.
Let $x \in X$.
Let $R$ be a neighborhood of $\tuple{x,x}$ in the product space $\struct{X \times X, \tau_{X \times X}}$.
Let $R^{-1}$ denote the inverse relation of $R$ where $R$ is viewed as a relation on $X \times X$. 
Then:
:$R^{-1}$ is a neighborhood of $\tuple{x,x}$ in $\struct{X \times X, \tau_{X \times X}}$.

Proof:
By definition of neighborhood:
:$\tuple{x, x} \in R$
By definition of product topology:
:$\BB = \set {V_1 \times V_2: V_1, V_2 \in \tau}$ is a basis for $\tau_{X \times X}$
From Characterization of Neighborhood by Basis:
:$\exists V_1, V_2 \in \tau : \tuple{x, x} \in V_1 \times V_2 : V_1 \times V_2 \subseteq R$
By definition of symmetric relation:
:$\tuple{x, x} \in V_2 \times V_1 : V_2 \times V_1 \subseteq R^{-1}$
By definition of product topology:
:$V_2 \times V_1 \in \tau_{X \times X}$
Hence $R^{-1}$ is a neighborhood $\tuple{x, x}$ by definition.
{{qed}}
Category:Neighborhoods
Category:Inverse Relations
ni0ml0ojzpr30bz0yfltirdllen2vod
Theorem: Cauchy's Inequality/Vector Form

Let $\mathbf a$ and $\mathbf b$ be vectors in a vector space $V$.
Then:
:$\paren {\mathbf a \cdot \mathbf b}^2 \le \paren {\mathbf a \cdot \mathbf a} \paren {\mathbf b \cdot \mathbf b}$
where $\cdot$ denotes dot product.

Proof:
Let us express $\mathbf a$ and $\mathbf b$ in component form:
{{begin-eqn}}
{{eqn | l = \mathbf a
      | o = :=
      | r = \sum_{i \mathop = 1}^n a_i \mathbf e_i
}}
{{eqn | l = \mathbf b
      | o = :=
      | r = \sum_{i \mathop = 1}^n b_i \mathbf e_i
}}
{{end-eqn}}
where the ordered $n$-tuple $\tuple {\mathbf e_1, \mathbf e_2, \ldots, \mathbf e_n}$ is the  standard ordered basis of $V$.
Then we have:
{{begin-eqn}}
{{eqn | l = \paren {\mathbf a \cdot \mathbf b}^2
      | r = \paren {\sum_{i \mathop = 1}^n a_i b_i}^2
      | c = {{Defof|Dot Product|subdef = General Context}}
}}
{{eqn | o = \le
      | r = \paren {\sum_{i \mathop = 1}^n {a_i}^2} \paren {\sum_{i \mathop = 1}^n {b_i}^2}
      | c = Cauchy's Inequality
}}
{{eqn | o = \le
      | r = \paren {\mathbf a \cdot \mathbf a} \paren {\mathbf b \cdot \mathbf b}
      | c = {{Defof|Dot Product|subdef = General Context}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hölder's Inequality for Sums/Formulation 1

Let $\mathbf x$ and $\mathbf y$ denote the vectors consisting of the sequences:
:$\mathbf x = \sequence {x_n} \in {\ell^p}_\GF$
:$\mathbf y = \sequence {y_n} \in {\ell^q}_\GF$
where ${\ell^p}_\GF$ denotes the $p$-sequence space in $\GF$.
Let $\norm {\mathbf x}_p$ denote the $p$-norm of $\mathbf x$.
Then:
:$\mathbf x \mathbf y \in {\ell^1}_\GF$
and:
:$\norm {\mathbf x \mathbf y}_1 \le \norm {\mathbf x}_p \norm {\mathbf y}_q$
where:
:$\mathbf x \mathbf y := \sequence {x_n y_n}_{n \mathop \in \N}$
:$\norm {\mathbf x \mathbf y}_1$ is the '''$1$-norm''', also known as the '''taxicab norm'''.

Proof:
Define:
{{begin-eqn}}
{{eqn | l = \mathbf u
      | r = \sequence {u_n}
      | rr= = \dfrac {\mathbf x} {\norm {\mathbf x}_p}
      | c = 
}}
{{eqn | l = \mathbf v
      | r = \sequence {v_n}
      | rr= = \dfrac {\mathbf y} {\norm {\mathbf y}_q}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | q = 
      | l = \norm {\mathbf u}_p
      | r = \norm {\dfrac {\mathbf x} {\norm {\mathbf x}_p} }
      | c = 
}}
{{eqn | r = \paren {\sum_{n \mathop = 0}^\infty \size {\dfrac {x_n} {\norm {\mathbf x}_p} }^p}^{1 / p}
      | c = 
}}
{{eqn | r = \dfrac 1 {\norm {\mathbf x}_p} \paren {\sum_{n \mathop = 0}^\infty \size {x_n}^p}^{1 / p}
      | c = 
}}
{{eqn | r = \dfrac 1 {\norm {\mathbf x}_p} \norm {\mathbf x}_p
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
and similarly:
:$\norm {\mathbf v}_q = 1$
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \N
      | l = \size {u_n v_n}
      | r = \size {u_n} \size {v_n}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | n = 1
      | o = \le
      | r = \dfrac 1 p \size {u_n}^p + \dfrac 1 q \size {v_n}^q
      | c = Young's Inequality for Products: $\size {u_n}$ and $\size {v_n}$ are indeed (strictly) positive
}}
{{end-eqn}}
By the comparison test, it follows that:
{{begin-eqn}}
{{eqn | l = \mathbf u \mathbf v
      | r = \sequence {u_n v_n}
      | rr= \in {\ell^1}_\GF
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \mathbf x \mathbf y
      | r = \norm {\mathbf x}_p \norm {\mathbf y}_q \mathbf u \mathbf v
      | rr= \in {\ell^1}_\GF
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \norm {\mathbf u \mathbf v}_1
      | o = \le
      | r = \dfrac 1 p \norm {\mathbf u}_p + \dfrac 1 q \norm {\mathbf v}_q
      | c = from $(1)$
}}
{{eqn | r = \dfrac 1 p + \dfrac 1 q
      | c = as $\norm {\mathbf u}_p = \norm {\mathbf v}_p = 1$
}}
{{eqn | r = 1
      | c = {{hypothesis}}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \norm {\mathbf x \mathbf y}_1
      | r = \norm {\mathbf x}_p \norm {\mathbf y}_q \norm {\mathbf u \mathbf v}_1
      | c = 
}}
{{eqn | o = \le
      | r = \norm {\mathbf x}_p \norm {\mathbf y}_q
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Hölder's Inequality for Sums/Formulation 2

Let $\sequence {x_n}_{n \mathop \in \N}$ and $\sequence {y_n}_{n \mathop \in \N}$ be sequences in $\GF$ such that $\ds \sum_{k \mathop \in \N} \size {x_k}^p$ and $\ds \sum_{k \mathop \in \N} \size {y_k}^q$ are convergent.
Then:
:$\ds \sum_{k \mathop \in \N} \size {x_k y_k} \le \paren {\sum_{k \mathop \in \N} \size {x_k}^p}^{1 / p} \paren {\sum_{k \mathop \in \N} \size {y_k}^q}^{1 / q}$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = X
      | r = \paren {\sum_{k \mathop \in \N} \size {x_k}^p}^{1 / p}
}}
{{eqn | l = Y
      | r = \paren {\sum_{k \mathop \in \N} \size {y_k}^q}^{1 / q}
}}
{{end-eqn}}
We note that $X, Y \in \R_{\ge 0}$.
Let:
{{begin-eqn}}
{{eqn | q = \forall k \in \N
      | l = u_k
      | r = \dfrac {x_k} X
}}
{{eqn | l = v_k
      | r = \dfrac {y_k} Y
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | q = \forall k \in \N
      | l = \size {u_k v_k}
      | r = \size {u_k} \size {v_k}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | n = 1
      | o = \le
      | r = \dfrac 1 p \size {u_k}^p + \dfrac 1 q \size {v_k}^q
      | c = Young's Inequality for Products
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop \in \N} \size {u_k v_k}
      | o = \le
      | r = \sum_{k \mathop \in \N} \dfrac 1 p \size {u_k}^p + \sum_{k \mathop \in \N} \dfrac 1 q \size {v_k}^q
      | c = summing over $\N$
}}
{{eqn | r = \sum_{k \mathop \in \N} \dfrac 1 p \size {\dfrac {x_k} X}^p + \sum_{k \mathop \in \N} \dfrac 1 q \size {\dfrac {y_k} Y}^q
      | c = substituting for $u_k$ and $v_k$
}}
{{eqn | r = \dfrac 1 p \paren {\dfrac 1 {X^p} \sum_{k \mathop \in \N} \size {x_k}^p} + \dfrac 1 q \paren {\dfrac 1 {Y^q} \sum_{k \mathop \in \N} \size {y_k}^q}
      | c = extracting constants
}}
{{eqn | r = \dfrac 1 p + \dfrac 1 q
      | c = as $\ds X^p = \sum_{k \mathop \in \N} \size {x_k}^p$ and $\ds Y^q = \sum_{k \mathop \in \N} \size {y_k}^q$
}}
{{eqn | r = 1
      | c = {{hypothesis}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | q = \forall k \in \N
      | l = \size {x_k y_k}
      | r = X Y \size {u_k v_k}
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop \in \N} \size {x_k y_k}
      | r = X Y \sum_{k \mathop \in \N} \size {u_k v_k}
      | c = summing over $\N$
}}
{{eqn | r = \paren {\sum_{k \mathop \in \N} \size {x_k}^p}^{1 / p} \paren {\sum_{k \mathop \in \N} \size {y_k}^q}^{1 / q} \sum_{k \mathop \in \N} \size {u_k v_k}
      | c = {{hypothesis}}
}}
{{eqn | o = \le
      | r = \paren {\sum_{k \mathop \in \N} \size {x_k}^p}^{1 / p} \paren {\sum_{k \mathop \in \N} \size {y_k}^q}^{1 / q} \times 1
      | c = from $(1)$
}}
{{eqn | r = \paren {\sum_{k \mathop \in \N} \size {x_k}^p}^{1 / p} \paren {\sum_{k \mathop \in \N} \size {y_k}^q}^{1 / q}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Characterization of Paracompactness in T3 Space/Lemma 13

:there exists a sequence $\sequence{V_n}_{n \in \N}$ of neighborhoods of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} }$:
::$V_0 = V$
::$\forall n \in \N_{> 0} : V_n$ is symmetric as a relation on $X \times X$
::$\forall n \in \N_{> 0}$ the composite relation $V_n \circ V_n$ is a subset of $V_{n - 1}$, that is, $V_n \circ V_n \subseteq V_{n - 1}$

Proof:
==== Lemma 20 ====
{{:Characterization of Paracompactness in T3 Space/Lemma 20}}{{qed|lemma}}
The sequence $\sequence{V_n}_{n \in \N}$ is now constructed using the Principle of Recursive Definition and Zermelo's Well-Ordering Theorem.
Let:
:$\NN = \leftset{U \subseteq X \times X : U }$ is a neighborhood of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} } \rightset{}$
From Zermelo's Well-Ordering Theorem, let:
:$\preccurlyeq$ be a well-ordering on $\NN$
Let $g: \NN \to \NN$ be the mapping defined by:
:$\forall U \in \NN : \map g U = \min \leftset{ V \in \NN : V \circ V \subseteq U}$ and $V$ is symmetric $\rightset{}$
From {{Lemma|Characterization of Paracompactness in T3 Space|20}}:
:$\forall U \in \NN : \leftset{ V \in \NN : V \circ V \subseteq U}$ and $V$ is symmetric $\rightset{} \ne \O$
By definition of well-ordering:
:$g$ is well-defined
From Principle of Recursive Definition, there exists exactly one sequence $\sequence{V_n}_{n \in \N}$ of neighborhoods of the diagonal $\Delta_X$ in $\struct {X \times X, \tau_{X \times X} }$:
:$V_0 = V$
:$\forall n \in \N_{> 0} : V_n$ is symmetric as a relation on $X \times X$
:$\forall n \in \N_{> 0}$ the composite relation $V_n \circ V_n$ is a subset of $V_{n - 1}$, that is, $V_n \circ V_n \subseteq V_{n - 1}$
{{qed}}
{{AoC}}
Category:Characterization of Paracompactness in T3 Space
snjmgqlivwz4jeeqoblgizhey1xtqcq
Theorem: Characterization of Set Equals Union of Sets

Let $A$ be a set.
Let $\BB$ be a set of sets.
Then $A = \ds \bigcup \BB$ {{iff}}:
:$\forall a \in A : \exists B \in \BB : a \in B$
:$\forall B \in \BB : B \subseteq A$

Proof:
=== Necessary Condition ===
Let $A = \ds \bigcup \BB$.
By definition of set union:
:$\forall a \in A = \ds \bigcup \BB : \exists B \in \BB : a \in B$
From Set is Subset of Union:
:$\forall B \in \BB : B \subseteq \ds \bigcup \BB = A$
{{qed|lemma}}
Theorem: Subset of Discrete Set of Subsets is Discrete

Let $T = \struct {S, \tau}$ be a topological space.
Let $\FF \subseteq \powerset S$ be a set of subsets of $S$.
Let $\GG \subseteq \FF$.
If $\FF$ is discrete then $\GG$ is discrete.

Proof:
We prove the contrapositive statement:
:If $\GG$ is not discrete then $\FF$ is not discrete.
Let $\GG$ not be discrete.
By definition of discrete:
:$\exists x \in S : \forall N \subseteq S : N$ is a neighborhood of $x : \exists X_1, X_2 \in \GG : X_1 \ne X_2: X_1 \cap N \ne \O, X_2 \cap N \ne \O$
By definition of subset:
:$\forall X \in \GG : X \in \FF$
Hence:
:$\exists x \in S : \forall N \subseteq S : N$ is a neighborhood of $x : \exists X_1, X_2 \in \FF : X_1 \ne X_2: X_1 \cap N \ne \O, X_2 \cap N \ne \O$
By definition, $\FF$ is not discrete.
The result follows from Rule of Transposition.
{{qed}}
Category:Discrete Sets of Subsets
aqh16hx3f6fiyso19im53wlm9xbqphp
Theorem: Double Orthocomplement of Closed Linear Subspace

Let $H$ be a Hilbert space.
Let $A \subseteq H$ be a closed linear subspace of $H$.
Then:
:$\paren {A^\perp}^\perp = A$

Proof:
{{MissingLinks|identity operator}}
Let $I : H \to H$ be the identity operator (viz., $I h = h$).
Also, let $P : H \to A$ be the orthogonal projection.
Then $I - P : H \to A^\perp$ is the Orthogonal Projection onto Orthocomplement.
By Kernel of Orthogonal Projection:
:$\map \ker {I - P} = \paren {A^\perp}^\perp$
{{qed|lemma}}
From Orthogonal Projection is Projection:
:$h \in P \sqbrk H \implies h = P h$
where $P \sqbrk H$ denotes the image of $H$ under $P$.
Also:
:$0 = \paren {I - P} h \iff h = P h$ 
Therefore,:
:$\map \ker {I - P} = P \sqbrk H$
{{qed|lemma}}
Finally, from Range of Orthogonal Projection:
:$P \sqbrk H = A$
{{qed|lemma}}
To conclude:
:$\paren {A^\perp}^\perp = \map \ker {I - P} = P \sqbrk H = A$
{{qed}}
Theorem: Löwenheim-Skolem Theorem

Let $\FF$ be a formula which is valid in a countably infinite domain.
Then $\FF$ is universally valid.

Proof:
{{ProofWanted}}
{{Namedfor|Leopold Löwenheim|name2 = Thoralf Albert Skolem|cat = Löwenheim|cat2 = Skolem}}
Theorem: Second Derivative of Inverse Function

Let $f$ be a real function which is of differentiability class $2$.
Let $f$ have an inverse $f^{-1}$, likewise of differentiability class $2$.
Then:
:$\dfrac {\d^2 x} {\d y^2} = -\dfrac {\d^2 y} {\d x^2} \paren {\dfrac {\d y} {\d x} }^{-3}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^2 x} {\d y^2}
      | r = \map {\dfrac \d {\d y} } {\dfrac {\d x} {\d y} }
      | c = {{Defof|Second Derivative}}
}}
{{eqn | r = \map {\dfrac \d {\d y} } {\dfrac 1 {\d y / \d x} }
      | c = Derivative of Inverse Function
}}
{{eqn | r = \dfrac {-1} {\paren {\d y / \d x}^2} \map {\dfrac \d {\d y} } {\dfrac {\d y} {\d x} }
      | c = Derivative of Composite Function
}}
{{eqn | r = \dfrac {-1} {\paren {\d y / \d x}^2} \dfrac {\d x} {\d y} \map {\dfrac \d {\d x} } {\dfrac {\d y} {\d x} }
      | c = Derivative of Composite Function
}}
{{eqn | r = \dfrac {-1} {\paren {\d y / \d x}^3} \dfrac {\d^2 y} {\d x^2}
      | c = {{Defof|Second Derivative}}, Derivative of Inverse Function and simplification
}}
{{eqn | r = -\dfrac {\d^2 y} {\d x^2} \paren {\dfrac {\d y} {\d x} }^{-3}
      | c = rearranging into given format
}}
{{end-eqn}}
{{qed}}
Theorem: Third Derivative of Inverse Function

Let $f$ be a real function which is of differentiability class $3$.
Let $f$ have an inverse $f^{-1}$, likewise of differentiability class $3$.
Then:
:$\dfrac {\d^3 x} {\d y^3} = -\paren {\dfrac {\d^3 y} {\d x^3} \dfrac {\d y} {\d x} - 3 \paren {\dfrac {\d^2 y} {\d x^2} }^2} \paren {\dfrac {\d y} {\d x} }^{-5}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^3 x} {\d y^3}
      | r = \map {\dfrac \d \d y } {\dfrac {\d^2 x} {\d y^2} }
      | c = {{Defof|Third Derivative}}
}}
{{eqn | r = \map {\dfrac \d {\d y} } {-\dfrac {\d^2 y} {\d x^2} \paren {\dfrac {\d y} {\d x} }^{-3} }
      | c = Derivative of Inverse Function
}}
{{eqn | r = -\paren {\paren {\dfrac {\d y} {\d x} }^{-3} \map {\dfrac \d {\d y} } {\dfrac {\d^2 y} {\d x^2} } + \dfrac {\d^2 y} {\d x^2} \map {\dfrac \d {\d y} } {\paren {\dfrac {\d y} {\d x} }^{-3} } }
      | c = Product Rule for Derivatives
}}
{{eqn | r = -\paren {\paren {\dfrac {\d y} {\d x} }^{-3} \dfrac {\d x} {\d y} \map {\dfrac \d {\d x} } {\dfrac {\d^2 y} {\d x^2} } + \dfrac {\d^2 y} {\d x^2} \dfrac {\d x} {\d y} \map {\dfrac \d {\d x} } {\paren {\dfrac {\d y} {\d x} }^{-3} } }
      | c = Derivative of Composite Function
}}
{{eqn | r = -\paren {\paren {\dfrac {\d y} {\d x} }^{-3} \dfrac {\d x} {\d y} \dfrac {\d^3 y} {\d x^3} + \dfrac {\d^2 y} {\d x^2} \dfrac {\d x} {\d y} \paren {-3 \paren {\dfrac {\d y} {\d x} }^{-4} } \map {\dfrac \d {\d x} } {\dfrac {\d y} {\d x} } }
      | c = {{Defof|Third Derivative}}, Derivative of Composite Function
}}
{{eqn | r = -\paren {\paren {\dfrac {\d y} {\d x} }^{-3} \dfrac {\d x} {\d y} \dfrac {\d^3 y} {\d x^3} + \paren {\dfrac {\d^2 y} {\d x^2} }^2 \dfrac {\d x} {\d y} \paren {-3 \paren {\dfrac {\d y} {\d x} }^{-4} } }
      | c = {{Defof|Second Derivative}}
}}
{{eqn | r = -\paren {\dfrac {\d^3 y} {\d x^3} - 3 \paren {\dfrac {\d^2 y} {\d x^2} }^2 \paren {\dfrac {\d y} {\d x} }^{-1} } \paren {\dfrac {\d y} {\d x} }^{-3} \dfrac {\d x} {\d y}
      | c = simplifying
}}
{{eqn | r = -\paren {\dfrac {\d^3 y} {\d x^3} - 3 \paren {\dfrac {\d^2 y} {\d x^2} }^2 \paren {\dfrac {\d y} {\d x} }^{-1} } \paren {\dfrac {\d y} {\d x} }^{-3} \paren {\dfrac {\d y} {\d x} }^{-1}
      | c = Derivative of Composite Function
}}
{{eqn | r = -\paren {\dfrac {\d^3 y} {\d x^3} \dfrac {\d y} {\d x} - 3 \paren {\dfrac {\d^2 y} {\d x^2} }^2} \paren {\dfrac {\d y} {\d x} }^{-5}
      | c = simplifying and manipulating into required form
}}
{{end-eqn}}
{{qed}}
Theorem: Relation is Equivalence iff Reflexive and Circular

Let $\RR \subseteq S \times S$ be a relation in $S$.
Then:
:$\RR$ is reflexive and circular
{{iff}}:
:$\RR$ is an equivalence relation.

Proof:
=== Sufficient Condition ===
Let $\RR$ be reflexive and circular.
Then from Reflexive Circular Relation is Equivalence:
:$\RR$ is an equivalence relation.
{{qed|lemma}}
Theorem: Equivalence Relation is Circular

Let $\RR \subseteq S \times S$ be an equivalence relation.
Then $\RR$ is also a circular relation.

Proof:
Let $x, y, z \in S$ be arbitrary such that:
:$\tuple {x, y} \in \RR$ and $\tuple {y, z} \in \RR$
We have {{afortiori}} that $\RR$ is transitive.
Hence:
:$\tuple {x, z} \in \RR$
We also have {{afortiori}} that $\RR$ is symmetric.
Hence:
:$\tuple {z, x} \in \RR$
We have demonstrated that:
:$\tuple {x, y} \in \RR$ and $\tuple {y, z} \in \RR \implies \tuple {z, x} \in \RR$
and $\RR$ is circular by definition.
{{Qed}}
Theorem: Primitive of x over x squared plus a squared/Corollary

:$\ds \int \frac {x \rd x} {a^2 + b^2 x^2} = \frac 1 {2 b^2} \map \ln {a^2 + b^2 x^2} + C$

Proof:
Let $z = b x$.
Then:
:$\dfrac {\d x} {\d z} = \dfrac 1 b$
Hence:
{{begin-eqn}}
{{eqn | l = \int \frac {x \rd x} {a^2 + b^2 x^2}
      | r = \int \dfrac 1 b \frac {\paren {z / b} \d z} {a^2 + z^2}
      | c = Integration by Substitution
}}
{{eqn | r = \dfrac 1 {b^2} \int \frac {z \d z} {a^2 + z^2}
      | c = simplifying, and Linear Combination of Primitives
}}
{{eqn | r = \dfrac 1 {b^2} \cdot \frac 1 2 \map \ln {a^2 + z^2} + C
      | c = Primitive of $\dfrac z {a^2 + z^2}$
}}
{{eqn | r = \dfrac 1 {2 b^2} \map \ln {a^2 + b^2 x^2} + C
      | c = subtituting for $z$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Reciprocal of a squared minus x squared/Logarithm Form 2/Corollary

:$\ds \int \frac {\d x} {a^2 - b^2 x^2} = \dfrac 1 {2 a b} \ln \size {\dfrac {a + b x} {a - b x} } + C$

Proof:
Let $z = b x$.
Then:
:$\dfrac {\d x} {\d z} = \dfrac 1 b$
Hence:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {a^2 - b^2 x^2}
      | r = \int \dfrac 1 b \frac {\d z} {a^2 - z^2}
      | c = Integration by Substitution
}}
{{eqn | r = \dfrac 1 b \cdot \dfrac 1 {2 a} \ln \size {\dfrac {a + x} {a - x} } + C
      | c = Primitive of $\dfrac 1 {a^2 - z^2}$: Logarithm Form $2$
}}
{{eqn | r = \dfrac 1 {2 a b} \ln \size {\dfrac {a + b x} {a - b x} } + C
      | c = subtituting for $z$ and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Determinant of Plane Reflection Matrix

The matrix associated with a reflection of the plane has a determinant of $-1$.

Proof:
From Matrix Equation of Plane Reflection, we have:
{{begin-eqn}}
{{eqn | l = \begin {vmatrix} \cos 2 \alpha & \sin 2 \alpha \\ \sin 2 \alpha & -\cos 2 \alpha \end {vmatrix}
      | r = -\map \cos {2 \alpha} \map \cos {2 \alpha} - \map \sin {2 \alpha} \map \sin {2 \alpha}
      | c = Determinant of Order 2
}}
{{eqn | r = -\paren {\cos^2 2 \alpha + \sin^2 2 \alpha}
}}
{{eqn | r = -1
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Geometric Reflections
Category:Determinants
e33jvmqfdt7m4snhj56usjs768oe2yg
Theorem: Inverse of Plane Reflection Matrix

Let $\mathbf R$ be the matrix associated with a reflection in the plane.
:<nowiki>$\mathbf R = \begin{bmatrix}
\cos 2\alpha & \sin 2\alpha \\
\sin 2\alpha & -\cos 2\alpha
\end{bmatrix}$</nowiki>
Then its inverse matrix $\mathbf R^{-1}$ is itself.

Proof:
Consider $\mathbf R \mathbf R$:
{{begin-eqn}}
{{eqn | l = \mathbf R \mathbf R
      | r = \begin {bmatrix} \cos 2 \alpha & \sin 2 \alpha \\ \sin 2 \alpha & -\cos 2 \alpha \end {bmatrix} \begin {bmatrix} \cos 2 \alpha & \sin 2 \alpha \\ \sin 2 \alpha & -\cos 2 \alpha \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} \map \cos {2 \alpha} \map \cos {2 \alpha} + \map \sin {2 \alpha} \map \sin {2 \alpha} & \map \cos {2 \alpha} \map \sin {2 \alpha} - \map \sin {2 \alpha} \map \cos {2 \alpha} \\ \map \sin {2 \alpha} \map \cos {2 \alpha} - \map \cos {2 \alpha} \map \sin {2 \alpha} & \map \sin {2 \alpha} \map \sin {2 \alpha} + \map \cos {2 \alpha} \map \cos {2 \alpha} \end {bmatrix}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | r = \begin {bmatrix} \cos^2 2 \alpha + \sin^2 2 \alpha & 0 \\ 0 & \sin^2 2 \alpha + \cos^2 2 \alpha \end {bmatrix}
}}
{{eqn | r = \begin {bmatrix} 1 & 0 \\ 0 & 1 \end {bmatrix}
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Hence, by the definition of the inverse matrix, $\mathbf R$ is the inverse matrix of $\mathbf R$.
{{qed}}
Category:Inverse Matrices
qutepnz4uwmbxa5pqrs1vlhuinccfic
Theorem: Arcsine in terms of Twice Arctangent

:$\arcsin x = 2 \map \arctan {\dfrac x {1 + \sqrt {1 - x^2} } }$

Proof:
Let: 
:$\theta = \arcsin x$
Then by the definition of arcsine:
:$x = \sin \theta$
and: 
:$-\dfrac \pi 2 < \theta < \dfrac \pi 2$
Then:
{{begin-eqn}}
{{eqn | l = \tan \dfrac \theta 2
      | r = \dfrac {\sin \theta} {1 + \cos \theta}
      | c = {{Corollary|Half Angle Formula for Tangent|1}}
}}
{{eqn | r = \dfrac {\sin \theta} {1 + \sqrt {1 - \sin^2 \theta} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \dfrac x {1 + \sqrt {1 - x^2} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \dfrac \theta 2
      | r = \map \arctan {\dfrac x {1 + \sqrt {1 - x^2} } }
      | c = taking arctangent of both sides
}}
{{eqn | ll= \leadsto
      | l = \arcsin x
      | r = 2 \map \arctan {\dfrac x {1 + \sqrt {1 - x^2} } }
      | c = substituting $\theta \gets \arcsin x$
}}
{{end-eqn}}
{{qed}}
Category:Arcsine Function
Category:Arctangent Function
nkpkjiko6zl1022cwr3d6253mfp31lj