avewright/proofwiki-math huggingface dataset:
Theorem: Reverse Triangle Inequality/Real and Complex Fields/Corollary 2

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\size {x + y} \ge \size x - \size y$
where $\size x$ denotes either the absolute value of a real number or the complex modulus of a complex number.

Proof:
Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Let $z := -y$.
Then we have:
{{begin-eqn}}
{{eqn | l = \size {x - z}
      | o = \ge
      | r = \size x - \size z
      | c = {{Corollary|Reverse Triangle Inequality/Real and Complex Fields|1|disp = Reverse Triangle Inequality for Real and Complex Fields}}
}}
{{eqn | l = \size {x - \paren {-y} }
      | o = \ge
      | r = \size x - \size {-y}
      | c = Definition of $z$
}}
{{eqn | ll= \leadsto
      | l = \size {x + y}
      | o = \ge
      | r = \size x - \size {-y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x + y}
      | o = \ge
      | r = \size x - \size y
      | c = as $\size y = \size {-y}$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Triangle Inequality/Real Numbers/General Result

Let $x_1, x_2, \dotsc, x_n \in \R$ be real numbers.
Let $\size x$ denote the absolute value of $x$.
Then:
:$\ds \size {\sum_{i \mathop = 1}^n x_i} \le \sum_{i \mathop = 1}^n \size {x_i}$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \size {\sum_{i \mathop = 1}^n x_i} \le \sum_{i \mathop = 1}^n \size {x_i}$
$\map P 1$ is true by definition of the usual ordering on real numbers:
:$\size {x_1} \le \size {x_1}$
Theorem: Chebyshev's Sum Inequality/Discrete

Let $a_1, a_2, \ldots, a_n$ be real numbers such that:
:$a_1 \ge a_2 \ge \cdots \ge a_n$
Let $b_1, b_2, \ldots, b_n$ be real numbers such that:
:$b_1 \ge b_2 \ge \cdots \ge b_n$
Then:
:$\ds \dfrac 1 n \sum_{k \mathop = 1}^n a_k b_k \ge \paren {\dfrac 1 n \sum_{k \mathop = 1}^n a_k} \paren {\dfrac 1 n \sum_{k \mathop = 1}^n b_k}$

Proof:
We have {{hypothesis}} that the sequences $\sequence {a_k}$ and $\sequence {b_k}$ are both decreasing.
For $j, k \in \set {1, 2, \ldots, n}$, consider:
:$\paren {a_j - a_k} \paren {b_j - b_k}$
Therefore $a_j - a_k$ and $b_j - b_k$ have the same sign for all $j, k \in \set {1, 2, \ldots, n}$.
So:
:$\forall j, k \in \set {1, 2, \ldots, n}: \paren {a_j - a_k} \paren {b_j - b_k} \ge 0$
Hence:
{{begin-eqn}}
{{eqn | l = 0
      | o = \le
      | r = \sum_{j \mathop = 1}^n \sum_{k \mathop = 1}^n \paren {a_j - a_k} \paren {b_j - b_k}
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 1}^n \sum_{k \mathop = 1}^n \paren {a_j b_j - a_k b_j - a_j b_k + a_k b_k}
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 1}^n \sum_{k \mathop = 1}^n a_j b_j - \sum_{j \mathop = 1}^n \sum_{k \mathop = 1}^n a_k b_j - \sum_{j \mathop = 1}^n \sum_{k \mathop = 1}^n a_j b_k + \sum_{j \mathop = 1}^n \sum_{k \mathop = 1}^n a_k b_k
      | c = 
}}
{{eqn | r = n \sum_{j \mathop = 1}^n a_j b_j - \sum_{k \mathop = 1}^n a_k \sum_{j \mathop = 1}^n b_j - \sum_{j \mathop = 1}^n a_j \sum_{k \mathop = 1}^n b_k + n \sum_{k \mathop = 1}^n a_k b_k
      | c = General Distributivity Theorem
}}
{{eqn | r = 2 n \sum_{k \mathop = 1}^n a_k b_k - 2 \sum_{k \mathop = 1}^n a_k \sum_{k \mathop = 1}^n b_k
      | c = renaming and gathering equal terms
}}
{{eqn | r = n \sum_{k \mathop = 1}^n a_k b_k - \sum_{k \mathop = 1}^n a_k \sum_{k \mathop = 1}^n b_k
      | c = dividing through by $2$
}}
{{eqn-intertext|Then we may manipulate it into the required form:}}
{{eqn | r = \dfrac 1 n \sum_{k \mathop = 1}^n a_k b_k - \dfrac 1 {n^2} \sum_{k \mathop = 1}^n a_k \sum_{k \mathop = 1}^n b_k
      | c = dividing through by $n^2$
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 n \sum_{k \mathop = 1}^n a_k b_k
      | o = \ge
      | r = \paren {\dfrac 1 n \sum_{k \mathop = 1}^n a_k} \paren {\dfrac 1 n \sum_{k \mathop = 1}^n b_k}
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Positive Real Numbers whose Reciprocals Sum to 1

Let $p, q \in \R_{\ge 0}$ be positive real numbers such that:
:$\dfrac 1 p + \dfrac 1 q = 1$
Then $p > 1$ and $q > 1$.

Proof:
From Division by Zero it is immediate that $p > 0$ and $q > 0$.
{{AimForCont}} either $0 < p \le 1$ or $0 < q \le 1$.
{{WLOG}}, suppose $0 < p \le 1$.
Note we have that:
:$\dfrac 1 q = 1 - \dfrac 1 p$
First suppose $p = 1$.
Then:
:$\dfrac 1 q = 0$
But there exists no $q \in \R$ such that $\dfrac 1 q = 0$.
Hence it cannot be the case that $p = 1$.
Now suppose $0 < p < 1$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac 1 p
      | o = >
      | r = 1
      | c = 
}}
{{eqn | l = 1 - \dfrac 1 p
      | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 q
      | o = <
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = q
      | o = <
      | r = 0
      | c = 
}}
{{end-eqn}}
But this contradicts our assertion that $q > 0$.
Hence by Proof by Contradiction it follows that $p > 1$.
Similarly we reach a contradiction by assuming $0 < q \le 1$.
Hence $p > 1$ and $q > 1$ as required.
{{qed}}
Category:Real Analysis
toy3m1z85tmox92uoefdt1fk3t2iedd
Theorem: Hölder's Inequality for Sums/Formulation 1/Equality

