avewright/proofwiki-math huggingface dataset:
Theorem: Integral of Modulus of Continuous Real Function is Zero iff Zero Function

Let $I$ be an open interval.
Let $\lambda$ be the Lebesgue measure on $I$.
Let $f : I \to \R$ be a continuous real function such that:
:$\ds \int_I \size f \rd \lambda = 0$
Then $f = 0$.

Proof:
From Measurable Function Zero A.E. iff Absolute Value has Zero Integral, we have:
:$\map f x = 0$ for $\lambda$-almost all $x \in I$.
From Continuous Real Function Vanishing Almost Everywhere is Zero Function, we have that:
:$\map f x = 0$ for all $x \in I$.
{{qed}}
Category:Integrals of Integrable Functions
Category:Continuous Real Functions
7v3u13hx8ga8o85qg3dgjyg0fv91m4p
Theorem: P-Sequence Space is Strictly Increasing in p

Let $\GF \in \set {\R, \C}$.
Let $p, q \in \hointr 1 \infty$ be such that $1 \le p < q$.
Let $\map {\ell_p} {\N, \GF}$ and $\map {\ell_q} {\N, \GF}$ be the $p$ and $q$-sequence spaces. 
Then:
:$\map {\ell_p} {\N, \GF} \subsetneq \map {\ell_q} {\N, \GF}$

Proof:
We first show that $\map {\ell_p} {\N, \GF} \subseteq \map {\ell_q} {\N, \GF}$.
Let $\phi \in \map {\ell_p} {\N, \GF}$.
From Terms in Convergent Series Converge to Zero, we have $\map \phi n \to 0$ as $n \to \infty$. 
Hence there exists $N \in \N$ such that $\cmod {\map \phi n} < 1$ for $n \ge N$.
Then we have:
:$\cmod {\map \phi n}^q < \cmod {\map \phi n}^p$ for $n \ge N$.
We therefore have that:
:$\ds \sum_{n \mathop = N}^\infty \cmod {\map \phi n}^q < \sum_{n \mathop = N}^\infty \cmod {\map \phi n}^p < \infty$
Writing:
:$\ds \sum_{n \mathop = 1}^\infty \cmod {\map \phi n}^q = \sum_{n \mathop = 1}^{N - 1} \cmod {\map \phi n}^q + \sum_{n \mathop = N}^\infty \cmod {\map \phi n}^q$
we conclude that:
:$\ds \sum_{n \mathop = 1}^\infty \cmod {\map \phi n}^q < \infty$
To show that $\map {\ell_p} {\N, \GF} \ne \map {\ell_q} {\N, \GF}$, we find $\phi \in \map {\ell_q} {\N, \GF} \setminus \map {\ell_p} {\N, \GF}$.
Define $\phi : \N \to \R$ by $\map \phi n = n^{-1/p}$.
We then have:
:$\ds \sum_{n \mathop = 1}^\infty \cmod {\map \phi n}^p = \sum_{n \mathop = 1}^\infty \frac 1 n = \infty$
by Harmonic Series is Divergent. 
On the other hand, we have:
:$\ds \frac q p > 1$
and hence:
:$\ds \sum_{n \mathop = 1}^\infty \cmod {\map \phi n}^q = \sum_{n \mathop = 1}^\infty \frac 1 {n^{q/p} } < \infty$
by Convergence of P-Series.
Hence $\phi \in \map {\ell_q} {\N, \GF} \setminus \map {\ell_p} {\N, \GF}$.
We conclude that:
:$\map {\ell_p} {\N, \GF} \subsetneq \map {\ell_q} {\N, \GF}$
{{qed}}
Category:P-Sequence Spaces
2cb3yphsw0o0t1gdfqztk2r7yho43gz
Theorem: Nth Forward Difference is Constant iff Function is Polynomial of Degree N/Corollary

Let $y = \map f x$ be a real function.
Let $\Delta y$ denote the forward difference operator on $y$.
Let $f$ be a polynomial function of degree $n$.
Then $\Delta^{n + 1} y$ is zero for all $y$.

