avewright/proofwiki-math huggingface dataset:
Theorem: Probability Mass Function of Negative Binomial Distribution (Type 1)/Also defined as

Let $X$ be a discrete random variable on a probability space $\struct {\Omega, \Sigma, \Pr}$.
Let $X$ have the '''type $1$ negative binomial distribution with parameters $r$ and $p$''', defined as number of number of Bernoulli trials before the $r$th failure has occurred.
Then the probability mass function of $X$ is given by:
:$\map \Pr {X = k} = \dbinom {k + r - 1} {r - 1} p^r \paren {1 - p}^k$
where:
:$\Img X = \set {0, 1, 2, \ldots}$
:$0 < p < 1$.
Then the probability mass function of $X$ is given by:
:$\map \Pr {X = k} = \dbinom {k - 1} {r - 1} p^{k - r} \paren {1 - p}^r$
where:
:$0 < p < 1$
:$\Img X = \set {r, r + 1, r + 2, \dotsc}$

Proof:
{{Recall|Negative Binomial Distribution (Type 1)|subdef = Also defined as}}
{{:Definition:Negative Binomial Distribution (Type 1)/Also defined as}}
First note that the number of Bernoulli trials has to be at least $r$, so the image is correct: $\Img X = \set {r, r + 1, r + 2, \ldots}$.
Now, note that if $X$ takes the value $k$, then in the first $k - 1$ trials there must have been $r - 1$ failures.
Hence there must have been $k - r$ successes, and so a failure happens at trial number $k$.
So the probability of the occurrence of the event $\sqbrk {X = k}$ is given by the binomial distribution, as follows:
:$\map {p_X} k = \dbinom {k - 1} {r - 1} p^{k - r} \paren {1 - p}^r$
where $k \in \set {r, r + 1, r + 2, \ldots}$
Hence the result, by definition of probability mass function.
{{qed}}
Theorem: Equivalence of Definitions of Frame Isomorphism/Definition 1 Implies Definition 2

Let $L_1$ and $L_2$ be frames.
Let $\phi : L_1 \to L_2$ be a bijective frame homomorphism.
Then:
:$\phi : L_1 \to L_2$ is an order isomorphism.

Proof:
From Frame Homomorphism is Lattice Homomorphism:
:$\phi : L_1 \to L_2$ is a bijective lattice homomorphism
By definition of lattice isomorphism:
:$\phi : L_1 \to L_2$ is a lattice isomorphism
From Inverse of Lattice Isomorphism is Lattice Isomorphism:
:$\phi^{-1} : L_2 \to L_1$ is a lattice isomorphism
By definition of lattice isomorphism:
:$\phi^{-1} : L_2 \to L_1$ is a bijective lattice homomorphism
From Lattice Homomorphism is Order-Preserving:
:$\phi : L_1 \to L_2$ and $\phi^{-1} : L_2 \to L_1$ are order-preserving bijections
Hence $\phi : L_1 \to L_2$ is an order isomorphism by definition.
Theorem: Expectation of Negative Binomial Distribution (Type 2)/Also defined as

Let $X$ be a discrete random variable with the type $2$ negative binomial distribution with parameters $r$ and $p$.
Let $X$ use the definition as the number of failures before $r$ successes have occurred.
Then the expectation of $X$ is given by:
:$\expect X = \dfrac {r q} p$
where $q = 1 - p$.

Proof:
Let $Y$ be a discrete random variable with the type $2$ negative binomial distribution with parameters $r$ and $p$.
Let $Y$ use the definition as the number of successes before $r$ failures have occurred.
From Expectation of Negative Binomial Distribution (Type 2):
:$\expect X = \dfrac {r p} q$
By definition:
:$p$ is the probability of success.
:$q$ is the probability of failure.
Hence the result by exchanging $q$ and $p$.
{{qed}}
Theorem: Equivalence of Definitions of Frame Isomorphism/Definition 4 Implies Definition 1

Let $L_1 = \struct {S_1, \preceq_1}$ and $L_2 = \struct {S_2, \preceq_2}$ be frames.
Let $\phi : L_1 \to L_2$ be a complete lattice isomorphism.
Then:
:$\phi$ is a bijective frame homomorphism

