avewright/proofwiki-math huggingface dataset:
Theorem: Characterization of Adjunction via Triangle Identities

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $F: \mathbf D \to \mathbf C$ and $G:\mathbf C \to \mathbf D$ be covariant functors.
Then:
:there exists an adjunction $\tuple{F, G, \alpha}$ between $\mathbf C$ and $\mathbf D$
{{iff}}:
:there exist natural transformations $\eta: \operatorname {id}_{\mathbf D} \to GF$ and $\xi: FG \to \operatorname {id}_{\mathbf C}$ satisfying the triangle identities:
{{Property|Triangle Identities}}
Moreover:
:$\eta$ is the unit of adjunction $\alpha$
and:
:$\xi$ is the counit of adjunction $\alpha$.

Proof:
=== Necessary Condition ===
Let $\tuple{F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Let $\eta: \operatorname {id}_{\mathbf D} \to GF$ denote the unit of adjunction $\alpha$.
Let $\xi: FG \to \operatorname {id}_{\mathbf C}$ denote the counit of adjunction $\alpha$.
{{:Characterization of Adjunction via Triangle Identities/Necessary Condition}}{{qed|lemma}}
Theorem: Characterization of Adjunction via Triangle Identities/Lemma 1

:for objects $D \in \mathbf D$ and $C \in \mathbf C$:
::$\map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD} } = \eta_D$
::$\map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } = \xi_C$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD} }
      | r = G \operatorname{id}_{FD} \circ \eta_D
      | c = Definition of $\alpha_{\tuple{D, FD} }$
}}
{{eqn | r = \operatorname{id}_{GFD} \circ \eta_D
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = \eta_D
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} }
      | r = \xi_C \circ F \operatorname{id}_{GC}
      | c = Definition of $\beta_{\tuple{GC, C} }$
}}
{{eqn | r = \xi_C \circ \operatorname{id}_{FGC}
      | c = {{Defof|Covariant Functor}}
}}
{{eqn | r = \xi_C
      | c = {{Defof|Identity Morphism}}
}}
{{end-eqn}}
{{qed}}
Category:Characterization of Adjunction via Triangle Identities
mhl7kbswui9wqrha30sryx9ijg7joke
Theorem: Characterization of Adjunction via Triangle Identities/Lemma 3

:for objects $D \in \mathbf D, C \in \mathbf C$ and morphism $g:FD \to C \in \mathbf C$:
::$\map {\alpha_{\tuple{D, C} } } {g} = Gg \circ \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD}}$

Proof:
==== Lemma 1 ====
{{:Characterization of Adjunction via Triangle Identities/Lemma 1}}{{qed|lemma}}
We have:
{{begin-eqn}}
{{eqn | l = \map {\alpha_{\tuple{D, C} } } {g}
      | r = Gg \circ \eta_D
      | c = Definition of $\alpha_{\tuple{D, C} }$
}}
{{eqn | r = Gg \circ \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD} }
      | c = Lemma 1
}}
{{end-eqn}}
{{qed}}
Category:Characterization of Adjunction via Triangle Identities
kc6kgy72iy27fr4u7vitadh1x3vkkd7
Theorem: Characterization of Adjunction via Triangle Identities/Lemma 4

:for objects $D_1, D_2 \in \mathbf D$ and morphism $f:D_1 \to D_2 \in \mathbf D$:
::$\map {\alpha_{\tuple{D_1, FD_2} } } {Ff} = \map {\alpha_{\tuple{D_2, FD_2} } } {\operatorname{id}_{FD_2}} \circ f$