Proof:
By definition of $n$th forward difference operator:
{{begin-eqn}}
{{eqn | l = \map {\Delta^{n + 1} f} {x_i}
      | r = \map \Delta {\map {\Delta^n f} {x_i} }
      | c = 
}}
{{eqn | r = \Delta^n \map f {x_{i + 1} } - \Delta^n \map f {x_i}
      | c = 
}}
{{end-eqn}}
From Nth Forward Difference is Constant iff Function is Polynomial of Degree N:
:$\Delta^n \map f {x_{i + 1} } = \Delta^n \map f {x_i}$
Hence the result.
{{qed}}
Theorem: Existence of Null Sequence not in any P-Sequence Space

Let $\GF \in \set {\R, \C}$.
For each $p \in \hointr 1 \infty$, let $\map {\ell_p} {\N, \GF}$ be the $p$-sequence space.
Then there exists $\phi : \N \to \GF$ such that $\map \phi n \to 0$ as $n \to \infty$, yet:
:$\ds \phi \not \in \bigcup_{1 \le p < \infty} \map {\ell_p} {\N, \GF}$

Proof:
Define $\phi : \N \to \R$ by:
:$\ds \map \phi n = \frac 1 {\map \log n}$ for $n \in \N$.
Let $p \in \hointr 1 \infty$. 
From Order of Natural Logarithm Function, we have:
:$\ds \map \log n \le p n^{1/p}$ for each $n \in \N$.
Hence:
:$\ds \frac 1 {\map \log n} \ge \frac 1 p n^{-1/p}$
We therefore have:
:$\ds \frac 1 {\paren {\map \log n}^p} \ge p^{-p} n^{-1}$
By Harmonic Series is Divergent, we have:
:$\ds \sum_{n \mathop = 1}^\infty p^{-p} n^{-1} = \infty$ 
and hence:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 {\paren {\map \log n}^p} = \infty$
Hence $\phi \not \in \map {\ell_p} {\N, \GF}$.
Since $p \in \hointr 1 \infty$ was arbitrary, we have:
:$\ds \phi \not \in \bigcup_{1 \le p < \infty} \map {\ell_p} {\N, \GF}$
{{qed}}
Category:P-Sequence Spaces
tp59r2kwl5m58vser0eneg3418uaz5y
Theorem: Characterization of Adjunction Using Right Adjuncts of 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 $\alpha$ associate $\tuple{D, C}$ with a bijection:
:$\alpha_{\tuple{D, C} } : \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}}:
:$(1)\quad$ for every $h:FD \to C_1 \in \mathbf C$ and $g:C_1 \to C_2 \in \mathbf C$
::$\qquad\qquad\map {\alpha_{\tuple{D, C_2} } } {g \circ h} = Gg \circ \map {\alpha_{\tuple{D, C_1} } } h$
:$(2)\quad$ for every $f:D_2 \to D_1 \in \mathbf D$ and $h:FD_1 \to C \in \mathbf C$:
::$\qquad\qquad\map {\alpha_{\tuple{D_2, C} } } {h \circ Ff} = \map {\alpha_{\tuple{D_1, C} } } h \circ f$
That is, given commutative diagrams in $\mathbf C$:
:<nowiki>$\begin{xy}
<8em,5em>*+{FD} = "TC2",
<3.5em,0em>*+{C_1} = "BL2",
<12.5em,0em>*+{C_2} = "BR2",
"BL2";"BR2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TC2";"BL2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{h},
"TC2";"BR2" **@{.} ?>*@{>} ?<>(.7)*!/_1.8em/{g \circ h},
<23.5em,5em>*+{FD_1} = "TL",
<32.5em,5em>*+{FD_2} = "TR",
<28em,0em>*+{C} = "BC",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F f},
"TL";"BC" **@{-} ?>*@{>} ?<>(.4)*!/^1em/{h},
"TR";"BC" **@{.} ?>*@{>} ?<>(.3)*!/_1.8em/{h \circ F f},
\end{xy}$</nowiki>
the following diagrams commute in $\mathbf D$:
:<nowiki>$\begin{xy}
<4.5em,5em>*+{D} = "TC2",
<0em,0em>*+{G C_1} = "BL2",
<9em,0em>*+{G C_2} = "BR2",
"BL2";"BR2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{Gg},
"TC2";"BL2" **@{-} ?>*@{>} ?<>(0.9)*!/^2.5em/{\map {\alpha_{\tuple{D, C_1} } } h},
"TC2";"BR2" **@{.} ?>*@{>} ?<>(0.95)*!/_3.3em/{\map {\alpha_{\tuple{D, C_2} } } {g \circ h} },
<20em,5em>*+{D_1} = "TL",
<29em,5em>*+{D_2} = "TR",
<24.5em,0em>*+{G C} = "BC",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"TL";"BC" **@{-} ?>*@{>} ?<>(.1)*!/^2.5em/{\map {\alpha_{\tuple{D_1, C} } } h},
"TR";"BC" **@{.} ?>*@{>} ?<>(-.1)*!/_3.3em/{\map {\alpha_{\tuple{D_2, C} } } {h \circ F 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}}:
:$(3):\quad$ for every $f:D_2 \to D_1 \in \mathbf D$, $h:FD_1 \to C_1 \in \mathbf C$ and $g:C_1 \to C_2 \in \mathbf C$:
::$\map {\alpha_{\tuple{D_2, C_2} } } {g \circ h \circ Ff} = Gg \circ \map {\alpha_{\tuple{D_1, C_1} } } h \circ f$
The proof will now proceed to show that $(3)$ holds {{iff}} $(1)$ and $(2)$ hold.
Theorem: Barycentric Coordinates are Unique iff Vertices are Affinely Independent