Proof:
By definition of complete lattice isomorphism:
:$\phi : L_1 \to L_2$ is a bijective complete lattice homomorphism.
From Complete Lattice Homomorphism is Frame Homomorphism:
:$\phi : L_1 \to L_2$ is a bijective frame homomorphism.
Theorem: Continued Fraction for Exponential Function

:$e^x = \cfrac 1 {1 - \cfrac x {1 + x - \cfrac x {2 + x - \cfrac {2 x} {3 + x - \cfrac {3 x} {4 + x - \cfrac \ddots \ddots} } } } }$

Proof:
{{begin-eqn}}
{{eqn | l = e^x
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n } {n!}
      | c = Power Series Expansion for Exponential Function
}}
{{eqn | r = 1 + x + \frac {x^2} {2!} + \frac {x^3} {3!} + \frac {x^4} {4!} + \cdots
      | c = 
}}
{{eqn | r = 1 + \paren 1 \paren x + \paren 1 \paren x \paren {\dfrac x 2} + \paren 1 \paren x \paren {\dfrac x 2} \paren {\dfrac x 3} + \paren 1 \paren x \paren {\dfrac x 2} \paren {\dfrac x 3} \paren {\dfrac x 4} + \cdots
      | c = 
}}
{{eqn | r = a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + a_0 a_1 a_2 a_3 a_4 + \cdots
      | c =
}}
{{end-eqn}}
From Euler's Continued Fraction Formula, we have:
:$a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots = \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} } } }$
Therefore:
{{begin-eqn}}
{{eqn | l = 1 + \paren 1 \paren x + \paren 1 \paren x \paren {\dfrac x 2} + \paren 1 \paren x \paren {\dfrac x 2} \paren {\dfrac x 3} + \paren 1 \paren x \paren {\dfrac x 2} \paren {\dfrac x 3} \paren {\dfrac x 4} + \cdots
      | r = \cfrac 1 {1 - \cfrac {\paren x } {1 + \paren x - \cfrac {\paren {\dfrac x 2} } {1 + \paren {\dfrac x 2} - \cfrac {\paren {\dfrac x 3} } {1 + \paren {\dfrac x 3} - \cfrac {\paren {\dfrac x 4} } {1 + \paren {\dfrac x 4} - \cfrac \ddots \ddots} } } } }
      | c = 
}}
{{eqn | r = \cfrac 1 {1 - \cfrac {\paren x} {\paren {1 + \paren x} - \cfrac {\paren {\dfrac x 2} \times 2} {2 \times \paren {1 + \paren {\dfrac x 2} } - \cfrac {\paren {\dfrac x 3} \times 2 \times 3} {3 \times \paren {1 + \paren {\dfrac x 3} } - \cfrac {\paren {\dfrac x 4} \times 3 \times 4 } {4 \times \paren {1 + \paren {\dfrac x 4} } - \cfrac \ddots \ddots} } } } }
      | c = multiplying by $1$
}}
{{eqn | r = \cfrac 1 {1 - \cfrac x {1 + x - \cfrac x {2 + x - \cfrac {2 x } {3 + x - \cfrac {3 x} {4 + x - \cfrac \ddots \ddots} } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: One Represented With Infinite Twos

{{begin-eqn}}
{{eqn | l = 1
      | r = \cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } + \cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } + \cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } + \cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } + \cfrac 2 {\cfrac 2 {\ddots + \ddots} + \cfrac 2 {\ddots + \ddots} } } } }
      | c = 
}}
{{end-eqn}}
where the bottom row contains $2^n$ ones and the pyramid above it contains $\paren{2^n - 1}$ twos.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 1
      | r = \cfrac 2 {1 + 1}
      | c = One Layer Deep: $2^1$ ones and $\paren{2^1 - 1}$ twos
}}
{{eqn | r = \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} }
      | c = Two Layers Deep: $2^2$ ones and $\paren{2^2 - 1}$ twos
}}
{{eqn | r = \cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } }
      | c = Three Layers Deep: $2^3$ ones and $\paren{2^3 - 1}$ twos
}}
{{eqn | r = \cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } } }
      | c = Four Layers Deep: $2^4$ ones and $\paren{2^4 - 1}$ twos
}}
{{eqn | r = \cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } } + \cfrac 2 {\cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } + \cfrac 2 {\cfrac 2 {1 + 1} + \cfrac 2 {1 + 1} } } } }
      | c = Five Layers Deep: $2^5$ ones and $\paren{2^5 - 1}$ twos
}}
{{eqn | r = \cdots
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Continued Fractions
Category:Number Theory
Category:Recreational Mathematics
rf84fk30ynbgc69q55gl0937ej87zfr
Theorem: Continued Fraction for Logarithm of 1 + x

:$\map \ln {1 + x} = \cfrac x {1 + \cfrac x {2 - x + \cfrac {2^2 x} {3 - 2 x + \cfrac {3^2 x} {4 - 3 x + \cfrac {\ddots} {\ddots} } } } }$

Proof:
{{begin-eqn}}
{{eqn | l = \map \ln {1 + x}
      | r = \sum_{n \mathop = 1}^\infty \paren {-1}^{n - 1} \frac {x^n} n
      | c = Power Series Expansion for Logarithm of 1 + x
}}
{{eqn | r = x - \frac {x^2} 2 + \frac {x^3} 3 - \frac {x^4} 4 + \cdots
      | c = 
}}
{{eqn | r = \paren x + \paren x \paren {-\dfrac x 2} + \paren x \paren {-\dfrac x 2} \paren {-\dfrac {2 x} 3} + \paren x \paren {-\dfrac x 2} \paren {-\dfrac {2 x} 3} \paren {-\dfrac {3 x} 4} + \cdots
      | c = 
}}
{{eqn | r = a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots
      | c =
}}
{{end-eqn}}
From Euler's Continued Fraction Formula, we have:
:$a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots = \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} } } }$
Therefore:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren x + \paren x \paren {-\dfrac x 2} + \paren x \paren {-\dfrac x 2} \paren {-\dfrac {2 x} 3} + \paren x \paren {-\dfrac x 2} \paren {-\dfrac {2 x} 3} \paren {-\dfrac {3 x} 4} + \cdots
      | c = 
}}
{{eqn | r = \cfrac x {1 - \cfrac {\paren {-\dfrac x 2} } {1 + \paren {-\dfrac x 2} - \cfrac {\paren {-\dfrac {2 x} 3} } {1 + \paren {-\dfrac {2 x} 3} - \cfrac {\paren {-\dfrac {3 x} 4} } {1 + \paren {-\dfrac {3 x} 4} - \cfrac {\ddots} {\ddots} } } } }
      | c = 
}}
{{eqn | r = \cfrac x {1 - \cfrac {\paren {-\dfrac x 2} \times 2} {2 \times \paren {1 + \paren {-\dfrac x 2} } - \cfrac {\paren {-\dfrac {2 x} 3} \times 2 \times 3 } {3 \times \paren {1 + \paren {-\dfrac {2 x} 3} } - \cfrac {\paren {-\dfrac {3 x} 4} \times 3 \times 4 } {4 \times \paren {1 + \paren {-\dfrac {3 x} 4} } - \cfrac {\ddots} {\ddots} } } } }
      | c =multiplying top and bottom of $n$th line by $n$
}}
{{eqn | r = \cfrac x {1 + \cfrac x {2 - x + \cfrac {2^2 x} {3 - 2 x + \cfrac {3^2 x} {4 - 3 x + \cfrac {\ddots} {\ddots} } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Continued Fraction for Real Arcsine Function

:$\arcsin x = \cfrac x {1 - \cfrac {x^2} {2 \times 3 + x^2 - \cfrac {2 \times 3 \times \paren {3 x}^2} {4 \times 5 + \paren {3 x}^2 - \cfrac {4 \times 5 \times \paren {5 x}^2} {6 \times 7 + \paren {5 x}^2 - \cfrac {6 \times 7 \times \paren {7 x}^2} {\ddots } } } } }$

Proof:
{{begin-eqn}}
{{eqn | l = \arcsin x
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
      | c = Power Series Expansion for Real Arcsine Function for $-1 \le x \le 1$
}}
{{eqn | r = x + \frac {x^3} {2 \times 3} + \frac {\paren {1 \times 3} x^5} {2 \times 4 \times 5} + \frac {\paren {1 \times 3 \times 5} x^7} {2 \times 4 \times 6 \times 7} + \cdots
      | c = 
}}
{{eqn | r = x + x \paren {\dfrac {x^2} {2 \times 3} } + x \paren {\dfrac {x^2} {2 \times 3} } \paren {\dfrac {\paren {3 x}^2} {4 \times 5} } + x \paren {\dfrac {x^2} {2 \times 3} } \paren {\dfrac {\paren {3 x}^2} {4 \times 5} } \paren {\dfrac {\paren {5 x}^2} {6 \times 7} } + \cdots
      | c = 
}}
{{eqn | r = a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots
      | c =
}}
{{end-eqn}}
From Euler's Continued Fraction Formula, we have:
:$a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots = \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  } } } } }$
Therefore:
{{begin-eqn}}
{{eqn | l = x + x \paren {\dfrac {x^2} {2 \times 3} } + x \paren {\dfrac {x^2} {2 \times 3} } \paren {\dfrac {\paren {3 x}^2} {4 \times 5} } + x \paren {\dfrac {x^2} {2 \times 3} } \paren {\dfrac {\paren {3 x}^2} {4 \times 5} } \paren {\dfrac {\paren {5 x}^2} {6 \times 7} } + \cdots
      | r = \cfrac x {1 - \cfrac {\paren {\dfrac {x^2} {2 \times 3} } } {1 + \paren {\dfrac {x^2} {2 \times 3} } - \cfrac {\paren {\dfrac {\paren {3 x}^2} {4 \times 5} } } {1 + \paren {\dfrac {\paren {3 x}^2} {4 \times 5} } - \cfrac {\paren {\dfrac {\paren {5 x}^2} {6 \times 7} } } {1 + \paren {\dfrac {\paren {5 x}^2} {6 \times 7} } - \cfrac {\ddots} {\ddots  } } } } }
      | c = 
}}
{{eqn | r = \cfrac x {1 - \cfrac {\paren {\dfrac {x^2} {2 \times 3} } \times 2 \times 3 } {2 \times 3 \times \paren {1 + \paren {\dfrac {x^2} {2 \times 3} } } - \cfrac {\paren {\dfrac {\paren {3 x}^2} {4 \times 5} } \times 2 \times 3 \times 4 \times 5 } {4 \times 5 \times \paren {1 + \paren {\dfrac {\paren {3 x}^2} {4 \times 5} } } - \cfrac {\paren {\dfrac {\paren {5 x}^2} {6 \times 7} } \times 4 \times 5 \times 6 \times 7 } {6 \times 7 \times \paren {1 + \paren {\dfrac {\paren {5 x}^2} {6 \times 7} } } - \cfrac {\ddots} {\ddots  } } } } }
      | c = multiplying by $1$
}}
{{eqn | r = \cfrac x {1 - \cfrac {x^2} {2 \times 3 + x^2 - \cfrac {2 \times 3 \times \paren {3 x}^2} {4 \times 5 + \paren {3 x}^2 - \cfrac {4 \times 5 \times \paren {5 x}^2} {6 \times 7 + \paren {5 x}^2 - \cfrac {6 \times 7 \times \paren {7 x}^2} {\ddots } } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse of Bijective Complete Lattice Homomorphism is Bijective Complete Lattice Homomorphism

Let $L_1 = \struct {A_1, \preceq_1}$ and $L_2 = \struct {A_2, \preceq_2}$ be complete lattices.
Let $\phi: L_1 \to L_2$ be a bijective complete lattice homomorphism.
Let $\phi^{-1} : A_2 \to A_1$ be the inverse of $\phi : A_1 \to A_2$.
Then:
:$\phi^{-1} : L_2 \to L_1$ is a bijective complete lattice homomorphism.

Proof:
From Inverse of Bijection is Bijection:
:$\phi^{-1}$ is a bijection
It remains to show that $\phi^{-1}$ is a complete lattice homomorphism.
Theorem: Converse of Fermat's Little Theorem does not hold

Let $n$ be a natural number.
Let:
:$n \divides a^n - a$
where:
:$a$ is a natural number such that $n$ is not a divisor of $a$.
:$\divides$ denotes divisibility.
Then it is not necessarily the case that $n$ is prime

Proof:
;Proof by Counterexample
We have that:
:$2^{341} \equiv 2 \pmod {341}$
despite the fact that $341$ is not prime:
:$341 = 11 \times 31$
{{qed}}
Theorem: Category DLat is Full Subcategory of Lat

Let $\mathbf {DLat}$ denote the category of distributive lattices.
Let $\mathbf {Lat}$ denote the category of lattices.
Then:
:$\mathbf {DLat}$ is a full subcategory of $\mathbf {Lat}$

Proof:
By definition of distributive lattice:
:a distributive lattice is a lattice
Hence the objects of $\mathbf {DLat}$ is a collection of objects of $\mathbf {Lat}$
By definition of category of distributive lattices:
:every morphism of $\mathbf {DLat}$ is a morphism of $\mathbf {Lat}$
Hence the morphisms of $\mathbf {DLat}$ is a collection of morphisms of $\mathbf {Lat}$
Composition in $\mathbf {DLat}$ and $\mathbf {Lat}$ is standard composition of mappings in both categories.
Hence composition in $\mathbf {DLat}$ is inherited from $\mathbf {Lat}$.
Identity morphisms in $\mathbf {DLat}$ and $\mathbf {Lat}$ are the identity mappings in both categories.
Hence identity morphisms in $\mathbf {DLat}$ are inherited from $\mathbf {Lat}$.
It follows that $\mathbf {DLat}$ is a subcategory of $\mathbf {Lat}$ by definition.
For every pair of objects $D_1$ and $D_2$ of $\mathbf {DLat}$:
:every morphism $f : D_1 \to D_2$ of $\mathbf {Lat}$ is a morphism of $\mathbf {DLat}$
by definition of category of distributive lattices.
Hence $\mathbf {DLat}$ is a full subcategory of $\mathbf {Lat}$ by definition.
{{qed}}
Category:Category of Distributive Lattices
kte3ghur3osi4szkssmbyo1r11qz2d9
Theorem: Category of Distributive Lattices is Category

Let $\mathbf {DLat}$ denote the category of distributive lattices.
Then:
:$\mathbf {DLat}$ is a metacategory

Proof:
From Category DLat is Full Subcategory of Lat:
:$\mathbf {DLat}$ is a full subcategory of the category of lattices
By definition of subcategory:
:$\mathbf {DLat}$ is a metacategory
{{qed}}
Category:Category of Distributive Lattices
h6ioghc0zqpd1un1b97ltg2f80zeicz
Theorem: Tangent of Three Right Angles minus Angle

:$\map \tan {x - \dfrac {3 \pi} 2} = \cot x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {x - \frac {3 \pi} 2}
      | r = \frac {\map \sin {x - \frac {3 \pi} 2} } {\map \cos {x - \frac {3 \pi} 2} } 
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {-\cos x} {-\sin x}
      | c = Sine of Angle minus Three Right Angles and Cosine of Angle minus Three Right Angles
}}
{{eqn | r = \cot x
      | c = Cotangent is Cosine divided by Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Empty Mapping is Surjective iff Codomain is Empty

Let $T$ be a set.
Let $\O$ denote the empty set.
Let $e: \O \to T$ be the empty mapping.
Then $e$ is a surjection {{iff}} $T = \O$.

Proof:
Let $T = \O$.
From Empty Mapping to Empty Set is Bijective, $e$ is a bijection.
Hence {{afortiori}} $e$ is a surjection.
{{qed|lemma}}
Let $T \ne \O$.
{{AimForCont}} $e$ is a surjection.
Let $t \in T$.
As $e$ is a surjection:
:$(1): \quad \exists s \in S: \map e s = t$
But by Null Relation is Mapping iff Domain is Empty Set:
:$\Dom e = \O$
Hence:
:$\nexists s \in S: \map e s = t$
This is a contradiction of $(1)$.
Hence by Proof by Contradiction it is not possible for $e$ to be a surjection.
Hence if $e$ is a surjection it must be the case that $T = \O$.
{{qed|lemma}}
So we have:
:$T = \O$ implies that $e$ is a surjection
:$e$ is a surjection implies that $T = \O$
and the result follows.
{{qed}}
Category:Empty Mapping
Category:Surjections
evtkf3zlet7t50x679am02exot5mr8h
Theorem: Classification of Stationary Points/Function of Two Variables

Let $\SS$ be a surface defined by the Cartesian equation $z = \map f {x, y}$.
Let $P$ be a stationary point on $\SS$.
Then $P$ is either:
:a local maximum
:a local minimum
:a saddle point.

Proof:
{{ProofWanted|one direction immediate, the other not so much}}
Theorem: Hyperbolic Sine Function in terms of Hypergeometric Function

:$\sinh x = x \paren {\map { {}_0 \operatorname F_1} {\dfrac 3 2; \dfrac {x^2} 4} }$

Proof:
{{begin-eqn}}
{{eqn | l = x \paren {\map { {}_0 \operatorname F_1} {\frac 3 2; \dfrac {x^2} 4} }
      | r = x \sum_{n \mathop = 0}^\infty \frac 1 {\paren {\frac 3 2}^{\bar n} } \frac {\paren {\frac {x^2} 4 }^n} {n!}
      | c = {{Defof|Generalized Hypergeometric Function}}
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 3 2} } {\map \Gamma {\frac 3 2 + n} } \frac {\paren {\frac {x^2} 4 }^n} {\map \Gamma {n + 1} }
      | c = Rising Factorial as Quotient of Factorials, Gamma Function Extends Factorial
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\frac 1 2 \map \Gamma {\frac 1 2} } {\map \Gamma {n + 1 + \frac 1 2} } \frac {x^{2 n} } {2^{2 n} \map \Gamma {n + 1} }
      | c = Gamma Difference Equation, Power of Power
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + 1 + \frac 1 2} } \frac {x^{2 n} } {2^{2 n + 1} \map \Gamma {n + 1} }
      | c = 
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + 1 + \frac 1 2} } \frac {x^{2 n} } {2^{2 \paren {n + 1} - 1} \map \Gamma {n + 1} }
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {x^{2 n + 1} } {\map \Gamma {2 \paren {n + 1} } }
      | c = Legendre's Duplication Formula
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \sinh x
      | c = Power Series Expansion for Hyperbolic Sine Function
}}
{{end-eqn}}
{{qed}}
Theorem: Area under Acceleration-Time Graph

