avewright/proofwiki-math huggingface dataset:
Theorem: Characterization of Existence of Bifunctor Induced By One-Variable Functors/Necessary Condition

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
For each object $C \in \mathbf C$, let:
:$L_C: \mathbf D \to \mathbf E$ be a covariant functor.
For each object $D \in \mathbf D$, let:
:$M_D: \mathbf C \to \mathbf E$  be a covariant functor.
Let $F: \mathbf C \times \mathbf D \to \mathbf E$ be a bifunctor such that:
::$(1)\quad$ For each object $C \in \mathbf C : F(C, -) = L_C$
::$(2)\quad$ For each object $D \in \mathbf D : F(-, D) = M_D$
:where:
::$F(C, -)$ denotes the functor from $\mathbf D$ to $\mathbf E$ obtained by substitution of first variable with $C$
::$F(-, D)$ denotes the functor from $\mathbf C$ to $\mathbf E$ obtained by substitution of second variable with $D$
Then:
:for morphisms $f: C \to C' \in \mathbf C$ and $g: D \to D' \in \mathbf D$:
::$\map {M_{D'} } f \circ \map {L_C} g = \map {L_{C'} } g \circ \map {M_D} f$

Proof:
By definition of substitution of first variable:
:for each object $C \in \mathbf C$:
::for each object $D \in \mathbf D : \map {L_C} D = \map F {C, D}$
::for each mophism $g \in \mathbf D : \map {L_C} g = \map F {\operatorname{id}_C, g}$
By definition of substitution of second variable with $D$:
:for each object $D \in \mathbf D$, let:
::for each object $C \in \mathbf C : \map {M_D} C = \map F {C, D}$
::for each mophism $f \in \mathbf C : \map {M_D} f = \map F  {f, \operatorname{id}_D}$
The result follows immediately from Characterization of Bifunctor Induced By One-Variable Functors.
Theorem: Euler Characteristic of Sphere

Let $S$ be a surface which is homeomorphic to the sphere.
Then the Euler characteristic of $S$ is given by:
:$\map \chi S = 2$

Proof:
From the Euler Polyhedron Formula: 
:$V - E + F = 2$
where:
:$V$ is the number of vertices
:$E$ is the number of edges
:$F$ is the number of faces
of a convex polyhedron.
That is, the Euler characteristic of a convex polyhedron is $2$.
A convex polyhedron is topologically equivalent to the sphere.
From Euler Characteristic of Surface is Topological Invariant, the result follows.
{{qed}}
Theorem: Euler Number for Odd Index is Zero

Let $E_n$ be the $n$th Euler number.
Let $n$ be odd.
Then $E_n = 0$.

Proof:
{{Recall|Euler Numbers}}
{{:Definition:Euler Numbers}}
From Secant Function is Even:
{{begin-eqn}}
{{eqn | l = \sech x
      | r = \map \sech {-x}
      | c = Secant Function is Even
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 0}^\infty \frac {E_n x^n} {n!}
      | r = \sum_{n \mathop = 0}^\infty \frac {E_n \paren {-x}^n} {n!}
      | c = {{Defof|Euler Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 0}^\infty \frac {E_n x^n} {n!} - \sum_{n \mathop = 0}^\infty \frac {E_n \paren {-x}^n} {n!}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 0}^\infty \frac {E_n \paren {x^n - \paren {-x}^n} } {n!}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall x \in \openint {-\dfrac \pi 2} {\dfrac \pi 2}: \forall n \in \N
      | l = E_n \paren {x^n - \paren {-x}^n}
      | r = 0
      | c = 
}}
{{end-eqn}}
When $n$ is odd:
:$\paren {x^n - \paren {-x}^n} = 2 x^n$
and so for $E_n \paren {x^n - \paren {-x}^n} = 0$ for all $x$, it must be the case that $E_n = 0$.
{{qed}}
Theorem: Probability of Occurrence of Complementary Event

Let $\Pr$ be a probability measure on an event space $\Sigma$.
Let $A \in \Sigma$.
The probability of the occurrence of the complementary event to $A$ can be evaluated as:
:$\map \Pr {\overline A} = 1 - \map \Pr A$
where $\overline A$ denotes the complementary event to $A$.