Let $V = \tuple {v_0, v_1, \ldots, v_k}$ be a set of $k + 1$ vertices in $\mathbb R^k$.
Let $x$ be any point in $\mathbb R^k$.
Let $\tuple {\lambda_0, \lambda_1, \ldots, \lambda_k}$ be the barycentric coordinates of $x$ {{WRT}} the vertices.
Then the barycentric coordinates are unique {{iff}} $V$ is affinely independent.

Proof:
=== Necessary Case ===
Let $V$ be affinely independent.
{{AimForCont}} $\tuple {\beta_0, \beta_1, \ldots, \beta_k}$ are other barycentric coordinates for the point $x$ where:
:$\exists p \in \closedint 0 k : \beta_p \ne \lambda_p$
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \sum_{i \mathop = 0}^k \lambda_i v_i
}}
{{eqn | r = \sum_{i \mathop = 0}^k \beta_i v_i
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | ll = \leadsto
      | l = \sum_{i \mathop = 0}^k \lambda_i v_i - \sum_{i \mathop = 0}^k \beta_i v_i
      | r = 0
}}
{{eqn | ll = \leadsto
      | l = \sum_{i \mathop = 0}^k \paren {\lambda_i - \beta_i} v_i
      | r = 0
      | c = Linear Combination of Indexed Summations
}}
{{end-eqn}}
Pulling the term with index $p$ out of the summation:
{{begin-eqn}}
{{eqn | l = \paren {\lambda_p - \beta_p} v_p + \sum_{i \mathop = 0 \\ i \mathop \ne p}^k \paren {\lambda_i - \beta_i} v_i
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \paren {\lambda_p - \beta_p} v_p
      | r = -\sum_{i \mathop = 0 \\ i \mathop \ne p}^k \paren {\lambda_i - \beta_i} v_i
}}
{{eqn | ll= \leadsto
      | l = v_p
      | r = -\sum_{i \mathop = 0 \\ i \mathop \ne p}^k \frac {\paren {\lambda_i - \beta_i} } {\paren {\lambda_p - \beta_p} } v_i
}}
{{end-eqn}}
Thus the vertex $v_p$ is a linear combination of $V \setminus v_p$.
The sum of the coefficients in the linear combination is given by:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 0 \\ i \mathop \ne p}^k -\frac {\paren {\lambda_i - \beta_i} } {\paren {\lambda_p - \beta_p} }
      | r = \frac {\lambda_p - \beta_p} {\lambda_p - \beta_p} + \sum_{i \mathop = 0}^k -\frac {\paren {\lambda_i - \beta_i} } {\paren {\lambda_p - \beta_p} }
      | c = adding and subtracting $\paren {\lambda_p - \beta_p} / \paren {\lambda_p - \beta_p}$
}}
{{eqn | r = 1 - \sum_{i \mathop = 0}^k \frac {\paren {\lambda_i - \beta_i} } {\paren {\lambda_p - \beta_p} }
}}
{{eqn | r = 1 - \frac 1 {\lambda_p - \beta_p} \paren {\sum_{i \mathop = 0}^k \lambda_i - \sum_{i \mathop = 0}^k \beta_i}
      | c = Linear Combination of Indexed Summations
}}
{{eqn | r = 1 - \frac 1 {\lambda_p - \beta_p} \paren {1 - 1}
      | c = {{Defof|Barycentric Coordinates}}
}}
{{eqn | r = 1
}}
{{end-eqn}}
Therefore, the vertex $v_p$ is affinely dependent on $V \setminus v_p$.
Therefore, $V$ is not affinely independent.
Since this contradicts the initial assumption that the vertices are affinely independent, the supposition that:
:$\exists p \in \closedint 0 k : \beta_p \ne \lambda_p$
is false.
Therefore:
:$\forall p \in \closedint 0 k : \beta_p = \lambda_p$
Thus barycentric coordinates are unique.
{{qed|lemma}}
Theorem: Cyclic Group is Finitely Generated