Let $P$ be a particle moving in a straight line.
Let the acceleration of $P$ as a function of time be $\map a t$.
Let the velocity of $P$ as a function of time be $\map v t$.
Let the motion of $P$ be plotted on an acceleration-time-graph $G$.
Let $v_1$ and $v_2$ be the velocities of $P$ at times $t_1$ and $t_2$ respectively.
Then the area under $G$ between times $t_1$ and $t_2$ is equal to $v_2 - v_1$.

Proof:
Let $A$ be the area under $G$ between times $t_1$ and $t_2$.
Then
{{begin-eqn}}
{{eqn | l = A
      | r = \int_{t_1}^{t_2} \map a t \rd t
      | c = Area under Curve
}}
{{eqn | r = \int_{t_1}^{t_2} \map {\dfrac {\d v} {\d t} } t \rd t
      | c = {{Defof|Acceleration}}
}}
{{eqn | r = \map v {t_2} - \map v {t_1}
      | c = Fundamental Theorem of Calculus
}}
{{eqn | r = v_2 - v_1
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cosine Function in terms of Hypergeometric Function

:$\cosh x = \map { {}_0 \operatorname F_1} {\dfrac 1 2; \dfrac {x^2} 4}$

Proof:
{{begin-eqn}}
{{eqn | l = \map { {}_0 \operatorname F_1} {\frac 1 2; \dfrac {x^2} 4}
      | r = \sum_{n \mathop = 0}^\infty \frac 1 {\paren {\frac 1 2}^{\bar n} } \frac {\paren {\frac {x^2} 4 }^n} {n!}
      | c = {{Defof|Generalized Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {\frac 1 2 + n} } \frac {\paren {\frac {x^2} 4 }^n} {\map \Gamma {n + 1} }
      | c = Rising Factorial as Quotient of Factorials, Gamma Function Extends Factorial
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + \frac 1 2} } \frac {x^{2 n} } {2^{2 n} \map \Gamma {n + 1} }
      | c = Gamma Difference Equation, Power of Power
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + \frac 1 2} } \frac {x^{2 n} } {2^{2 n - 1} \paren {2 n} \map \Gamma n }
      | c = Gamma Difference Equation
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {x^{2 n} } {\map \Gamma {2 n } \paren {2 n} }
      | c = Legendre's Duplication Formula
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {x^{2 n} } {\paren {2 n}!}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \cosh x
      | c = Power Series Expansion for Hyperbolic Cosine Function
}}
{{end-eqn}}
{{qed}}
Theorem: Continued Fraction for Real Hyperbolic Tangent Function

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