Proof:
From Union of Event with Complement is Certainty:
:$\map \Pr {A \cup \overline A} = 1$
From Intersection of Event with Complement Can't Happen:
:$\map \Pr {A \cap \overline A} = 0$
Then:
{{begin-eqn}}
{{eqn | l = \map \Pr A + \map \Pr {\overline A}
      | r = \map \Pr {A \cup \overline A}
      | c = Probability of Union of Disjoint Events is Sum of Individual Probabilities
}}
{{eqn | r = 1
      | c = from above
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Condition for Differential to be Exact

The expression:
:$\ds \sum_i P_i \rd x_i$
where
:$\set {P_i}$ are real-valued functions over $\set {x_1, x_2, \ldots}$
is an '''exact differential''' {{iff}}:
:$\forall i, j : \dfrac {\partial P_i} {\partial x_j} = \dfrac {\partial P_j} {\partial x_i}$

Proof:
=== Sufficient Case ===
Let:
:$\ds \sum_i P_i \rd x_i$
be an exact differential.
By definition, this is the total differential of some real-valued function $f$.
Thus:
:$\forall i : P_i = \dfrac {\partial f} {\partial x_i}$
Therefore:
{{begin-eqn}}
{{eqn | l = \frac {\partial P_i} {\partial x_j}
      | r = \frac \partial {\partial x_j} \paren {\frac {\partial f} {\partial x_i} }
}}
{{eqn | r = \frac {\partial^2 f} {\partial x_j \partial x_i}
}}
{{eqn | r = \frac {\partial^2 f} {\partial x_i \partial x_j}
      | c = Clairaut's Theorem
}}
{{eqn | r = \frac \partial {\partial x_i} \paren {\frac {\partial f} {\partial x_j} }
}}
{{eqn | r = \frac {\partial P_j} {\partial x_i}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Constant Functor is Covariant Functor

Let $\mathbf C, \mathbf D$ be a categories.
Let $D \in \mathbf D$ be an object of $\mathbf D$.
Let $F: \mathbf C \to \mathbf D$ denote the $D$-valued constant functor.
Then:
:$F$ is a covariant functor.

Proof:
=== Constant Functor Preserves Composition ===
Let $f_1: C_1 \to C_2, f_2: C_2 \to C_3$ be morphisms in $\mathbf C$.
We have:
{{begin-eqn}}
{{eqn | l = \map F {f_2 \circ f_1}
      | r = \operatorname{id}_D
      | c = {{Defof|Constant Functor}}
}}
{{eqn | r = \operatorname{id}_D \circ \operatorname{id}_D
      | c = Identity Morphism is Idempotent
}}
{{eqn | r = F f_1 \circ F f_2
      | c = {{Defof|Constant Functor}}
}}
{{end-eqn}}
It follows that $F$ preserves composite morphisms.
{{qed|lemma}}
Theorem: Constant Natural Transformation is Natural Transformation

Let $\mathbf C, \mathbf D$ be a categories.
Let $f : D_1 \to D_2 \in \mathbf D$ be a morphism of $\mathbf D$.
Let $F_{D_1}: \mathbf C \to \mathbf D, F_{D_2}: \mathbf C \to \mathbf D$ denote the $D_1$, $D_2$-valued constant functors respectively.
Let $\eta: F_{D_1} \to F_{D_2}$ denote the $f$-valued constant natural transformation.
Then:
:$\eta$ is a natural transformation.

Proof:
Let $g: X \to Y \in \mathbf C$ be a morphism.
We have:
{{begin-eqn}}
{{eqn | l = f
      | r = f \circ \operatorname{id}_{D_1}
      | c = {{Defof|Identity Morphism}}
}}
{{eqn | r = \eta_Y \circ \operatorname{id}_{D_1}
      | c = {{Defof|Constant Natural Transformation}}
}}
{{eqn | n = 1
      | r = \eta_Y \circ F_{D_1} g
      | c = {{Defof|Constant Functor}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = f
      | r = \operatorname{id}_{D_2} \circ f
      | c = {{Defof|Identity Morphism}}
}}
{{eqn | r = \operatorname{id}_{D_2} \circ \eta_X
      | c = {{Defof|Constant Natural Transformation}}
}}
{{eqn | n = 2
      | r = F_{D_2} g \circ \eta_X
      | c = {{Defof|Constant Functor}}
}}
{{end-eqn}}
Equating $(1)$ with $(2)$:
:$\eta_Y \circ F_{D_1} g = F_{D_2} g \circ \eta_X$
It follows that $\eta : F_{D_1} \to F_{D_2}$ is a natural transformation.
{{qed}}
Theorem: Excenter of Triangle is Point of Intersection of Bisectors of Angles

Let $T$ be a triangle.
Let $X$ be an excenter of $T$.
Then $X$ is the intersection of:
:the angle bisector of the interior angle at one of the vertices of $T$
:the angle bisectors of the exterior angles at the other two vertices of $T$.

Proof:
:490px
Let $T = \triangle ABC$ be a triangle.
Let an excircle $\bigcirc DEF$ be constructed:
:tangent to $BC$ at $F$
:tangent to the production of $AC$ at $D$
:tangent to the production of $AB$ at $E$.
Let $X$ denote the center of $\bigcirc DEF$.
Let $r$ denote the radius of $\bigcirc DEF$.
By definition, $X$ is an excenter of $T$.
From Tangent to Circle is Perpendicular to Radius:
:$\angle ADX$ is a right angle
:$\angle AEX$ is a right angle
:$\angle BFX$ is a right angle
:$\angle CFX$ is a right angle.
Consider the triangles $\triangle ADX$ and $\triangle AEX$.
We have that:
:$\angle ADX = \angle AEX$ as both are right angles
:$DX = EX = r$
:$AX$ is common
Hence from the RHS Condition:
:$\triangle ADX = \triangle AEX$
Hence by definition $AX$ is the angle bisector of $\angle DAE$, which is the same as $\angle CAB$.
But $\angle CAB$ is the interior angle of $T$ at $A$.
{{qed|lemma}}
{{WLOG}}, let us consider the triangles $\triangle CDX$ and $\triangle CFX$.
We have that:
:$\angle CDX = \angle CFX$ as both are right angles
:$DX = FX = r$
:$CX$ is common
Hence from the RHS Condition:
:$\triangle CDX = \triangle CFX$
Hence by definition $CX$ is the angle bisector of $\angle DCF$.
But $\angle DCF$ is one of the exterior angle of $T$ at $C$.
{{qed|lemma}}
Using the same argument {{mutatis}}, considering the triangles $\triangle BEX$ and $\triangle BFX$, we see that $DX$ is the angle bisector of $\angle EBF$.
But $\angle EBF$ is one of the exterior angle of $T$ at $B$.
{{qed|lemma}}
Hence it has been shown that the excenter $X$ of $T$ is the intersection of:
:the angle bisector of the interior angle $\angle BAC$ of $T$
:the angle bisectors of the exterior angles $\angle DCF$ and $\angle EBF$ of $T$.
{{qed}}
Theorem: Field from Barycentric Charge Distribution

Let $\map \rho r$ be a barycentric charge density within space and centered at $\CC$ where $r$ is the distance from $\CC$.
Let the total amount of charge be finite.
:$\ds \int \map \rho {\mathbf r'} \rd V < \infty$
where $\mathbf r'$ ranges over the whole of space.
Let the field generated by point charge be given by the inverse square law.
Then, the field $\map {\mathbf F} {\mathbf r}$ generated by $\map \rho r$ at a position $\mathbf r$ is identical to that of a point charge at $\CC$ with a charge equal to the total charge contained within a sphere with radius $r = \size{\mathbf r}$.
That is,
:$\ds \map {\mathbf F} {\mathbf r} = \frac {k Q_{enc} } {r^2} \mathbf {\hat r}$
where
:$k$ is a physical constant,
:$\ds Q_{enc} = \int_{r' \mathop \le r} \map \rho {\mathbf r'} \rd V$, i.e., the charge enclosed within a sphere of radius $r$

Proof:
In general, the field generated by a charge density distribution at a position $\mathbf r$ is found by integrating the field generated at $\mathbf r$ by every charged volume element:
:$\ds \map {\mathbf F} {\mathbf r} = \int \rd \map {\mathbf F} {\mathbf r'}$
where $\mathbf r'$ is the position of a charged volume element $\rd V$.
The integration occurs over all space.
To evaluate this integral, we choose the volume element $\d V$ to be spherical shells of radius $r'$ and centered at $\CC$.
According to the Shell Theorem, if the position of $\mathbf r$ is outside the volume element, then the field due to this charged volume element is the same as a point charge placed at the shell's center.
{{begin-eqn}}
{{eqn | l = \d \map {\mathbf F} {\mathbf r}
      | r = \frac {k \rd Q} {r^2} \mathbf {\hat r}
      | c = {{Defof|Inverse Square Law}} and $r = \size {\mathbf r}$
}}
{{eqn | r = \frac {k \mathbf {\hat r} } {r^2} \map \rho {r'} \d V
      | c = $\d V$ is a spherical shell of radius $r'$ and infinitesimal thickness $\d r'$
}}
{{end-eqn}}
We could expand the volume element to $\d V = 4 \pi r'^2 \d r'$, but that's not necessary since we already know the result of the integration from the Shell Theorem.
So, the integral becomes
{{begin-eqn}}}
{{eqn | l = \map {\mathbf F} {\mathbf r}
      | r = \int_0^\infty \frac {k \mathbf {\hat r} } {r^2} \map \rho {r'} \d V
}}
{{eqn | r = \frac k {r^2} \mathbf {\hat r} \int_0^r \map \rho {r'} \d V
      | c = field from shells with $r' > r$ is zero due to Shell Theorem
}}
{{eqn | r = \frac {k Q_{enc} } {r^2} \mathbf {\hat r}
      | c = $Q_{enc}$ is the total charge enclosed within a sphere of radius $r$
}}
{{end-eqn}}
{{qed}}
{{help|The condition that the total charge is finite is probably sufficient, but not necessary. What condition is required for the field to exist and to avoid pathological cases like an infinite uniform charge density?}}
Theorem: Section Formula

Let $A$, $B$ and $P$ be collinear points.
Let $P$ divide $AB$ externally in the ratio $1 : k$.
Let the position vectors of $A$, $B$ and $P$ be $\mathbf a$, $\mathbf b$ and $\mathbf p$ respectively.
Then:
:$\mathbf p = \dfrac {k \mathbf a - \mathbf b} {k - 1}$

Proof:
{{ProofWanted|We surely have something similar for the internal division in ratio situation, but it wasn't called this. This and that need to be combined and rationalised.}}
Theorem: Symmetric Regular Right Bipyramid is not Isotoxal Polyhedron

Let $\PP$ be a symmetric regular right bipyramid.
Then $\PP$ is ''not'' an isotoxal polyhedron.
The only counterexample is the regular octahdron.

Proof:
First we note that the regular octahdron is an example of a regular polyhedron.
Hence from Regular Polyhedron is Isotoxal, the regular octahdron is {{afortiori}} an isotoxal polyhedron.
Otherwise, we note that the bases of the pyramids forming $\PP$ are polygons with $n$ sides, where $n \ne 4$.
Hence apices of the pyramids are vertices where $n$ edges meet.
However, the other vertices of $\PP$ are where $4$ edges meet.
Hence there can exist no symmetry that can superimpose an edges of $\PP$ which are adjacent to one of the apices onto one of the other edges.
Hence the result, by definition of isotoxal polyhedron.
{{qed}}
Theorem: Symmetric Regular Right Bipyramid is not Isogonal Polyhedron

Let $\PP$ be a symmetric regular right bipyramid.
Then $\PP$ is ''not'' in general an isogonal polyhedron.
The only counterexample is the regular octahdron.

Proof:
First we note that the regular octahdron is an example of a regular polyhedron.
Hence from Regular Polyhedron is Isogonal, the regular octahdron is {{afortiori}} an isogonal polyhedron.
Otherwise, we note that the bases of the pyramids forming $\PP$ are polygons with $n$ sides, where $n \ne 4$.
Hence apices of the pyramids are vertices where $n$ edges meet.
However, the other vertices of $\PP$ are where $4$ edges meet.
Hence there can exist no symmetry that can superimpose an apex onto one of the other vertices.
Hence the result, by definition of isogonal polyhedron.
{{qed}}
Theorem: Equiangular Polygon is not necessarily Isogonal

Let $\PP$ be an equiangular polygon.
Then it is not necessarily the case that $\PP$ is also isogonal.

Proof:
;Proof by Counterexample
Consider the following equiangular octagon $ABCDEFGH$:
:320px
where:
:all interior angles are $\dfrac {3 \pi} 4$ radians, that is, $135 \degrees$
:sides $AB$ and $EF$ are the same length $r$
:sides $CD$ and $GH$ are the same length $s$
:sides $BC$, $DE$, $FG$ and $HA$ are all the same length $t$
such that $r \ne s$, $r \ne t$ and $s \ne t$.
By definition, $ABCDEFGH$ is equiangular.
However, there exists no symmetry mapping that will take, for example, vertex $A$ to vertex $H$.
Hence, also by definition, $ABCDEFGH$ is not isogonal.
{{qed}}
Category:Equiangular Polygons
Category:Isogonal Polygons
1n84k5fxxv375w06zzqnzwxyprfrm9y
Theorem: General Solution to Differential Equation gives rise to Family of Curves

The general solution to a differential equation gives rise to a family of curves.
A particular solution may be identified by interpretation of boundary conditions.

Proof:
{{ProofWanted|The assertion is made in the source given, but I'm not sure whether this is true in absolute general}}
Theorem: Constant Functor is Contravariant Functor

Let $\mathbf C, \mathbf D$ be a categories.
Let $D \in \mathbf D$ be an object of $\mathbf D$.
Let $F: \mathbf C \to \mathbf D$ denote the $D$-valued constant functor.
Then:
:$F$ is a contravariant functor.

Proof:
=== Constant Functor Reverses Composition ===
Let $f_1: C_1 \to C_2, f_2: C_2 \to C_3$ be morphisms in $\mathbf C$.
We have:
{{begin-eqn}}
{{eqn | l = \map F {f_2 \circ f_1}
      | r = \operatorname{id}_D
      | c = {{Defof|Constant Functor}}
}}
{{eqn | r = \operatorname{id}_D \circ \operatorname{id}_D
      | c = Identity Morphism is Idempotent
}}
{{eqn | r = F f_2 \circ F f_1
      | c = {{Defof|Constant Functor}}
}}
{{end-eqn}}
It follows that $F$ reverses composite morphisms.
{{qed|lemma}}
Theorem: Diagonal Functor on Product Category is Covariant Functor

Let $\mathbf C$ be a 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 on product category.
Then:
:$\Delta$ is a covariant functor.

Proof:
=== $\Delta$ Preserves Composition ===
Let $f_1 : C_1 \to C_2, f_2:C_2 \to C_3 \in \mathbf C$ be morphisms.
We have:
{{begin-eqn}}
{{eqn | l = \map \Delta {f_2 \circ f_1}
      | r = \tuple{f_2 \circ f_1, f_2 \circ f_1}
      | c = {{Defof|Diagonal Functor on Product Category}}
}}
{{eqn | r = \tuple{f_2, f_2} \circ \tuple{f_1, f_1}
      | c = {{Defof|Product Category|Composition in Product Category}}
}}
{{eqn | r = \Delta f_2 \circ \Delta f_1
      | c = {{Defof|Diagonal Functor on Product Category}}
}}
{{end-eqn}}
It follows that $\Delta$ preserves compositions.
{{qed|lemma}}
Theorem: Diagonal Functor is Covariant Functor

Let $\mathbf C$ be a category.
Let $\mathbf J$ be a small index category.
Let $\mathbf {C^J}$ denote the functor category $\mathbf J$ into $\mathbf C$.
Let $\Delta_{\mathbf J}: \mathbf C \to \mathbf {C^J}$ denote the diagonal functor on index category.
Then:
:$\Delta_{\mathbf J}$ is a covariant functor.

Proof:
=== $\Delta_{\mathbf J}$ Preserves Composition ===
Let $f_1 : C_1 \to C_2, f_2:C_2 \to C_3 \in \mathbf C$ be morphisms.
We have:
{{begin-eqn}}
{{eqn | q = \forall i \in \mathbf J
      | l = \map {\Delta_{\mathbf J} } {f_2 \circ f_1}_i
      | r = f_2 \circ f_1
      | c = {{Defof|Diagonal Functor on Index Category}}
}}
{{eqn | r = \map {\Delta_{\mathbf J} } {f_2}_i \circ \map {\Delta_{\mathbf J} } {f_1}_i
      | c = {{Defof|Diagonal Functor on Index Category}}
}}
{{eqn | r = \paren{\map {\Delta_{\mathbf J} } {f_2} \circ \map {\Delta_{\mathbf J} } {f_1} }_i
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{end-eqn}}
Hence:
:$\map {\Delta_{\mathbf J} } {f_2 \circ f_1} = \map {\Delta_{\mathbf J} } {f_2} \circ \map {\Delta_{\mathbf J} } {f_1}$
It follows that $\Delta_{\mathbf J}$ preserves compositions.
{{qed|lemma}}
Theorem: Characterization of Adjunction Using Left Adjuncts of Triple Compositions

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let $F : \mathbf D \to \mathbf C$,  $G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\mathbf D \times \mathbf C$ denote the product category of $\mathbf D$ with $\mathbf C$.
For each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ let $\beta$ associate $\tuple{D, C}$ with a bijection:
:$\beta_{\tuple{D, C} } : \map {\operatorname{Hom}_{\mathbf D} } {D, GC} \to \map {\operatorname{Hom}_{\mathbf C} } {FD, C}$
For each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ let $\alpha_{\tuple{D, C} }$ denote the inverse of $\beta_{\tuple{D, C} }$:
:$\alpha_{\tuple{D, C} } = \beta_{\tuple{D, C} }^{-1} : \map {\operatorname{Hom}_{\mathbf C} } {FD, C} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GC}$
Then:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:for every:
::$f:D_2 \to D_1 \in \mathbf D$
::$h:D_1 \to G C_1 \in \mathbf D$
::$g:C_1 \to C_2 \in \mathbf C$
:we have:
::$\map {\beta_{\tuple{D_2, C_2} } } {G g \circ h \circ f} = g \circ \map {\beta_{\tuple{D_1, C_1} } } h \circ F f$
That is, given commutative diagram in $\mathbf D$:
::<nowiki>$\begin{xy}
<5.5em,5em>*+{D_1} = "TL",
<14.5em,5em>*+{D_2} = "TR",
<5.5em,0em>*+{G C_1} = "BL",
<14.5em,0em>*+{G C_2} = "BR",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{G g},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{h},
"TR";"BR" **@{.} ?>*@{>} ?<>(.5)*!/_2.5em/{G g\circ h \circ f},
\end{xy}$</nowiki>
the following diagram commutes in $\mathbf C$:
::<nowiki>$\begin{xy}
<0em,5em>*+{F D_1} = "TL",
<9em,5em>*+{F D_2} = "TR",
<0em,0em>*+{C_1} = "BL",
<9em,0em>*+{C_2} = "BR",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^3.0em/{\map {\beta_{\tuple{D_1, C_1} } } h},
"TR";"BR" **@{.} ?>*@{>} ?<>(.5)*!/_5.0em/{\map {\beta_{\tuple{D_2, C_2} } } {G g \circ h \circ f} },
\end{xy}$</nowiki>

Proof:
From Characterization of Adjunction Using Right Adjuncts of Triple Compositions:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(2):\quad$for every:
::$f:D_2 \to D_1 \in \mathbf D$
::$h:F D_1 \to C_1 \in \mathbf D$
::$g:C_1 \to C_2 \in \mathbf C$
:we have:
::$\map {\alpha_{\tuple{D_2, C_2} } } {g \circ h \circ F f} = G g \circ \map {\alpha_{\tuple{D_1, C_1} } } h \circ f$
It is to be shown that $(1)$ holds {{iff}} $(2)$ holds.
Theorem: Product of Category of Sets

Let $\mathbf{Sets}$ be the category of sets.
Let $I$ be an indexing set.
Let $\family {S_i}_{i\in I}$ be a family of sets.
Let $\ds S := \prod_{i \mathop \in I} S_i$ be the Cartesian product of $\family {S_i}_{i\in I}$.
Let $\sequence {\pr_i: S \to S_i}_{i\in I}$ be the family of the  projections.
Then $S$ together with $\sequence{\pr_i}_{i \in I}$ is the product of $\family {S_i}_{i \in I}$ in $\mathbf{Sets}$.

Proof:
{{ProofWanted}}
Category:Category of Sets
hd2hvj8b3wm1sp7uk698dbborhmwtdm
Theorem: Complete Countable Metric Space has Isolated Point

Let $\struct {X, d}$ be a countable complete metric space.
Then $X$ has an isolated point.

Proof:
Write:
:$\ds X = \bigcup_{x \mathop \in X} \set x$
This is a countable union.
From Finite Subset of Metric Space is Closed, $\set x$ is closed in $X$ for each $x \in X$.
By the Baire Category Theorem, $\struct {X, d}$ is a Baire space.
By Baire Space is Non-Meager, $\struct {X, d}$ is not meager.
Hence for some $x_0 \in X$, $\set {x_0}$ is not nowhere dense.
That is:
:$\set {x_0}^\circ \ne \O$
where $\circ$ denotes interior.
That is, by the definition of an open set, there exists $\epsilon > 0$ such that:
:$\map {B_\epsilon} {x_0} \subseteq \set {x_0}$
where $\map {B_\epsilon} {x_0}$ denotes the open ball of radius $\epsilon$ and center $x_0$. 
That is:
:$\map {B_\epsilon} {x_0} = \set {x_0}$
Hence $x_0$ is an isolated point.
{{qed}}
Category:Metric Spaces
Category:Isolated Points
dl9r2ilh2gpa9zlmofy11zl6ugkew6m
Theorem: Continuous Real Function Vanishing Almost Everywhere is Zero Function

Let $I$ be an open interval.
Let $\lambda$ be the Lebesgue measure on $I$. 
Let $f : I \to \R$ be a continuous function be such that:
:$\map f x = 0$ for almost all $x \in I$.
Then:
:$\map f x = 0$ for all $x \in I$.

Proof:
{{AimForCont}} there exists $x_0 \in I$ such that:
:$\map f {x_0} \ne 0$
so that:
:$\cmod {\map f {x_0} } > 0$
Since $f$ is continuous function at $x_0$, there exists $\delta > 0$ such that:
:for all $x \in \openint {x_0 - \delta} {x_0 + \delta} \cap I$, we have:
::$\cmod {\map f x - \map f {x_0} } < \dfrac {\cmod {\map f {x_0} } } 2$
We can pick $\delta > 0$ such that:
:$\openint {x_0 - \delta} {x_0 + \delta} \subseteq I$
By the Reverse Triangle Inequality, we have:
:$\ds \size {\size {\map f x} - \size {\map f {x_0} } } < \dfrac {\cmod {\map f {x_0} } } 2$
That is:
:$\ds \size {\map f x} > \size {\map f {x_0} } - \frac {\cmod {\map f {x_0} } } 2 = \frac {\size {\map f {x_0} } } 2$
In particular:
:$\size {\map f x} > 0$ for all $x \in \tuple {x_0 - \delta, x_0 + \delta}$.
From Measure of Interval is Length, we have:
:$\map \lambda {\tuple {x_0 - \delta, x_0 + \delta} } = 2 \delta$
Hence we have:
:$\map \lambda {\set {x \in I : \map f x \ne 0} } \ge 2 \delta > 0$
Hence it is not the case that:
:$\map f x = 0$ for almost all $x \in I$
a contradiction.
{{qed}}
Category:Lebesgue Measure
Category:Continuous Real Functions
cc4jlnejnuukkmkhijejzph7d5hdt4z