Let $\CC$ be a cyclic group.
Then $\CC$ is finitely generated.

Proof:
Let $\CC$ be a cyclic group.
Then by definition of cyclic group:
:$\exists g \in \CC: \CC = \gen g$
where $\gen g$ is the generator of $\CC$.
As $\set g$ is a finite set the result follows by definition of finitely generated group.
{{qed}}
Theorem: Characterization of Adjunction Using Right Adjuncts of Morphisms

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 $\alpha$ associate $\tuple{D, C}$ with a bijection:
:$\alpha_{\tuple{D, C} } : \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}}:
:$(1)\quad$ for every $g:FD \to C \in \mathbf C$:
::$\qquad\qquad\map {\alpha_{\tuple{D, C} } } {g} = Gg \circ \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD}}$
:$(2)\quad$ for every $f:D_2 \to D_1 \in \mathbf D$:
::$\qquad\qquad\map {\alpha_{\tuple{D_2, FD_1} } } {Ff} = \map {\alpha_{\tuple{D_1, FD_1} } } {\operatorname{id}_{FD_1}} \circ f$
That is, the following diagrams commute in $\mathbf D$:
:<nowiki>$\begin{xy}
<4.5em,5em>*+{D} = "TC2",
<0em,0em>*+{GFD} = "BL2",
<9em,0em>*+{GC} = "BR2",
"BL2";"BR2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{Gg},
"TC2";"BL2" **@{-} ?>*@{>} ?<>(0.95)*!/^3.0em/{\map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD} } },
"TC2";"BR2" **@{.} ?>*@{>} ?<>(0.9)*!/_2.5em/{\map {\alpha_{\tuple{D, C} } } {g} },
<21em,5em>*+{D_1} = "TL",
<30em,5em>*+{D_2} = "TR",
<25.5em,0em>*+{GFD_1} = "BC",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"TL";"BC" **@{-} ?>*@{>} ?<>(-.15)*!/^3.3em/{\map {\alpha_{\tuple{D_1, FD_1} } } {\operatorname{id}_{FD_1} } },
"TR";"BC" **@{.} ?>*@{>} ?<>(-.15)*!/_2.8em/{\map {\alpha_{\tuple{D_2, FD_1} } } {F f} },
\end{xy}$</nowiki>