:$\norm {\mathbf x \mathbf y}_1 = \norm {\mathbf x}_p \norm {\mathbf y}_q$
{{iff}}:
:$\forall k \in \N: \size {y_k} = c \size {x_k}^{p - 1}$
for some real constant $c$.

Proof:
{{ProofWanted}}
Category:Hölder's Inequality for Sums
49yp9senu7jy68h3ybyua5hibcz8xpc
Theorem: Plancherel Theorem

For all $f \in \map {L^1} {\R^n} \cap \map {L^2} {\R^n}$, we have:
:$\norm {\map \FF f}_2 = \norm {\map {\FF ^{-1} } f}_2 = \norm f_2$
where:
:$\map \FF f$ is the Fourier transform of $f$
:$\map {\FF ^{-1} } f$ is the inverse Fourier transform of $f$
:$\norm \cdot_2$ denotes the $L^2$ norm

Proof:
{{ProofWanted}}
{{Namedfor|Michel Plancherel}}
Theorem: Reverse Triangle Inequality/Real and Complex Fields/Corollary 3

Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Then:
:$\size {x + y} \ge \size {\size x - \size y}$
where $\size x$ denotes either the absolute value of a real number or the complex modulus of a complex number.

Proof:
Let $x$ and $y$ be elements of either the real numbers $\R$ or the complex numbers $\C$.
Let $z := -y$.
Then we have:
{{begin-eqn}}
{{eqn | l = \size {x - z}
      | o = \ge
      | r = \size {\size x - \size z}
      | c = Reverse Triangle Inequality for Real and Complex Fields
}}
{{eqn | l = \size {x - \paren {-y} }
      | o = \ge
      | r = \size {\size x - \size {-y} }
      | c = Definition of $z$
}}
{{eqn | ll= \leadsto
      | l = \size {x + y}
      | o = \ge
      | r = \size {\size x - \size {-y} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {x + y}
      | o = \ge
      | r = \size {\size x - \size y}
      | c = as $\size y = \size {-y}$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: T3 Space with Sigma-Locally Finite Basis is Perfectly T4 Space

Let $T = \struct {S, \tau}$ be a $T_3$ topological space.
Let $\BB$ be a $\sigma$-locally finite basis.
Then:
:$T$ is a perfectly $T_4$ space

Proof:
From T3 Space with Sigma-Locally Finite Basis is T4 Space:
:$T$ is a $T_4$ space
It remains to show that every closed set in $T$ is a $G_\delta$ set
Let $\BB = \ds \bigcup_{n \mathop \in \N} \BB_n$ be a $\sigma$-locally finite basis where $\BB_n$ is a locally finite set of subsets for each $n \in \N$.
Let $F$ be closed in $T$.
By definition of closed set:
:$X \setminus F$ is open in $T$.
Let $G = X \setminus F$.
Theorem: Localization of Module Homomorphism is Multiplicative

Let $A$ be a commutative ring with unity.
Let $S \subseteq A$ be a multiplicatively closed subset.
Let $S^{-1}A$ be the localization of $A$ at $S$.
Let $f_1$ and $f_2$ be $A$-homomorphisms:
:$M_1 \stackrel {f_1} \longrightarrow M_2 \stackrel {f_2} \longrightarrow M_3$
For $i=1,2,3$, let $\struct { S^{-1}M_i, \iota_i}$ be the localization of $M_i$ at $S$.
Let $S^{-1}f_1$ and $S^{-1}f_i$ be the unique $S^{-1}A$-homomorphisms:
:$S^{-1}M_1 \stackrel {S^{-1}f_1} \longrightarrow S^{-1}M_2 \stackrel {S^{-1}f_2} \longrightarrow S^{-1}M_3$
such that:
:$\iota_{i+1} \circ f_i = \paren {S^{-1}f_i} \circ \iota_i$
Let:
:$S^{-1}M_1 \stackrel {S^{-1}\paren {f_2 \circ f_1}} \longrightarrow S^{-1}M_3$
be the unique $S^{-1}A$-homomorphism such that:
:$\iota_3 \circ \paren {f_2 \circ f_1} = \paren {S^{-1} \paren {f_2 \circ f_1} } \circ \iota_1$
Then we have:
:$S^{-1} \paren {f_2 \circ f_1} = \paren {S^{-1} f_2} \circ \paren {S^{-1} f_1}$

Proof:
Let $g : S^{-1}M_1 \to S^{-1}M_3$ be defined by:
:$g:= \paren {S^{-1} f_2} \circ \paren {S^{-1} f_1}$
Then:
{{begin-eqn}}
{{eqn | l = g \circ \iota_1
      | r = \paren {S^{-1}f_2} \circ \paren {S^{-1}f_1 } \circ \iota_1
}}
{{eqn | r = \paren {S^{-1}f_2} \circ \iota_2 \circ f_1
      | c = {{Defof|Localization of Module|$S^{-1} f_1$}}
}}
{{eqn | r = \iota_3 \circ \paren {f_2 \circ f_1}
      | c = {{Defof|Localization of Module|$S^{-1} f_2$}}
}}
{{end-eqn}}
Thus, by {{Defof|Localization of Module|$S^{-1} \paren {f_2 \circ f_1}$}}, we have:
:$g = S^{-1} \paren {f_2 \circ f_1}$
{{qed}}
Theorem: Matrix Equation of Plane Rotation

Let $r_\alpha$ be a rotation of the plane about the origin through an angle of $\alpha$.
Let $r_\alpha$ rotate an arbitrary point in the plane $P = \tuple {x, y}$ onto $P' = \tuple {x', y'}$
Then the rotation matrix representing $r_\alpha$ can be presented as:
:$\begin {bmatrix} x' \\ y' \end {bmatrix} = \begin {bmatrix} \cos \alpha & -\sin \alpha \\ \sin \alpha & \cos \alpha \end {bmatrix} \begin {bmatrix} x \\ y \end {bmatrix}$

Proof:
Let the coordinates of $P'$ be encoded as the elements of a $2 \times 1$ matrix.
We have:
{{begin-eqn}}
{{eqn | l = \begin {bmatrix} x' \\ y' \end {bmatrix}
      | r = P'
}}
{{eqn | r = \map {r_\alpha} P
      | c = {{Defof|Plane Rotation}}
}}
{{eqn | r = \begin {bmatrix} x \cos \alpha - y \sin \alpha \\ x \sin \alpha + y \cos \alpha \end {bmatrix}
      | c = Equation defining Plane Rotation
}}
{{eqn | r = \begin {bmatrix} \cos \alpha & -\sin \alpha \\ \sin \alpha & \cos \alpha \end {bmatrix} \begin {bmatrix} x \\ y \end {bmatrix}
     | c = {{Defof|Matrix Product (Conventional)}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Inverse of Nonsingular 2 x 2 Real Square Matrix

Let $\mathbf A$ be an nonsingular $2 \times 2$ real square matrix defined as:
:$\mathbf A = \begin{pmatrix} a & b \\ c & d \end{pmatrix}$
Then its inverse matrix $\mathbf A^{-1}$ is:
:$\mathbf A^{-1} = \dfrac 1 {\map \det {\mathbf A} } \begin {pmatrix} d & -b \\ -c & a \end {pmatrix} = \dfrac 1 {a d - b c} \begin {pmatrix} d & -b \\ -c & a \end {pmatrix}$

Proof:
=== Case: $a \ne 0$ ===
We construct $\begin {pmatrix} \mathbf A & \mathbf I \end {pmatrix}$:
:$\begin {pmatrix} \mathbf A & \mathbf I \end {pmatrix} = \paren {\begin {array} {cc|cc} a & b & 1 & 0 \\ c & d & 0 & 1 \\ \end {array} }$
In the following, $\sequence {e_n}_{n \mathop \ge 1}$ denotes the sequence of elementary row operations that are to be applied to $\begin {pmatrix} \mathbf A & \mathbf I \end {pmatrix}$.
The matrix that results from having applied $e_1$ to $e_k$ in order is denoted $\begin {pmatrix} \mathbf A_k & \mathbf B_k \end {pmatrix}$.
{{begin-eqn}}
{{eqn | l = \begin {pmatrix} \mathbf A & \mathbf I \end {pmatrix}
      | r = \paren {\begin {array} {cc {{|}} cc} a & b & 1 & 0 \\ c & d & 0 & 1 \\ \end {array} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \begin {pmatrix} \mathbf A_1 & \mathbf B_1 \end {pmatrix}
      | r = \paren {\begin {array} {cc {{|}} cc} 1 & \dfrac b a & \dfrac 1 a & 0 \\ c & d & 0 & 1 \\ \end {array} }
      | c = $e_1 := r_1 \to \dfrac 1 a r_1$
}}
{{eqn | ll= \leadsto
      | l = \begin {pmatrix} \mathbf A_2 & \mathbf B_2 \end {pmatrix}
      | r = \paren {\begin {array} {cc {{|}} cc} 1 & \dfrac b a & \dfrac 1 a & 0 \\ 0 & \dfrac {a d - b c} a & -\dfrac c a & 1 \\ \end {array} }
      | c = $e_2 := r_2 \to -c r_1 + r_2$
}}
{{eqn | ll= \leadsto
      | l = \begin {pmatrix} \mathbf A_3 & \mathbf B_3 \end {pmatrix}
      | r = \paren {\begin {array} {cc {{|}} cc} 1 & \dfrac b a & \dfrac 1 a & 0 \\ 0 & 1 & -\dfrac c {a d - b c} & \dfrac a {a d - b c} \\ \end {array} }
      | c = $e_3 := r_2 \to \dfrac a {a d - b c} r_1$
}}
{{eqn | ll= \leadsto
      | l = \begin {pmatrix} \mathbf A_4 & \mathbf B_4 \end {pmatrix}
      | r = \paren {\begin {array} {cc {{|}} cc} 1 & 0 & \dfrac d {a d - b c} & -\dfrac b {a d - b c} \\ 0 & 1 & -\dfrac c {a d - b c} & \dfrac a {a d - b c} \\ \end {array} }
      | c = $e_4 := r_1 \to -\dfrac b a r_2 + r_1$
}}
{{end-eqn}}
It is seen that $\begin {pmatrix} \mathbf A_4 & \mathbf B_4 \end {pmatrix}$ is the required reduced echelon form:
:$\mathbf A_4 = \mathbf I$
Hence by the Matrix Inverse Algorithm:
{{begin-eqn}}
{{eqn | l = \mathbf A^{-1}
      | r = \mathbf B_4
}}
{{eqn | l = 
      | r = \begin{pmatrix} \dfrac d {a d - b c} & -\dfrac b {a d - b c} \\ -\dfrac c {a d - b c} & \dfrac a {a d - b c} \end{pmatrix}
}}
{{eqn | l =
      | r = \dfrac 1 {a d - b c} \begin {pmatrix} d & -b \\ -c & a \end {pmatrix}
      | c = {{Defof|Matrix Scalar Product}}
}}
{{eqn | l = 
      | r = \dfrac 1 {\map \det {\mathbf A} } \begin {pmatrix} d & -b \\ -c & a \end {pmatrix}
      | c = Determinant of Order 2
}}
{{end-eqn}}
Hence the result.
{{qed|lemma}}
Theorem: Element of Localization of Module is Represented as Quotient over S

Let $A$ be a commutative ring with unity.
Let $S \subseteq A$ be a multiplicatively closed subset.
Let $S^{-1}A$ be the localization of $A$ at $S$.
Let $M$ be a $A$-module.
Let $\struct { S^{-1}M, \iota}$ be the localization of $M$ at $S$.
Let $x \in S^{-1}M$.
Then there exist $m \in M$ and $s \in S$ such that:
:$x = s^{-1} \map \iota m$

Proof:
Recall that $S \subseteq \paren {S^{-1}A}^\times$ by {{Defof|Localization of Ring}}.
{{ProofWanted}}
Category:Commutative Algebra
bxdbbuto9481clltm3bz01s8h4li7pt
Theorem: Evaluation Linear Transformation on Normed Vector Space is Weak to Weak-* Continuous Embedding into Second Normed Dual

Let $\Bbb F \in \set {\R, \C}$.
Let $X$ be a normed vector space over $\Bbb F$. 
Let $X^\ast$ be the normed dual of $X$. 
Let $X^{\ast \ast}$ be the second normed dual of $X$. 
Let $w$ be the weak topology on $X$.
Let $w^\ast$ be the weak-$\ast$ topology on $X^{\ast \ast}$.
Let $\iota : X \to X^{\ast \ast}$ be the evaluation linear transformation.
Then $\iota$ is $\struct {w, w^\ast}$-continuous.

Proof:
From the definition of the initial topology, $w^\ast$ is generated by the mappings $f^\wedge : X^{\ast \ast} \to \Bbb F$ defined by: 
:$\map {f^{\wedge} } \Phi = \map \Phi f$
for each $f \in X^\ast$ and $\Phi \in X^{\ast \ast}$.
From Continuity in Initial Topology, it therefore suffices to verify that $f^\wedge \circ \iota : \struct {X, w} \to \Bbb F$ is continuous for each $f \in X^\ast$.
From Characterization of Continuity of Linear Functional in Weak Topology, we can equivalently show that $f^\wedge \circ \iota \in X^\ast$ for each $f \in X^\ast$.
For each $x \in X$ and $f \in X^\ast$, we have: 
{{begin-eqn}}
{{eqn	| l = \map {\paren {f^\wedge \circ \iota} } x
		| r = \map {f^\wedge} {x^\wedge} 
}}
{{eqn	| r = \map {x^\wedge} f
}}
{{eqn	| r = \map f x
}}
{{end-eqn}}
Hence we have: 
:$f^\wedge \circ \iota = f \in X^\ast$
and we are done. 
{{qed}}
Category:Weak Topologies on Topological Vector Spaces
Category:Weak-* Topologies
Category:Evaluation Linear Transformations (Normed Vector Spaces)
n85ika4dl0v8y6hye23v3rihtm6lo9q
Theorem: Determinant of Plane Rotation Matrix

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

Proof:
From Matrix Equation of Plane Rotation, we have:
{{begin-eqn}}
{{eqn | l = \begin {vmatrix} \cos \alpha & -\sin \alpha \\ \sin \alpha & \cos \alpha \end {vmatrix}
      | r = \map \cos \alpha \map \cos \alpha - \paren {-\map \sin \alpha} \map \sin \alpha
      | c = Determinant of Order 2
}}
{{eqn | l =
      | r = \cos^2 \alpha + \sin^2 \alpha
}}
{{eqn | l =
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Determinants
t7pfanl4ju7ay72tbesro29wjpr5v5x
Theorem: T3 Space with Sigma-Locally Finite Basis is Perfectly T4 Space/Lemma 2

:$\CC$ is a is a cover of $G$

Proof:
Let $x \in G$.
From Characterization of T3 Space:
:$\exists U \in \tau : x \in U : U^- \subseteq G$
where $U^-$ denotes the closure of $U$ in $T$.
By definition of basis:
:$\exists B \in \BB : x \in B : B \subseteq U$
From Topological Closure of Subset is Subset of Topological Closure:
:$B^- \subseteq U^-$
From Subset Relation is Transitive:
:$B^- \subseteq G$
Hence:
:$B \in \CC$
Since $x$ was arbitrary, we have:
:$\forall x \in G : C \in \CC : x \in C$
Hence $\CC$ is a cover of $G$ by definition.
{{qed}}
Category:T3 Space with Sigma-Locally Finite Basis is Perfectly T4 Space
jk68gofdtgmynpspivafflchjmeq3bp
Theorem: T3 Space with Sigma-Locally Finite Basis is Perfectly T4 Space/Lemma 1

:$G$ is an $F_\sigma$ set

Proof:
Let:
:$\CC = \set{B \in \BB : B^- \subseteq G}$
where $B^-$ denotes the closure of $B$ in $T$.
Theorem: Regular Space with Sigma-Locally Finite Basis is Perfectly Normal

Let $T = \struct {S, \tau}$ be a regular topological space.
Let $\BB$ be a $\sigma$-locally finite basis.
Then:
:$T$ is a perfectly normal space.

Proof:
{{Recall|Normal Space|normal space|index = 1}}
{{:Definition:Normal Space/Definition 1}}
{{Recall|Regular Space|regular space|index = 1}}
{{:Definition:Regular Space/Definition 2}}
From $T_3$ Space with $\sigma$-Locally Finite Basis is Perfectly $T_4$ Space:
:$T$ is a perfectly $T_4$ space
Hence $T$ is a perfectly normal space by definition.
{{qed}}
Category:Regular Spaces
Category:Sigma-Locally Finite Bases
Category:Perfectly Normal Spaces
b0bu0yq8w8l8nxsek39nlc41qdws6z9
Theorem: Neighborhood of Diagonal induces Open Cover

:$\VV$ is an open cover of $T$

Proof:
By definition of product topology:
:$\BB = \set {V_1 \times V_2: V_1, V_2 \in \tau}$ is a basis on $T \times T$
Let $x \in X$.
From Set is Neighborhood of Subset iff Neighborhood of all Points of Subset:
:$U$ is a neighborhood of the point $\tuple{x,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 U$
By definition of Cartesian product:
:$x \in V_1$ and $x \in V_2$
Let $V = V_1 \cap V_2$.
By definition of set intersection:
:$x \in V$
By {{Open-set-axiom|2}}:
:$V \in \tau$
From Intersection is Subset:
:$V \subseteq V_1$ and $V \subseteq V_2$
From Cartesian Product of Subsets:
:$V \times V \subseteq V_1 \times V2$
From Subset Relation is Transitive:
:$V \times V \subseteq U$
Hence:
:$\exists V \in \VV : x \in V$
Since $x$ was arbitrary, it follows that:
:$\forall x \in X : \exists V \in \VV : x \in V$
By definition, $\VV$ is an open cover of $T$. 
{{qed}}
Category:Product Spaces
Category:Neighborhoods
Category:Covers
09r4hefkvj9suyu6ux9lyyadqs9bbh0
Theorem: Characterization of Neighborhood by Basis

Let $\struct {S, \tau}$ be a topological space.
Let $\BB$ be an analytic basis for $\tau$.
Let $N \subseteq S$.
Let $x \in N$.
Then $N$ is a neighborhood at $x$ {{iff}}:
:$\exists B \in \BB : x \in B : B \subseteq N$

Proof:
From Basis induces Local Basis:
:$\BB_x = \set {B \in \BB: x \in B}$ is a local basis at $x$
By definition of local basis, $N$ is a neighborhood at $x$ {{iff}}:
:$\exists B \in \BB_x : B \subseteq N$
By definition of $\BB_x$,  $N$ is a neighborhood at $x$ {{iff}}:
:$\exists B \in \BB : x \in B : B \subseteq N$
{{qed}}
Category:Neighborhoods
nemlpbih69elkj5ws0kpzsfvabl8nsv
Theorem: Inverse of Plane Rotation Matrix

Let $\mathbf R$ be the matrix associated with a rotation of the plane about the origin through an angle of $\alpha$:
:<nowiki>$\mathbf R = \begin{bmatrix}
\cos \alpha & -\sin \alpha \\
\sin \alpha & \cos \alpha
\end{bmatrix}$</nowiki>
Then its inverse matrix $\mathbf R^{-1}$ is:
:<nowiki>$\mathbf R^{-1} = \begin{bmatrix}
\cos \alpha & \sin \alpha \\
-\sin \alpha & \cos \alpha
\end{bmatrix}$</nowiki>

Proof:
Let:
:<nowiki>$\mathbf A = \begin{bmatrix}
\cos \alpha & \sin \alpha \\
-\sin \alpha & \cos \alpha
\end{bmatrix}$</nowiki>
Consider $\mathbf R \mathbf A$:
{{begin-eqn}}
{{eqn | l = \mathbf R \mathbf A
      | r = <nowiki>\begin{bmatrix}
\cos \alpha & -\sin \alpha \\
\sin \alpha & \cos \alpha
\end{bmatrix} \begin{bmatrix}
\cos \alpha & \sin \alpha \\
-\sin \alpha & \cos \alpha
\end{bmatrix}</nowiki>
}}
{{eqn | r = <nowiki>\begin{bmatrix}
\map \cos {\alpha} \map \cos {\alpha} + \map \sin {\alpha} \map \sin {\alpha} & \map \cos {\alpha} \map \sin {\alpha} - \map \sin {\alpha} \map \cos {\alpha} \\
\map \sin {\alpha} \map \cos {\alpha} - \map \cos {\alpha} \map \sin {\alpha} & \map \sin {\alpha} \map \sin {\alpha} + \map \cos {\alpha} \map \cos {\alpha}
\end{bmatrix}</nowiki>
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | r = <nowiki>\begin{bmatrix}
\cos^2\alpha + \sin^2\alpha & 0 \\
0 & \sin^2\alpha + \cos^2\alpha
\end{bmatrix}</nowiki>
}}
{{eqn | r = <nowiki>\begin{bmatrix}
1 & 0 \\
0 & 1
\end{bmatrix}</nowiki>
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \mathbf {I_2}
      | c = {{Defof|Unit Matrix}}
}}
{{end-eqn}}
{{qed|lemma}}
Now consider $\mathbf A \mathbf R$:
{{begin-eqn}}
{{eqn | l = \mathbf A \mathbf R
      | r = <nowiki>\begin{bmatrix}
\cos \alpha & \sin \alpha \\
-\sin \alpha & \cos \alpha
\end{bmatrix} \begin{bmatrix}
\cos \alpha & -\sin \alpha \\
\sin \alpha & \cos \alpha
\end{bmatrix}</nowiki>
}}
{{eqn | r = <nowiki>\begin{bmatrix}
\map \cos {\alpha} \map \cos {\alpha} + \map \sin {\alpha} \map \sin {\alpha} & -\map \cos {\alpha} \map \sin {\alpha} + \map \sin {\alpha} \map \cos {\alpha} \\
-\map \sin {\alpha} \map \cos {\alpha} + \map \cos {\alpha} \map \sin {\alpha} & \map \sin {\alpha} \map \sin {\alpha} + \map \cos {\alpha} \map \cos {\alpha}
\end{bmatrix}</nowiki>
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{eqn | r = <nowiki>\begin{bmatrix}
\cos^2\alpha + \sin^2\alpha & 0 \\
0 & \sin^2\alpha + \cos^2\alpha
\end{bmatrix}</nowiki>
}}
{{eqn | r = <nowiki>\begin{bmatrix}
1 & 0 \\
0 & 1
\end{bmatrix}</nowiki>
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \mathbf {I_2}
      | c = {{Defof|Unit Matrix}}
}}
{{end-eqn}}
{{qed|lemma}}
Hence, by the definition of the inverse matrix, $\mathbf A$ is the inverse matrix of $\mathbf R$.
{{qed}}
Category:Inverse Matrices
Category:Geometric Rotations
5ehfpjmnm7uznedpdcrkvk0pr8fdakh
Theorem: Continued Fraction Expansion via Gauss Map

Let $T : \closedint 0 1 \to \closedint 0 1$ be the Gauss map.
Let $x \in \closedint 0 1 \setminus \Q$.
Then $x$ has the simple infinite continued fraction:
{{begin-eqn}}
{{eqn | l = x
      | r = \sqbrk {0; \map {a_1} x, \map {a_2} x, \ldots}
}}
{{eqn | r = 0 + \cfrac 1 {\map {a_1} x + \cfrac 1 {\map {a_2} x + \cfrac 1 \ddots} }
}}
{{end-eqn}}
where:
:$\map {a_n} x := \floor {\dfrac 1 {\map {T^{n - 1} } x} }$
:$\floor \cdot$ denotes the floor.

Proof:
For $x \in \closedint 0 1 \setminus \Q$, we have:
:$\map {a_1} x = \floor {\dfrac 1 x}$
and:
:$\forall n \in \N_{>0} : \map {a_n} x = \map {a_1} { T^{n-1} x }$
{{ProofWanted}}
Category:Continued Fractions
hjrdfdd1e6jlws39rj068ieocsek5ge