Proof:
==== Lemma 1 ====
{{:Characterization of Adjunction via Triangle Identities/Lemma 1}}{{qed|lemma}}
By definition of natural transformation:
:$(1): \quad GF f \circ \eta_{D_1} = \eta_{D_2} \circ f$
We have:
{{begin-eqn}}
{{eqn | l = \map {\alpha_{\tuple{D_1, FD_2} } } {Ff}
      | r = GF f \circ \eta_{D_1}
      | c = Definition of $\alpha_{\tuple{D_1, FD_2} }$
}}
{{eqn | r = \eta_{D_2} \circ f
      | c = By $(1)$
}}
{{eqn | r = \map {\alpha_{\tuple{D_2, FD_2} } } {\operatorname{id}_{FD_2} } \circ f
      | c = Lemma 1
}}
{{end-eqn}}
{{qed}}
Category:Characterization of Adjunction via Triangle Identities
n8321xgi2y4jnlf1h4yupwkidnqvyyf
Theorem: Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products

Let $\mathbf C$ be a locally small category.
Let $\mathbf C \times \mathbf C$ be the product category of $\mathbf C$ with itself.
Let $\Delta: \mathbf C \to \mathbf C \times \mathbf C$ denote the diagonal functor.
Then $\Delta$ has a right adjoint {{iff}} $\mathbf C$ has all binary products.
Moreover, the right adjoint is the product functor.

Proof:
=== Necessary Condition ===
{{:Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Necessary Condition}}{{qed|lemma}}
Theorem: Diagonal Functor on Product Category has Left Adjoint Iff Category has Binary Coproducts

Let $\mathbf C$ be a locally small category.
Let $\mathbf C \times \mathbf C$ be the product category of $\mathbf C$ with itself.
Let $\Delta: \mathbf C \to \mathbf C \times \mathbf C$ denote the diagonal functor.
Then $\Delta$ has a left adjoint {{iff}} $\mathbf C$ has all binary coproducts.
Moreover, the left adjoint is the coproduct functor.

Proof:
=== Necessary Condition ===
{{:Diagonal Functor on Product Category has Left Adjoint Iff Category has Binary Coproducts/Necessary Condition}}{{qed|Lemma}}
Theorem: Euler's Continued Fraction Formula/Corollary 1

:$\dfrac 1 A - \dfrac 1 B + \dfrac 1 C - \dfrac 1 D + \dfrac 1 E - \cdots = \cfrac 1 {A + \cfrac {A^2} {B - A + \cfrac {B^2} {C - B + \cfrac {C^2} {D - C + \cfrac {D^2} {E - D + \cfrac {\ddots} {\ddots} } } } } }$