Proof:
From Characterization of Adjunction Using Right Adjuncts of Compositions:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(3)\quad$ for every $h:FD \to C_1 \in \mathbf C$ and $g:C_1 \to C_2 \in \mathbf C$
::$\qquad\qquad\map {\alpha_{\tuple{D, C_2} } } {g \circ h} = Gg \circ \map {\alpha_{\tuple{D, C_1} } } h$
:$(4)\quad$ for every $f:D_2 \to D_1 \in \mathbf D$ and $h:FD_1 \to C \in \mathbf C$:
::$\qquad\qquad\map {\alpha_{\tuple{D_2, C} } } {h \circ Ff} = \map {\alpha_{\tuple{D_1, C} } } h \circ f$
The proof will now proceed to show that $(3)$ and $(4)$ hold {{iff}} $(1)$ and $(2)$ hold.
Theorem: Characterization of Adjunction Using Left Adjuncts of 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}}:
:$(1):\quad$ for every $h:D \to G C_1 \in \mathbf D$ and $g:C_1 \to C_2 \in \mathbf C$:
::$\qquad\qquad\map {\beta_{\tuple{D, C_2} } } {G g \circ h} = g \circ \map {\beta_{\tuple{D, C_1} } } h$
:$(2):\quad$ for every $f:D_2 \to D_1 \in \mathbf D$ and $h:D_1 \to G C \in \mathbf D$:
::$\qquad\qquad\map {\beta_{\tuple{D_2, C} } } {h \circ f} = \map {\beta_{\tuple{D_1, C} } } h \circ F f$
That is, given commutative diagram in $\mathbf D$:
::<nowiki>$\begin{xy}
<7em,5em>*+{D} = "TC",
<2.5em,0em>*+{G C_1} = "BL",
<11.5em,0em>*+{G C_2} = "BR",
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{G g},
"TC";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{h},
"TC";"BR" **@{.} ?>*@{>} ?<>(.8)*!/_2em/{G g\circ h},
<24em,5em>*+{D_1} = "TL",
<33em,5em>*+{D_2} = "TR",
<28.5em,0em>*+{G C} = "BC",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"TL";"BC" **@{-} ?>*@{>} ?<>(.4)*!/^1em/{h},
"TR";"BC" **@{.} ?>*@{>} ?<>(.25)*!/_1.5em/{h \circ f},
\end{xy}$</nowiki>
the following diagrams commute in $\mathbf C$:
::<nowiki>$\begin{xy}
<4.5em,5em>*+{F D} = "TC",
<0em,0em>*+{C_1} = "BL",
<9em,0em>*+{C_2} = "BR",
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TC";"BL" **@{-} ?>*@{>} ?<>(.9)*!/^2.5em/{\map {\beta_{\tuple{D, C_1} } } h},
"TC";"BR" **@{.} ?>*@{>} ?<>(1.0)*!/_3.5em/{\map {\beta_{\tuple{D, C_2} } } {G g \circ h} },
<21em,5em>*+{F D_1} = "TL",
<30em,5em>*+{F D_2} = "TR",
<25.5em,0em>*+{C} = "BC",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F f},
"TL";"BC" **@{-} ?>*@{>} ?<>(0)*!/^3.0em/{\map {\beta_{\tuple{D_1, C} } } h},
"TR";"BC" **@{.} ?>*@{>} ?<>(-0.1)*!/_3.0em/{\map {\beta_{\tuple{D_2, C} } } {h \circ f} },
\end{xy}$</nowiki>