Proof:
{{begin-eqn}}
{{eqn | l = \tanh x
      | r = \dfrac {\sinh x} {\cosh x}
      | c = {{Defof|Hyperbolic Tangent}}
}}
{{eqn | r = \frac {x \map { {}_0 \operatorname F_1} {\dfrac 3 2; \dfrac {x^2} 4} } {\map { {}_0 \operatorname F_1} {\dfrac 1 2; \dfrac {x^2} 4} }
      | c = Hyperbolic Sine Function in terms of Hypergeometric Function, Hyperbolic Cosine Function in terms of Hypergeometric Function
}}
{{eqn | r = \frac {x \map { {}_0 \operatorname F_1} {\dfrac 1 2 + 1; \dfrac {x^2} 4} } {\map { {}_0 \operatorname F_1} {\dfrac 1 2; \dfrac {x^2} 4} }
      | c = 
}}
{{end-eqn}}
From Hypergeometric Continued Fraction Formulation 1, we have:
:$\dfrac {\map { {}_0 \operatorname F_1} {a + 1; x} } {\map { {}_0 \operatorname F_1} {a; x} } = \cfrac a {a + \cfrac x {\paren {a + 1} + \cfrac x {\paren {a + 2} + \cfrac x {\paren {a + 3} + \cfrac x {\ddots + \cfrac \ddots \ddots} } } } }$
Therefore:
{{begin-eqn}}
{{eqn | l = \tanh x
      | r = \cfrac {\dfrac x 2} {\dfrac 1 2 + \cfrac {\dfrac {x^2} 4} {\paren {\dfrac 1 2 + 1} + \cfrac {\dfrac {x^2} 4} {\paren {\dfrac 1 2 + 2} + \cfrac {\dfrac {x^2} 4} {\paren {\dfrac 1 2 + 3} + \cfrac {\dfrac {x^2} 4} {\ddots + \cfrac \ddots \ddots} } } } }
      | c = $a = \dfrac 1 2$
}}
{{eqn | r = \cfrac {\dfrac x 2 \times 2} {2 \times \dfrac 1 2 + \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {2 \times \paren {\dfrac 3 2} + \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {2 \times \paren {\dfrac 5 2} + \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {2 \times \paren {\dfrac 7 2} + \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {\ddots + \cfrac \ddots \ddots} } } } }
      | c = multiplying top and bottom by $2$ throughout
}}
{{eqn | r = \cfrac x {1 + \cfrac {x^2} {3 + \cfrac {x^2} {5 + \cfrac {x^2} {7 + \cfrac {x^2} {9 + \cfrac {x^2} \ddots} } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}