Proof:
From Euler's Continued Fraction Formula, we have:
{{begin-eqn}}
{{eqn | l = a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots + a_0 a_1 a_2 a_3 \cdots a_n
      | r = a_0 \paren {1 + a_1 \paren {1 + a_2 \paren { 1 + a_3 \paren {\cdots + a_n } } } }
      | c = 
}}
{{eqn | r = \cfrac {a_0} {1 - \cfrac {a_1} {1 + a_1 - \cfrac {a_2} {1 + a_2 - \cfrac {a_3} {1 + a_3 - \cfrac {\ddots} {\ddots - \cfrac {a_{n - 1} } {1 + a_{n - 1} - \cfrac {a_n} {1 + a_n} } } } } } }
      | c = 
}}
{{end-eqn}}
Let $a_0 = \dfrac 1 A$, $a_1 = -\dfrac A B$, $a_2 = -\dfrac B C$, $a_3 = -\dfrac C D$, etc.
Then:
{{begin-eqn}}
{{eqn | l = \frac 1 A - \frac 1 B + \frac 1 C - \frac 1 D + \frac 1 E - \cdots
      | r = \frac 1 A + \paren {\frac 1 A} \paren {-\frac A B} + \paren {\frac 1 A} \paren {-\frac A B} \paren {-\frac B C} + \paren {\frac 1 A} \paren {-\frac A B} \paren {-\frac B C} \paren {-\frac C D} + \cdots
      | c = 
}}
{{eqn | r = a_0 + \paren {a_0} \paren {a_1} + \paren {a_0} \paren {a_1} \paren {a_2} + \paren {a_0} \paren {a_1} \paren {a_2} \paren {a_3} + \cdots
      | c = 
}}
{{eqn | r = \cfrac {\frac 1 A} {1 - \cfrac {-\frac A B} {1 + \paren {-\frac A B} - \cfrac {-\frac B C} {1 + \paren {-\frac B C} - \cfrac {-\frac C D} {1 + \paren {-\frac C D} - \cfrac \ddots \ddots} } } }
      | c = 
}}
{{eqn | r = \cfrac {\frac 1 A \times A} {1 \times A - \cfrac {-\frac A B \times A \times B} {1 \times B + \paren {-\frac A B} \times B - \cfrac {-\frac B C \times B \times C} {1 \times C + \paren {-\frac B C} \times C - \cfrac {-\frac C D \times C \times D} {1 \times D + \paren {-\frac C D} \times D - \cfrac \ddots \ddots} } } }
      | c = 
}}
{{eqn | r = \cfrac 1 {A + \cfrac {A^2} {B - A + \cfrac {B^2} {C - B + \cfrac {C^2} {D - C + \cfrac {D^2} {E - D + \cfrac \ddots \ddots} } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Leonhard Paul Euler}}
Theorem: Euler's Continued Fraction Formula/Corollary 2

:$A - B + C - D + E - \cdots = \cfrac A {1 + \cfrac {B} {A - B + \cfrac {A C} {B - C + \cfrac {B D} {C - D + \cfrac {C E} {D - E + \cfrac {\ddots} {\ddots} } } } } }$

Proof:
From Euler's Continued Fraction Formula, we have:
{{begin-eqn}}
{{eqn | l = a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots + a_0 a_1 a_2 a_3 \cdots a_n
      | r = a_0 \paren {1 + a_1 \paren {1 + a_2 \paren { 1 + a_3 \paren {\cdots + a_n } } } }
      | c = 
}}
{{eqn | r = \cfrac {a_0} {1 - \cfrac {a_1} {1 + a_1 - \cfrac {a_2} {1 + a_2 - \cfrac {a_3} {1 + a_3 - \cfrac {\ddots} {\ddots - \cfrac {a_{n - 1} } {1 + a_{n - 1} - \cfrac {a_n} {1 + a_n} } } } } } }
      | c = 
}}
{{end-eqn}}
Let $a_0 = A$, $a_1 = -\dfrac B A$, $a_2 = -\dfrac C B$, $a_3 = -\dfrac D C$, etc.
Then:
{{begin-eqn}}
{{eqn | l = A - B + C - D + E - \cdots
      | r = A + \paren {A} \paren {-\frac B A} + \paren {A} \paren {-\frac B A} \paren {-\frac C B} + \paren {A} \paren {-\frac B A} \paren {-\frac C B} \paren {-\frac D C} + \cdots
      | c = 
}}
{{eqn | r = a_0 + \paren {a_0} \paren {a_1} + \paren {a_0} \paren {a_1} \paren {a_2} + \paren {a_0} \paren {a_1} \paren {a_2} \paren {a_3} + \cdots
      | c = 
}}
{{eqn | r = \cfrac {A} {1 - \cfrac {-\frac B A} {1 + \paren {-\frac B A} - \cfrac {-\frac C B} {1 + \paren {-\frac C B} - \cfrac {-\frac D C} {1 + \paren {-\frac D C} - \cfrac {\ddots} {\ddots } } } } }
      | c = 
}}
{{eqn | r = \cfrac {A} {1 - \cfrac {-\frac B A \times A} {1 \times A + \paren {-\frac B A} \times A - \cfrac {-\frac C B \times A \times B} {1 \times B + \paren {-\frac C B} \times B - \cfrac {-\frac D C \times B \times C} {1 \times C + \paren {-\frac D C} \times C - \cfrac {\ddots} {\ddots } } } } }
      | c = 
}}
{{eqn | r = \cfrac A {1 + \cfrac {B} {A - B + \cfrac {A C} {B - C + \cfrac {B D} {C - D + \cfrac {C E} {D - E + \cfrac {\ddots} {\ddots} } } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Leonhard Paul Euler}}
Theorem: Continued Fraction for Pi plus Three

:$\pi + 3 = 6 + \cfrac {1^2} {6 + \cfrac {3^2} {6 + \cfrac {5^2} {6 + \cfrac {7^2} {6 + \cfrac {9^2} {6 + \cfrac \ddots \ddots} } } } }$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = S
      | r = \sum_{n \mathop = 1}^\infty  \frac {\paren {-1}^{n - 1} } {\paren {2 n} \paren {2 n + 1} \paren {2 n + 2} }
      | c = 
}}
{{eqn | n = 1
      | r = \frac 1 {2 \times 3 \times 4} - \frac 1 {4 \times 5 \times 6} + \frac 1 {6 \times 7 \times 8} - \frac 1 {8 \times 9 \times 10} + \cdots
      | c = 
}}
{{eqn | n = 2
      | r = \frac 1 4 \sum_{n \mathop = 1}^\infty \paren {\paren { \frac {\paren {-1}^{n - 1} } n} - \paren {\frac {4 \times \paren {-1}^{n - 1} } {2 n + 1} } + \paren {\frac {\paren {-1}^{n - 1} } {n + 1} } }
      | c = Partial Fraction Decomposition
}}
{{end-eqn}}
From Equation $2$, we have:
{{begin-eqn}}
{{eqn | l = S
      | r = \frac 1 4 \sum_{n \mathop = 1}^\infty \paren {\paren {\frac {\paren {-1}^{n - 1} } n} - \paren {\frac {4 \times \paren {-1}^{n - 1} } {2 n + 1} } + \paren {\frac {\paren {-1}^{n - 1} } {n + 1} } }
      | c = 
}}
{{eqn | r = \frac 1 4 \paren {\paren {1 - \frac 1 2 + \frac 1 3 - \frac 1 4 + \cdots} - \paren {4 \times \paren {\frac 1 3 - \frac 1 5 + \frac 1 7 - \frac 1 9 + \cdots} } + \paren {\frac 1 2 - \frac 1 3 + \frac 1 4 - \frac 1 5 + \cdots} }
      | c = 
}}
{{eqn | r = \frac 1 4 \paren {1 + \paren {4 \times \paren {-\frac 1 3 + \frac 1 5 - \frac 1 7 + \frac 1 9 - \cdots} } }
      | c = 
}}
{{eqn | r = \frac 1 4 \paren {1 - 4 + \paren {4 \times \paren {1 -\frac 1 3 + \frac 1 5 - \frac 1 7 + \frac 1 9 - \cdots} } }
      | c = adding $0$
}}
{{eqn | r = \frac 1 4 \paren {-3 + \paren {4 \times \paren {\frac \pi 4} } }
      | c = Leibniz's Formula for Pi
}}
{{eqn | r = \frac {\pi - 3} 4
      | c = 
}}
{{end-eqn}}
Theorem: Coefficients of Coordinates in General Equation of Plane Form Vector Perpendicular to Plane

Let $P$ be a plane that is described by the general equation:
:$\alpha_1 x + \alpha_2 y + \alpha_3 z = \gamma$
Let $\mathbf i$, $\mathbf j$ and $\mathbf k$ denote the unit vectors in the positive directions of the $x$-axis, $y$-axis and $z$-axis, respectively.
Then the vector:
:$\bsalpha = \alpha_1 \mathbf i + \alpha_2 \mathbf j + \alpha_3 \mathbf k$
is perpendicular to $P$.

Proof:
Let $A$ and $B$ be two points in $P$.
Let $\mathbf a$ and $\mathbf b$ be two vectors from the origin to $A$ and $B$, respectively.
Let $A$ and $B$ have the following coordinates:
:$A = \tuple {x_a, y_a, z_a}$
:$B = \tuple {x_b, y_b, z_b}$
Since the points are in $P$, they satisfy
:$\alpha_1 x_a + \alpha_2 y_a + \alpha_3 z_a = \gamma$
:$\alpha_1 x_b + \alpha_2 y_b + \alpha_3 z_b = \gamma$
Subtracting these two equations results in
{{begin-eqn}}
{{eqn | l = \alpha_1 \paren {x_a - x_b} + \alpha_2 \paren {y_a - y_b} + \alpha_3 \paren {z_a - z_b}
      | r = 0
}}
{{eqn | l = \paren {\alpha_1 \mathbf i + \alpha_2 \mathbf j + \alpha_3 \mathbf k} \cdot \paren {\mathbf a - \mathbf b}
      | r = 0
      | c = {{Defof|Dot Product}} and Definitions of $\mathbf a$ and $\mathbf b$
}}
{{eqn | l = \bsalpha \cdot \paren {\mathbf a - \mathbf b}
      | r = 0
      | c = Definition of $\bsalpha$
}}
{{end-eqn}}
Let $C$ be a point in $P$ such that $k \bsalpha = C$ for some $k \in \mathbb R$.
Since the choices of $A$ and $B$ were arbitrary, choose $A$ and $B$ so that $C$ is on $\overline {AB}$.
By Dot Product of Perpendicular Vectors, $\bsalpha$ is perpendicular to line segment $\overline {AB}$.
By Line Perpendicular to Plane, $\bsalpha$ is perpendicular to $P$.
{{qed}}
Category:Planes
Category:Equations of Planes
Category:Perpendiculars
in0q9utsh3l9m95d65xe0q04ga6k022
Theorem: Square Matrix has Linearly Dependent Rows iff Determinant is Zero

Let $M$ be an $n \times n$ square matrix.
Then:
:the rows of $M$ are linearly dependent
{{iff}}:
:$\map \det M = 0$

Proof:
=== Sufficient Condition ===
Let the rows of $M$ be linearly dependent.
Then there exists a set of coefficients $\set {\lambda_1, \lambda_2, \ldots, \lambda_n}$ such that:
:$\ds \sum_{i \mathop = 1}^n \lambda_i r_i = \mathbf 0$
where:
:$r_i$ is the $i$th row of $M$
:$\exists i \in \set {1, 2, \ldots, n} : \lambda_i \ne 0$
Let $D = \map \det M$.
In the following, let $D'$ denote the determinant of $M$ after having performed an elementary row operation on it.
Let us choose $k$ such that $\lambda_k \ne 0$.
Let row $k$ of $M$ be multiplied by $\lambda_k$.
This is an elementary row operation on $M$.
Hence by Effect of Elementary Row Operations on Determinant:
:$D' = \lambda_k D$
Add the following sum to row $k$ of $M$:
:$\ds \sum_{i \mathop = 1 \\ i \mathop \ne k}^n \lambda_i r_i$
This is also an elementary row operation on $M$.
Now:
{{begin-eqn}}
{{eqn | l = r_k
      | r = \lambda_k r_k + \sum_{i \mathop \ne k} \lambda_i r_i
}}
{{eqn | r = \sum_{i \mathop = 1}^n \lambda_k r_k
}}
{{eqn | r = \mathbf 0
      | c = rows of $M$ are linearly dependent
}}
{{end-eqn}}
So, the fact that the rows of $M$ are linearly dependent means that it is possible to set one row of $M$ to all zeros using elementary row operations.
By Effect of Elementary Row Operations on Determinant, the determinant of $M$ is unchanged.
Hence it is still the case that:
:$D' = \lambda_k D$
Row $k$ of $M$ can also be set to $\mathbf 0$ by multiplying it by zero.
By Effect of Elementary Row Operations on Determinant:
:$D' = 0$
Thus:
{{begin-eqn}}
{{eqn | l = D
      | r = D' / \lambda_k
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Transpose Exchanges Rows and Columns

Let $A$ be an $m \times n$ matrix over a set.
Let $r_k$ be the $k$th row of $A$ for $1 \leq k \leq m$.
Let $A^\intercal$ be the transpose of $A$.
Let $c_k$ be the $k$th column of $A^\intercal$.
Then, $r_k = c_k$.
Similarly, the $k$th column of $A$ is the $k$th row of $A^\intercal$.

Proof:
The $k$th row of $A$ is given by
:$r_k = \tuple {a_{k1}, a_{k2}, \ldots, a_{km} }$
where $a_{ij}$ is an matrix element of $A$.
The $k$th column of $A^\intercal$ is given by
:$c_k = \tuple {b_{1k}, b_{2k}, \ldots, b_{mk} }$
where $b_{ij}$ is an matrix element of $A^\intercal$.
According to the definition of transpose,
:$b_{ij} = a_{ji}$
Therefore,
{{begin-eqn}}
{{eqn | l = c_k
      | r = \tuple {b_{1k}, b_{2k}, \ldots, b_{mk} }
}}
{{eqn | r = \tuple {a_{k1}, a_{k2}, \ldots, a_{km} }
      | c = {{Defof|Transpose of Matrix}}
}}
{{eqn | r = r_k
}}
{{end-eqn}}
Also, {{mutatis}}, the columns of $A$ are the rows of $A^\intercal$.
{{qed}}
Category:Transposes of Matrices
Category:Matrices
tu5mv3fpqu90rw7htiksejd9ntw8wna
Theorem: Square Matrix has Linearly Dependent Columns iff Determinant is Zero

Let $M$ be an $n \times n$ square matrix.
Then:
:the columns of $M$ are linearly dependent
{{iff}}:
:$\map \det M = 0$

Proof:
Let $M^\intercal$ be the transpose of $M$.
By Determinant of Transpose:
:$\map \det M = 0 \iff \map \det {M^\intercal} = 0$
By Square Matrix has Linearly Dependent Rows iff Determinant is Zero:
:$\map \det {M^\intercal} = 0 \iff$ Rows of $M^\intercal$ are linearly dependent
By Transpose Exchanges Rows and Columns:
:Rows of $M^\intercal$ are linearly dependent $\iff$ Columns of $M$ are linearly dependent.
{{qed}}
Theorem: Union from Synthetic Basis is Topology/Open Set Axiom 2

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ fulfils {{Open-set-axiom|2}}.

Proof:
Let $U, V \in \tau$.
It is to be shown that:
:$U \cap V \in \tau$
Define:
:$\OO = \set {A \cap B: A, B \in \BB, \, A \subseteq U, \, B \subseteq V}$
By the definition of a synthetic basis:
:$\forall A, B \in \BB: A \cap B \in \tau$
Hence, by the definition of a subset, it follows that $\OO \subseteq \tau$.
By {{Open-set-axiom|1}}, which has been verified above for $\tau$, we have:
:$\ds \bigcup \OO \in \tau$
Since set intersection preserves subsets, we have:
:$\ds \forall W \in \OO: \exists A, B \in \BB: W = A \cap B \subseteq U \cap V$
By Union is Smallest Superset: General Result, it follows that:
:$\ds \bigcup \OO \subseteq U \cap V$
By the definition of $\tau$, it follows from Set is Subset of Union: General Result that:
:$\ds \forall x \in U \cap V: \exists A, B \in \BB: A \subseteq U, \, B \subseteq V: x \in A \cap B \subseteq \bigcup \OO$
That is, by the definition of a subset:
:$\ds U \cap V \subseteq \bigcup \OO$
By definition of set equality:
:$\ds U \cap V = \bigcup \OO \in \tau$
Theorem: Union from Synthetic Basis is Topology/Open Set Axiom 3

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ fulfils {{Open-set-axiom|3}}.

Proof:
By the definition of a synthetic basis, $\BB$ is a cover for $S$.
By Equivalent Conditions for Cover by Collection of Subsets, it follows that:
:$\ds S = \bigcup \BB \in \tau$
Theorem: Union from Synthetic Basis is Topology/Open Set Axiom 3

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ fulfils {{Open-set-axiom|3}}.

Proof:
By the definition of a synthetic basis, we have that:
:$\forall x \in X: \exists B \in \BB: x \in B \subseteq X$
Theorem: Union from Synthetic Basis is Topology/Open Set Axiom 1

Let $\BB$ be a synthetic basis on a set $X$.
Let $\ds \tau = \set {\bigcup \AA: \AA \subseteq \BB}$.
Then $\tau$ fulfils {{Open-set-axiom|1}}.

Proof:
Let $\AA \subseteq \tau$.
It is to be shown that:
:$\ds \bigcup \AA \in \tau$
Define:
:$\ds \AA' = \bigcup_{U \mathop \in \AA} \set {B \in \BB: B \subseteq U}$
By Union is Smallest Superset: Family of Sets, it follows that $\AA' \subseteq \BB$.
Hence, by Equivalence of Definitions of Topology Generated by Synthetic Basis and General Self-Distributivity of Set Union:
:$\ds \bigcup \AA = \bigcup_{U \mathop \in \AA} \bigcup \set {B \in \BB: B \subseteq U} = \bigcup \AA' \in \tau$
Theorem: Square Number ending in 10 Digits in Reverse Order

The next integer after $1 \, 111 \, 111 \, 111$ whose square ends in $0 \, 987 \, 654 \, 321$ is:
:$2 \, 380 \, 642 \, 361^2 = 5 \, 667 \, 458 \, 050 \, 987 \, 654 \, 321$

Proof:
{{ProofWanted|Is there a way to do this without an exhaustive search?}}
Theorem: Continued Fraction for Pi over N Times Real Cotangent Function

:$\dfrac \pi n \map \cot {\dfrac {\pi m} n} = \cfrac 1 {m + \cfrac {m^2} {n - 2 m + \cfrac {\paren {n - m}^2} {2 m + \cfrac {\paren {n + m}^2} {n - 2 m + \cfrac {\paren {2 n - m}^2} {2 m + \cfrac {\paren {2 n + m}^2} \ddots} } } } }$

Proof:
From {{Corollary|Mittag-Leffler Expansion for Cotangent Function|2}}, we have:
{{begin-eqn}}
{{eqn | l = \frac \pi n \map \cot {\frac {\pi m} n}
      | r = \frac 1 m + \sum_{k \mathop = 1}^\infty \paren {\frac 1 {k n + m} - \frac 1 {k n - m} }
      | c = 
}}
{{eqn | r = \frac 1 m + \paren {\frac 1 {n + m} - \frac 1 {n - m} } + \paren {\frac 1 {2 n + m} - \frac 1 {2 n - m} } + \paren {\frac 1 {3 n + m} - \frac 1 {3 n - m} } + \paren {\frac 1 {4 n + m} - \frac 1 {4 n - m} } + \cdots
      | c = 
}}
{{eqn | r = \frac 1 m - \frac 1 {n - m} + \frac 1 {n + m} - \frac 1 {2 n - m} + \frac 1 {2 n + m} - \frac 1 {3 n - m} + \frac 1 {3 n + m} - \frac 1 {4 n - m} + \frac 1 {4 n + m} - \cdots
      | c = 
}}
{{end-eqn}}
From {{Corollary|Euler's Continued Fraction Formula|1}}, we have:
:$\dfrac 1 A - \dfrac 1 B + \dfrac 1 C - \dfrac 1 D + \dfrac 1 E - \cdots = \cfrac 1 {A + \cfrac {A^2} {B - A + \cfrac {B^2} {C - B + \cfrac {C^2} {D - C + \cfrac {D^2} {E - D + \cfrac \ddots \ddots} } } } }$
:Setting $A = m$, $B = \paren {n - m}$, $C = \paren {n + m}$, $D = \paren {2 n - m}$, $E = \paren {2 n + m}$, $\cdots$, we get:
{{begin-eqn}}
{{eqn | o = 
      | r = \frac 1 m - \frac 1 {n - m} + \frac 1 {n + m} - \frac 1 {2 n - m} + \frac 1 {2 n + m} - \frac 1 {3 n - m} + \frac 1 {3 n + m} - \frac 1 {4 n - m} + \frac 1 {4 n + m} - \cdots
      | c = 
}}
{{eqn | r = \cfrac 1 {m + \cfrac {m^2} {\paren {n - m} - m + \cfrac {\paren {n - m}^2} {\paren {n + m} - \paren {n - m} + \cfrac {\paren {n + m}^2} {\paren {2 n - m} - \paren {n + m} + \cfrac {\paren {2 n - m}^2}{\paren {2 n + m} - \paren {2 n - m} + \cfrac {\paren {2 n + m}^2} \ddots} } } } }
      | c = 
}}
{{eqn | r = \cfrac 1 {m + \cfrac {m^2} {n - 2 m + \cfrac {\paren {n - m}^2} {2 m + \cfrac {\paren {n + m}^2} {n - 2 m + \cfrac {\paren {2 n - m}^2}{2 m + \cfrac {\paren {2 n + m}^2} \ddots} } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Cotangent of 22.5 Degrees

:$\cot 22.5 \degrees = \cot \dfrac \pi 8 = \sqrt 2 + 1$

Proof:
{{begin-eqn}}
{{eqn | l = \cot 22.5 \degrees
      | r = \frac {\cos 22.5 \degrees} {\sin 22.5 \degrees}
      | c = {{Defof|Cotangent/Complex Function|Cotangent}}
}}
{{eqn | r = \frac {\frac 1 2 \sqrt {2 + \sqrt 2} } {\frac 1 2 \sqrt {2 - \sqrt 2} }
      | c = {{sin|22.5}}, {{cos|22.5}}
}}
{{eqn | r = \frac {\sqrt {2 + \sqrt 2} \sqrt {2 + \sqrt 2} } {\sqrt {2 - \sqrt 2} \sqrt {2 + \sqrt 2}  }
      | c = multiplying top and bottom by $\sqrt {2 + \sqrt 2}$
}}
{{eqn | r = \frac {2 + \sqrt 2} {\sqrt {2^2 - 2} }
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {2 + \sqrt 2} {\sqrt 2}
      | c = 
}}
{{eqn | r = \sqrt 2 + 1
      | c = dividing top and bottom by $\sqrt 2$
}}
{{end-eqn}}
{{qed}}
Theorem: Closure and Complement Operations generate Monoid

Let $T = \struct {S, \tau}$ be a topological space.
Let $\AA$ be the set of subspaces of $T$.
Let $\Phi: \AA \to \AA$ be the set of sequences of compositions of mappings consisting of:
:complementation relative to $S$
:topological closure
:the identity mapping.
Let $\otimes: \Phi \times \Phi \to \Phi$ denote the binary operation on $\Phi$ defined as:
:$\forall \tuple {\phi, \phi} \in \Phi \times \Phi: \phi \otimes \phi := \phi \circ \phi$
where $\circ$ denotes composition of mappings.
Then $\struct {\Phi, \otimes}$ forms a monoid with as many as $14$ elements whose identity is the identity mapping.

Proof:
The fact that there are at most $14$ elements is demonstrated in the proof of maximum of Kuratowski's Closure-Complement Problem.
From that same page, we use the notation:
:let $a$ be used to denote the operation of taking the complement of $A$ relative to $S$: $\map a A = S \setminus A$
:let $b$ be used to denote the operation of taking the closure of $A$ in $T$: $\map b A = A^-$
:let $I$ be used to denote the identity operation on $A$, that is: $\map I A = A$.
:let the parentheses and the reference to $A$ be removed, so as to present, for example:
::$\map a {\map b {\map a A} }$
:as:
::$a b a$
where $A$ denotes an arbitrary element of $\AA$.
It is demonstrated there that the possible different subsets of $S$ that can be obtained from $A$ by applying $a$ and $b$ can be generated by none other than the following:
Theorem: Regular Open Set is Open

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$ be regular open in $T$.
Then $H$ is an open set of $T$.

Proof:
{{Recall|Regular Open Set|regular open set}}
{{:Definition:Regular Open Set}}
{{Recall|Interior (Topology)|set interior}}
{{:Definition:Interior (Topology)/Definition 2}}
Hence:
:as $H$ equals its interior
and:
:the interior of $H$ is an open set of $T$ by definition
the result follows.
{{qed}}
Category:Regular Open Sets
Category:Open Sets
guzwbo0z1fus8n9hr4xqjc1hdzwhjkn