Proof:
From Characterization of Adjunction Using Right Adjuncts of Compositions:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(3):\quad$ for every $h:FD \to C_1 \in \mathbf C$ and $g:C_1 \to C_2 \in \mathbf C$
::$\qquad\qquad\map {\alpha_{\tuple{D, C_2} } } {g \circ h} = Gg \circ \map {\alpha_{\tuple{D, C_1} } } h$
:$(4):\quad$ for every $f:D_2 \to D_1 \in \mathbf D$ and $h:FD_1 \to C \in \mathbf C$:
::$\qquad\qquad\map {\alpha_{\tuple{D_2, C} } } {h \circ Ff} = \map {\alpha_{\tuple{D_1, C} } } h \circ f$
It is to be shown that $(1)$ and $(2)$ hold {{iff}} $(3)$ and $(4)$ hold.
Theorem: Characterization of Adjunction Using Left Adjuncts of Morphisms

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}}:
:$(1):\quad$ for every $g:C_1 \to C_2 \in \mathbf C$:
::$\qquad\qquad\map {\beta_{\tuple{GC_1, C_2} } } {G g} = g \circ \map {\beta_{\tuple{GC_1, C_1} } } {\operatorname{id}_{GC_1}}$
:$(2):\quad$ for every $f:D \to GC \in \mathbf D$:
::$\qquad\qquad\map {\beta_{\tuple{D, C} } } f = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } \circ F f$
That is, the following diagrams commute in $\mathbf C$:
::<nowiki>$\begin{xy}
<4.5em,5em>*+{FGC_1} = "TC",
<0em,0em>*+{C_1} = "BL",
<9em,0em>*+{C_2} = "BR",
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TC";"BL" **@{-} ?>*@{>} ?<>(1.1)*!/^3.5em/{\map {\beta_{\tuple{GC_1, C_1} } } {\operatorname{id}_{GC_1} } },
"TC";"BR" **@{.} ?>*@{>} ?<>(1.2)*!/_3.5em/{\map {\beta_{\tuple{GC_1, C_2} } } {G g} },
<24em,5em>*+{FGC} = "TL",
<33em,5em>*+{F D} = "TR",
<28.5em,0em>*+{C} = "BC",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F f},
"TL";"BC" **@{-} ?>*@{>} ?<>(0)*!/^3.0em/{\map {\beta_{\tuple{{GC}, C} } } {\operatorname{id}_{GC} } },
"TR";"BC" **@{.} ?>*@{>} ?<>(0.1)*!/_2.2em/{\map {\beta_{\tuple{D, C} } } f},
\end{xy}$</nowiki>

Proof:
From Characterization of Adjunction Using Right Adjuncts of Compositions:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(3):\quad$ for every $h:D \to G C_1 \in \mathbf D$ and $g:C_1 \to C_2 \in \mathbf C$:
::$\qquad\qquad\map {\beta_{\tuple{D, C_2} } } {G g \circ h} = g \circ \map {\beta_{\tuple{D, C_1} } } h$
:$(4):\quad$ for every $f:D_2 \to D_1 \in \mathbf D$ and $h:D_1 \to G C \in \mathbf D$:
::$\qquad\qquad\map {\beta_{\tuple{D_2, C} } } {h \circ f} = \map {\beta_{\tuple{D_1, C} } } h \circ F f$
The proof will now proceed to show that $(3)$ and $(4)$ hold {{iff}} $(1)$ and $(2)$ hold.
Theorem: Floor Function/Examples/Floor of 3.2

:$\floor {3 \cdotp 2} = 3$

Proof:
We have that:
:$3 \le 3 \cdotp 2 < 4$
Hence $3$ is the floor of $3 \cdotp 2$ by definition.
{{qed}}
Theorem: Floor Function/Examples/Floor of 5

:$\floor 5 = 5$

Proof:
We have that $5$ is an integer.
Thus this is a specific example of Real Number is Integer iff equals Floor:
$\floor x = x \iff x \in \Z$
{{qed}}
Theorem: Force Field is Conservative iff Potential Energy Exists

Let $\map {\mathbf F} {\mathbf r}$ be a force field.
Then a potential energy function $\map P {\mathbf r}$ exists for $\map {\mathbf F} {\mathbf r}$ {{Iff}} $\map {\mathbf F} {\mathbf r}$ is conservative.

Proof:
=== Sufficient Case ===
We have that a potential energy function $\map P {\mathbf r}$ exists (not necessarily unique).
From the definition of potential energy:
:$\ds \map P {\mathbf r_2} - \map P {\mathbf r_1} = \int_{\mathbf r_1}^{\mathbf r_2} \map {\mathbf F} {\mathbf r} \cdot \rd \mathbf l$
Because $\map P {\mathbf r}$ is single valued, the {{LHS}} only depends on the endpoints $\mathbf r_1$ and $\mathbf r_2$.
Thus, the line integral on the {{RHS}} can only depend on the endpoints and not on the path taken.
Therefore, $\map {\mathbf F} {\mathbf r}$ is a conservative vector field by Definition 3.
{{qed|lemma}}
Theorem: Angular Speed of Rotation of Earth

The angular speed $\omega$ of rotation of Earth is approximately:
:$7.29 \times 10^{-5} \, \mathrm {rad \, s}^{-1}$

Proof:
{{tidy|minor stuff}}
By definition of angular speed,
:$\omega = \frac{\theta}{t}$
where $\theta$ is the angle traversed in time $t$.
In one complete rotation of Earth, the angle traversed is
:$2\pi \,\mathrm{rad}$
Also, the time required for one such rotation relative to the fixed stars is approximately one sidereal day, namely
:$86164 \,\mathrm{s}$
Substituting into the definition of angular speed,
:$\omega = \frac{2\pi}{86164}\,\mathrm{rad\,s^{-1}}$
Evaluating,
:$\frac{2\pi}{86164} \approx 7.2921 \times 10^{-5}$
Hence
:$\omega \approx 7.29 \times 10^{-5}\,\mathrm{rad\,s^{-1}}$
{{qed}}
Theorem: Euler-Maclaurin Summation Formula/Formulation 1

{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \map f k
      | r = \int_0^n \map f x \rd x + \sum_{k \mathop = 1}^\infty \frac {B_k} {k!} \paren {\map {f^{\paren {k - 1} } } n - \paren {-1}^k \map {f^{\paren {k - 1} } } 0}
      | c = 
}}
{{eqn | r = \int_0^n \map f x \rd x
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \frac 1 2 \paren {\map f n + \map f 0}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \frac 1 {12} \paren {\map {f'} n - \map {f'} 0}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \frac 1 {720} \paren {\map {f' ' '} n - \map {f' ' '} 0}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \frac 1 {30 \, 240} \paren {\map {f^{\paren 5} } n - \map {f^{\paren 5} } 0}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \frac 1 {1 \, 209 \, 600} \paren {\map {f^{\paren 7} } n - \map {f^{\paren 7} } 0} + \cdots
      | c = 
}}
{{end-eqn}}
where:
:$f^{\paren k}$ denotes the $k$th derivative of $f$
:$B_n$ denotes the $n$th Bernoulli number.

Proof:
{{ProofWanted|I'll let someone do this who's better at this than me}}
Theorem: Characterization of Adjunction Using Unit of Adjunction

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 exists a natural transformation $\eta: \operatorname {id}_{\mathbf D} \to GF$ such that:
::for each object $D$ in $\mathbf D$ the morphism $\eta_D$ is a universal morphism from object $FD$ to functor $G$
Moreover:
:$\forall D \in \mathbf D: \map {\alpha_{\tuple{D, FD}}} {\operatorname{id}_{FD}} = \eta_D$
and:
:$\forall g:FD \to C \in \mathbf C: \map {\alpha_{\tuple{D, C}}} g = Gg \circ \eta_D$

Proof:
=== Necessary Condition ===
Let $\tuple{F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
From Adjunction Induces Unit of Adjunction:
:the unit of adjunction $\eta$ is a natural transformation $\eta: \operatorname {id}_{\mathbf D} \to GF$ such that:
::for each object $D$ of $\mathbf D: \eta_{_D} = \map {\alpha_{\tuple{D, F D}}} {\operatorname {id}_{FD}}$
From Morphism of Unit of Adjunction is Universal:
:for each object $D$ in $\mathbf D$ the morphism $\eta_D$ is a universal morphism from object $FD$ to functor $G$
From Characterization of Adjunction Using Right Adjuncts of Morphisms:
:$\forall g:FD \to C \in \mathbf C: \map {\alpha_{\tuple{D, C}}} g = Gg \circ \eta_D$
{{qed|lemma}}