avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Exponential of a x by Hyperbolic Cosine of b x/Hyperbolic Form

:$\ds \int e^{a x} \cosh b x \rd x = \frac {e^{a x} \paren {a \cosh b x + b \sinh b x} } {a^2 - b^2} + C$
for $a^2 \ne b^2$.

Proof:
{{begin-eqn}}
{{eqn | l = \int e^{a x} \cosh b x \rd x
      | r = \frac {e^{a x} } 2 \paren {\frac {e^{b x} } {a + b} + \frac {e^{-b x} } {a - b} } + C
      | c = Primitive of $e^{a x} \cosh b x$: Exponential Form
}}
{{eqn | r = \frac {e^{a x} } 2 \paren {\frac {e^{b x} \paren {a - b} } {\paren {a + b} \paren {a - b} } + \frac {e^{-b x} \paren {a + b} } {\paren {a - b} \paren {a + b} } } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } 2 \paren {\frac {e^{b x} \paren {a - b} + e^{-b x} \paren {a + b} } {\paren {a + b} \paren {a - b} } } + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } 2 \paren {\frac {e^{b x} \paren {a - b} + e^{-b x} \paren {a + b} } {\paren {a^2 - b^2} } } + C
      | c = Difference of Two Squares
}}
{{eqn | r = \frac {e^{a x} } {a^2 - b^2} \paren {\frac {a e^{b x} - b e^{b x} + a e^{-b x} + b e^{-b x} } 2} + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {a^2 - b^2} \paren {a \frac {e^{b x} + e^{-b x} } 2 + b \frac {e^{b x} - e^{-b x} } 2} + C
      | c = 
}}
{{eqn | r = \frac {e^{a x} } {a^2 - b^2} \paren {a \frac {e^b x + e^{-b} x} 2 + b \sinh b x} + C
      | c = {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \frac {e^{a x} } {a^2 - b^2} \paren {a \cosh b x + b \sinh b x } + C
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac {e^{a x} \paren {a \cosh b x + b \sinh b x} } {a^2 - b^2} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral of Exponential of minus a x squared from 0 to Infinity

:$\ds \int_0^\infty \map \exp {-a x^2} \rd x = \dfrac 1 2 \sqrt {\dfrac \pi a}$
for $a > 0$.

Proof:
Recall Integral to Infinity of $\map \exp {-x^2}$:
:$\ds \int_0^\infty \map \exp {-x^2} \rd x = \dfrac {\sqrt \pi} 2$
Then:
{{begin-eqn}}
{{eqn | l = \int \map \exp {-a x^2} \rd x
      | r = \int \map \exp {-\paren {\sqrt a x}^2} \rd x
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt a} \int \map \exp {-\paren {\sqrt a x}^2} \rd \paren {\sqrt a x}
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | ll= \leadsto
      | l = \int_0^\infty \map \exp {-a x^2} \rd x
      | r = \dfrac 1 {\sqrt a} \int_0^\infty \map \exp {-\paren {\sqrt a x}^2} \rd \paren {\sqrt a x}
      | c = as the limits of integration stay the same
}}
{{eqn | r = \dfrac 1 {\sqrt a} \dfrac {\sqrt \pi} 2
      | c = 
}}
{{eqn | r = \dfrac 1 2 \sqrt {\dfrac \pi a}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Euler Characteristic is not Dependent upon Subdivision

Let $S$ be a surface.
Let $T_1$ and $T_2$ be subdivisions of $S$.
Let:
:$\map {\chi_1} S$ be the Euler characteristic of $S$ as calculated using $T_1$
:$\map {\chi_2} S$ be the Euler characteristic of $S$ as calculated using $T_2$.
Then:
:$\map {\chi_1} S = \map {\chi_2} S$

Proof:
Recall:
{{begin-eqn}}
{{eqn | l = \map {\chi_1} S
      | r = \map {\chi_2} S
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \map v {T_1} - \map e {T_1} + \map f {T_1}
      | r = \map v {T_2} - \map e {T_2} + \map f {T_2}
      | c = {{Defof|Euler Characteristic of Surface}}
}}
{{end-eqn}}
where:
:$\map v {T_1}$ denotes the order of $T_1$ (that is, the number of its vertices)
:$\map e {T_1}$ denotes the size of $T_1$ (that is, the number of its edges)
:$\map f {T_1}$ denotes the number of faces of $T_1$.
{{ProofWanted|Probably do it by induction on number of faces, once we have a rigorous definition of triangulation, and have the basics of the theory down.}}
Theorem: Relative Pseudocomplement Preserves Order

Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice.
Let $a, b, c \in S$.
Let $b \preceq c$.
Then
:$a \to b \preceq a \to c$
where $x \to y$ denotes the relative pseudocomplement of $x$ with respect to $y$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = a \to b
      | r = \max \set {a \wedge x : x \in S : a \wedge x \preceq b}
      | c = {{Defof|Relative Pseudocomplement}}
}}
{{eqn | o = \preceq
      | r = \max \set {a \wedge x : x \in S : a \wedge x \preceq c}
      | c = Finer Supremum Precedes Supremum
}}
{{eqn | r = a \to c
      | c = {{Defof|Relative Pseudocomplement}}
}}
{{end-eqn}}
{{qed}}
Category:Brouwerian Lattices
7bkjrwv3xlqh7b7px5ldwrd607m4w52
Theorem: Eulerian Graph is Semi-Eulerian

Let $G$ be an Eulerian graph.
Then $G$ is also a semi-Eulerian graph.

Proof:
Recall the definition of Eulerian graph:
{{:Definition:Eulerian Graph}}
Recall the definition of semi-Eulerian graph:
{{:Definition:Semi-Eulerian Graph}}
So, let $G$ be an Eulerian graph.
Let $C$ be an Eulerian circuit for $G$.
From Eulerian Circuit is Eulerian Trail, $C$ is also an Eulerian trail for $G$. 
Thus $G$ has an Eulerian trail.
The result follows by definition of semi-Eulerian graph.
{{qed}}
Category:Eulerian Graphs
Category:Semi-Eulerian Graphs
fvfbu4kx63ah4o30pdms9hnaul62t4y
Theorem: Eulerian Circuit is Eulerian Trail

Let $G$ be a graph.
Let $C$ be an Eulerian circuit for $G$.
Then $C$ is also an Eulerian trail for $G$.

Proof:
Recall the definition of Eulerian circuit:
{{:Definition:Eulerian Circuit}}
Recall the definition of Eulerian trail:
{{:Definition:Eulerian Trail}}
Recall the definition of circuit:
{{:Definition:Circuit (Graph Theory)}}
Hence an Eulerian circuit is an instance of an Eulerian trail.
{{qed}}
Category:Eulerian Circuits
Category:Eulerian Trails
caysqajiunomzmc40z5voyfttbhnpt4
Theorem: Euler's Criterion

Let $a$ be a residue order $n$ of $m$, where $a$ and $m$ are coprime.
Then:
:$a^{\map \phi m / d} \equiv 1 \pmod m$
where:
:$\map \phi m$ denotes the Euler $\phi$ function of $m$
:$d$ denotes the gretest common divisor of $\map \phi m$ and $n$
:$\equiv$ denotes modulo congruence.

Proof:
{{ProofWanted}}
{{Namedfor|Leonhard Paul Euler|cat = Euler}}
Theorem: Euler's Criterion

Let $a$ be a residue order $n$ of $m$, where $a$ and $m$ are coprime.
Then:
:$a^{\map \phi m / d} \equiv 1 \pmod m$
where:
:$\map \phi m$ denotes the Euler $\phi$ function of $m$
:$d$ denotes the gretest common divisor of $\map \phi m$ and $n$
:$\equiv$ denotes modulo congruence.

Proof:
Trivially, any $a \not \equiv 0 \pmod p$ is either a quadratic residue or a quadratic non-residue, modulo $p$.
Therefore, it suffices to check the sufficient condition for both of the equations (i.e., the ''if'' parts from the ''iff''s).
So let $a$ be a quadratic non-residue of $p$.
Also, let $b \in \set {1, 2, \ldots, p - 1}$.
The congruence $b x \equiv a \pmod p$ has (modulo $p$) a unique solution $b'$ by Solution of Linear Congruence.
Note that $b' \not\equiv b$, because otherwise we would have $b^2 \equiv a \pmod p$ and $a$ would be a quadratic residue of $p$.
It follows that the residue classes $\set {1, 2, \ldots, p - 1}$ modulo $p$ fall into $\dfrac {p - 1} 2$ pairs $b, b'$ such that $b b' \equiv a \pmod p$.
Therefore, we have:
:$\paren {p - 1}! = 1 \times 2 \times \cdots \times \paren {p - 1} \equiv a \times a \times \cdots \times a \equiv a^{\frac {p - 1} 2} \pmod p$
From Wilson's Theorem, we also have:
:$\paren {p - 1}! \equiv -1 \pmod p$
And so, for any quadratic non-residue of $p$:
:$a^{\frac {p - 1} 2} \equiv -1 \pmod p$
Subsequently, let $a$ be a quadratic residue of $p$.
By definition of a quadratic residue, the congruence $x^2 \equiv a \pmod p$ has a solution $x$.
Suppose also $y$ is a solution. Then we have:
{{begin-eqn}}
{{eqn | l = x^2 - y^2
      | o = \equiv
      | r = 0
      | rr= \pmod p
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x + y} \paren {x - y}
      | o = \equiv
      | r = 0
      | rr= \pmod p
}}
{{end-eqn}}
So either $x + y \equiv 0 \pmod p$ or $x - y \equiv 0 \pmod p$ from Product is Zero Divisor means Zero Divisor.
It follows that when $c \pmod p$ is one solution, $-c \pmod p$ is, too.
Also, these solutions are distinct as $p$ is odd.
Furthermore, we conclude that these are the only two solutions.
Now, remove $c$ and $p - c$ from $\set {1, 2, \ldots, p - 1}$.
The remaining integers fall, modulo $p$, into $\dfrac {p - 3} 2$ pairs $b, b'$ such that $b b' \equiv a \pmod p$ by Solution of Linear Congruence.
Therefore, we can compute the following:
{{begin-eqn}}
{{eqn | l = \paren {p - 1}!
      | r = 1 \times 2 \times \cdots \times c \times \cdots \times \paren {p - c} \times \cdots \times \paren {p - 1}
}}
{{eqn | o = \equiv
      | r = a \times a \times \cdots \times a \times c \times \paren {-c}
      | rr= \pmod p
}}
{{eqn | o = \equiv
      | r = a^{\frac {p - 3} 2} \paren {-c^2}
      | rr= \pmod p
}}
{{eqn | o = \equiv
      | r = a^{\frac {p - 3} 2} \paren {-a}
      | rr= \pmod p
}}
{{eqn | o = \equiv
      | r = -a^{\frac {p - 1} 2}
      | rr= \pmod p
}}
{{end-eqn}}
Again applying Wilson's Theorem, we conclude:
:$-a^{\frac {p-1} 2} \equiv - 1 \pmod p$
The assertion for quadratic residues $a$ of $p$ follows.
{{qed}}
Theorem: Euler's Criterion

Let $a$ be a residue order $n$ of $m$, where $a$ and $m$ are coprime.
Then:
:$a^{\map \phi m / d} \equiv 1 \pmod m$
where:
:$\map \phi m$ denotes the Euler $\phi$ function of $m$
:$d$ denotes the gretest common divisor of $\map \phi m$ and $n$
:$\equiv$ denotes modulo congruence.

Proof:
First note that the square roots of $1$ are $1, -1 \pmod p$.
Also, we have that $a^{p - 1} \equiv 1 \pmod p$ by Fermat's Little Theorem.
Combining these two observations, we find:
:$a^{\frac {p - 1} 2} \equiv 1 \text{ or } -1 \pmod p$
The theorem is therefore equivalent to stating that $a$ is a quadratic residue modulo $p$ {{iff}} $a^{\frac{p - 1} 2} \equiv 1 \pmod p$.
Namely, considering the above, we see this also implies that all quadratic non-residues will be congruent to $-1 \pmod p$.
We prove each direction of the equivalent statement separately:
=== Sufficient Condition ===
Assume $a$ is a quadratic residue modulo $p$.
We pick $k$ such that $k^2 \equiv a \pmod p$.
Then by Congruence of Powers and Fermat's Little Theorem:
:$a^{\frac{p-1} 2} \equiv k^{p-1} \equiv 1 \pmod p$
=== Necessary Condition ===
Now assume $a^{\frac{p - 1} 2} \equiv 1 \pmod p$.
Then let $y$ be a primitive root modulo $p$, so that $a$ can be written as $y^j$.
In particular:
:$y^{j \frac {p - 1} 2} \equiv 1 \pmod p$
From the definition of $y$, it has order $p-1$.
It follows that $p - 1 \divides j \dfrac {p - 1} 2$ from Element to Power of Multiple of Order is Identity.
We conclude that $j$ is necessarily an even integer, and denote $j' = \dfrac j 2$.
Let $k$ be such that $k \equiv y^{j'} \pmod p$.
By construction, we have:
:$k^2 \equiv y^{2 j'} \equiv y^j \equiv a \pmod p$
Hence $a$ is a quadratic residue modulo $p$.
{{qed}}
Theorem: Element Well Inside Itself Iff Has Complement

:$\forall a \in S : a \eqslantless a \iff a$ has a complement

Proof:
Follows immediately from:
:* Definition:Well Inside Relation
:* Definition:Complement (Lattice Theory)
{{qed}}
Theorem: Equivalence of Definitions of Even Permutation

{{TFAE|def = Even Permutation}}
Let $n \in \N$ be a natural number.
Let $S_n$ denote the symmetric group on $n$ letters.
Let $\rho \in S_n$ be a permutation in $S_n$.

Proof:
The '''sign of $\rho$''' is defined as:
:$\map \sgn \rho = \begin {cases} 1 & : \text {$k$ even} \\ -1 & : \text {$k$ odd} \\ \end {cases}$
The result follows.
{{qed}}
Category:Even Permutations
foox8y9d0yzpalw87h0e8vo4fvcpt1s
Theorem: Well Inside Implies Predecessor

:$\forall a,b \in S : a \eqslantless b \implies a \preceq b$

Proof:
Let $a, b \in S : a \eqslantless b$.
By definition of well inside relation:
:$\exists c \in S : a \wedge c = \bot, b \vee c = \top$
We have:
{{begin-eqn}}
{{eqn | l = a 
      | r = a \wedge \top
      | c = Predecessor is Infimum
}}
{{eqn | r = a \wedge \paren{b \vee c}
      | c = By choice of $c$
}}
{{eqn | r = \paren{a \wedge b} \vee \paren{a \wedge c}
      | c = {{Defof|Distributive Lattice}}
}}
{{eqn | r = \paren{a \wedge b} \vee \bot
      | c = By choice of $c$
}}
{{eqn | r = a \wedge b
      | c = Successor is Supremum
}}
{{end-eqn}}
From Predecessor is Infimum:
:$a \preceq b$
The result follows.
{{qed}}
Theorem: Well Inside Relation Extends to Predecessor and Successor

:$\forall a,b,c,d  \in S : a \preceq b \eqslantless c \preceq d \implies a \eqslantless d$

Proof:
Let $a,b,c,d  \in S : a \preceq b \eqslantless c \preceq d$
By definition of well inside relation:
:$\exists x \in S : b \wedge x = \bot, c \vee x = \top$
We have:
{{begin-eqn}}
{{eqn | l = \bot
      | o = \preceq
      | r = a \wedge x
      | c = {{Defof|Smallest Element}}
}}
{{eqn | o = \preceq
      | r = b \wedge x
      | c = Infimum Precedes Coarser Infimum
}}
{{eqn | r = \bot
      | c = By choice of $x$
}}
{{end-eqn}}
From {{Ordering-axiom|1}}:
:$a \wedge x = \bot$
Similarly, we have:
{{begin-eqn}}
{{eqn | l = \top
      | r = c \vee x
      | c = By choice of $x$
}}
{{eqn | o = \preceq
      | r = d \vee x
      | c = Finer Supremum Precedes Supremum
}}
{{eqn | o = \preceq
      | r = \top
      | c = {{Defof|Greatest Element}}
}}
{{end-eqn}}
From {{Ordering-axiom|1}}:
:$d \vee x = \top$
By definition of well inside relation:
:$a \eqslantless d$
The result follows.
{{qed}}
Theorem: Well Inside Elements Form Filter

:$\forall a \in S : \set{b \in S: a \eqslantless b}$ is a lattice filter

Proof:
Let $a \in S$.
Let $F = \set{b \in S: a \eqslantless b}$.
Theorem: Elements Well Inside Form Ideal

:$\forall a \in S : \set{b \in S: b \eqslantless a}$ is a a lattice ideal

Proof:
Let $a \in S$.
Let $I = \set{b \in S: b \eqslantless a}$.
Theorem: Dirichlet Beta Function at Odd Positive Integers/Examples/Dirichlet Beta Function of 5

:$\map \beta 5 = \dfrac {5 \pi^5} {1536} $

Proof:
{{begin-eqn}}
{{eqn | l = \map \beta {2 n + 1}
      | r = \paren {-1}^n \dfrac {E_{2 n} \pi^{2 n + 1} } {4^{n + 1} \paren {2 n}!}
      | c = Dirichlet Beta Function at Odd Positive Integers
}}
{{eqn | ll = \leadsto
      | l = \map \beta 5
      | r = \paren {-1}^2 \dfrac {E_4 \pi^5 } {4^3 \paren {4}!}
      | c = setting $n := 2$
}}
{{eqn | r = \frac {5 \pi^5} {1536}
      | c = Euler Number Values: $E_4 = 5$
}}
{{end-eqn}}
{{qed}}
Category:Dirichlet Beta Function at Odd Positive Integers
Category:Examples of Dirichlet Beta Function Values
oxjl7zr4xptu631ycqzo32ww93wc8uw
Theorem: Whole Sample Space represents Certain Event

Let the probability space of an experiment $\EE$ be $\struct {\Omega, \Sigma, \Pr}$.
The sample space $\Sigma$ represents an event which is certain.

Proof:
By definition, an event is a subset of the sample space $\Omega$.
Hence an outcome of $\EE$ is necessarily an element of $\Omega$.
That is, the probability that $\omega \in \Omega$ is $1$.
The result follows by definition of certain event.
Theorem: Universal Statement has no Existential Import

A universal statement of the form:
:''All $A$ are $B$
has no '''existential import'''.

Proof:
If there exist no $A$, then:
:''All $A$ are $B$
is vacuously true, and hence remains true.
If there exist no $B$, then:
:''All $A$ are $B$
is vacuously true when there exist no $A$.
Hence the result by definition of '''existential import'''.
{{qed}}
Theorem: Polylogarithm of Square

:$\map {\Li_s} z + \map {\Li_s} {-z} = 2^{1 - s} \map {\Li_s} {z^2}$

Proof:
<onlyinclude>
{{begin-eqn}}
{{eqn | l = \map {\Li_s} z + \map {\Li_s} {-z}
      | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^s} + \sum_{n \mathop = 1}^\infty \frac {\paren {-z}^n} {n^s}
      | c = {{Defof|Polylogarithm}}
}}
{{eqn | r = \paren {z + \frac {z^2} {2^s} + \frac {z^3} {3^s} + \frac {z^4} {4^s} + \frac {z^5} {5^s} + \frac {z^6} {6^s} + \cdots} + \paren {-z + \frac {z^2} {2^s} - \frac {z^3} {3^s} + \frac {z^4} {4^s} - \frac {z^5} {5^s} + \frac {z^6} {6^s} + \cdots}
      | c = 
}}
{{eqn | r = 2 \paren {\frac {z^2} {2^s} + \frac {z^4} {4^s} + \frac {z^6} {6^s} + \cdots}
      | c = odd terms cancel, even terms double
}}
{{eqn | r = \frac 2 {2^s} \paren {\frac {z^2} {1^s} + \frac {z^4} {2^s} + \frac {z^6} {3^s} + \cdots}
      | c = factoring out $2^s$
}}
{{eqn | r = 2^{1 - s} \sum_{n \mathop = 1}^\infty \frac {\paren {z^2}^n} {n^s}
      | c = 
}}
{{eqn | r = 2^{1 - s} \map {\Li_s} {z^2}
      | c = {{Defof|Polylogarithm}}
}}
{{end-eqn}}
{{qed}}
Category:Polylogarithm
jokt961hj9ofsg4mvmtffwf6g45xgzu
Theorem: Recurrence Relation for Polylogarithms

:$\ds \map {\Li_{s + 1} } z = \int_0^z \dfrac {\map {\Li_s} t} t \rd t$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^z \dfrac {\map {\Li_s} t} t \rd t
	  | r = \int_0^z \frac 1 t \times \sum_{n \mathop = 1}^\infty \frac {t^n} {n^s} \rd t
      | c = {{Defof|Polylogarithm}}
}}
{{eqn | r = \int_0^z \sum_{n \mathop = 1}^\infty \frac {t^{n - 1} } {n^s} \rd t
      | c = Quotient of Powers
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \int_0^z \frac {t^{n - 1} } {n^s} \rd t
      | c = Fubini's Theorem
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \intlimits {\frac {t^n} {n^{s + 1} } } 0 z
      | c = Primitive of Power
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^{s + 1} } 
      | c = 
}}
{{eqn | r = \map {\Li_{s + 1} } z
      | c = {{Defof|Polylogarithm}}
}}
{{end-eqn}}
{{qed}}
Category:Polylogarithm
Category:Recurrence Relations
iur4o737ir6yml1ocdofyjj6fkcty3g
Theorem: Exponential Distribution is Special Case of Gamma Distribution

The exponential distribution is a special case of the gamma distribution.

Proof:
{{ProofWanted|Need to rationalise the definitions}}
Theorem: Rate of Exponential Growth

Let $y = a e^{b t}$ be an exponential growth function.
Then the rate of growth of $y$ is proportional to the value of $y$ such that:
:$\dfrac {\d y} {\d t} = b y$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = a e^{b t}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d t}
      | r = a b e^{b t}
      | c = {{Corollary|Derivative of Exponential Function|1}}
}}
{{eqn | r = b y
      | c = Definition of $y$
}}
{{end-eqn}}
{{qed}}
Theorem: Existence of Ordinal with no Surjection from Set

Let $S$ be a set.
Then, there exists a non-empty ordinal $\alpha$ such that there is no surjection from $S$ to $\alpha$.

Proof:
By Hartogs' Lemma, let $\alpha$ be an ordinal such that there is no injection from $\alpha$ to $\powerset S$.
From Empty Mapping is Injective, it follows that $\alpha$ is non-empty.
{{AimForCont}} there is a surjection $\phi : S \to \alpha$.
Define $\psi : \alpha \to \powerset S$ as:
:$\map \psi \gamma = \set {x \in S : \map \phi x = \gamma}$
Let $\beta, \gamma \in \alpha$ such that:
:$\map \psi \beta = \map \psi \gamma$
Since $\phi$ is a surjection, there is some $x \in S$ such that:
:$\map \phi x = \beta$
from which it follows that:
:$x \in \map \psi \beta = \map \psi \gamma$
But then, by definition:
:$\map \phi x = \gamma$
so therefore, by definition of mapping:
:$\beta = \gamma$
Thus, by definition, $\psi$ is an injection from $\alpha$ to $\powerset S$.
{{finish}}
Category:Ordinals
Category:Surjections
hvbx5tc75z4k81mqd7ik2s2cqbme0mh
Theorem: Cartesian Product of Infinite Set Equivalent to Itself implies Axiom of Choice

Suppose that, for every Dedekind-infinite set $A$, it holds that:
:$A \sim A \times A$
where $\sim$ denotes set equivalence, and $\times$ denotes the cartesian product.
Then, the {{Axiom-link|Choice}} holds.

Proof:
By Zermelo's Well-Ordering Theorem is Equivalent to Axiom of Choice, it suffices to show that the hypothesis implies Zermelo's Well-Ordering Theorem.
Since every finite set is well-orderable, it suffices to consider only infinite sets.
Let $B$ be an arbitrary infinite set.
{{WLOG}}, assume that $B \cap \On = \O$.
By Existence of Ordinal with no Surjection from Set, let $\beta \in \On \setminus \set \O$ such that there is no surjection from $B$ to $\beta$.
From Set is Infinite iff exist Subsets of all Finite Cardinalities, it follows that $\beta$ is infinite.
We have:
:$\omega \subseteq \beta \subseteq B \cup \beta$
so by Equivalent Conditions for Dedekind-Infinite Set:
:$B \cup \beta$ is Dedekind-infinite.
Therefore, {{hypothesis}}, there exists a bijection:
:$\phi : B \cup \beta \to \paren {B \cup \beta} \times \paren {B \cup \beta}$
For each $x \in B$, define:
:$S_x = \set {\gamma \in \beta : \map \phi \gamma \in \beta \times \set x}$
{{AimForCont}} for some $x_0 \in B, S_{x_0} = \O$.
Then, since $\phi$ is a bijection, it follows that $\phi^{-1} \sqbrk {\beta \times \set {x_0}} \subseteq B$.
Hence, the mapping $\psi : B \to \beta$ defined as:
:$\map \psi y = \begin{cases} \gamma & : \map \phi y = \tuple {\gamma, x_0} \\ 0 & : \text{otherwise} \end{cases}$
is a surjection.
Since the contradicts the definition of $\beta$, we conclude that each $S_x \ne \O$.
Finally, we define $\chi : B \to \beta$ as:
:$\map \chi x = \min S_x$
Suppose that, for $x, y \in B$, we have:
:$\map \chi x = \map \chi y$
Then, since:
:$\map \phi {\map \chi x} \in \beta \times \set x$
:$\map \phi {\map \chi y} \in \beta \times \set y$
it follows from the equality that $x = y$.
Therefore, $\chi$ is an injection.
Thus, by Injection Induces Well-Ordering:
:$B$ is well-orderable
Since $B$ was arbitrary, it follows that Zermelo's Well-Ordering Theorem holds.
{{qed}}
Category:Cartesian Product
Category:Equivalents of Axiom of Choice
Category:Set Equivalence
4xhdxi2jdvnohjhc88ms8fb8uooanso
Theorem: Frame of Topological Space is Frame

:$\map \Omega T$ is a frame

Proof:
Recall that the frame of topological space $T$ is defined to be:
:$\map \Omega T = \struct{\tau, \subseteq}$
where $\subseteq$ denotes the subset relation.
From Topology forms Complete Lattice:
:$\map \Omega T$ is a complete lattice
Furthermore:
:$\forall \TT \subseteq \tau : \sup \TT = \bigcup \TT, \inf \TT = \paren{\bigcap \TT}^\circ$
where $\paren{\bigcap \TT}^\circ$ denotes the interior of $\bigcap \TT$
From Interior of Open Set and {{Open-set-axiom|2}}:
:$\forall U, V \in \tau : \paren{U \cap V}^\circ = U \cap V$
Hence:
:$\forall U, V \in \tau : U \wedge V = U \cap V$
From Intersection Distributes over Union (General Result):
:$\map \Omega T$ satisfies the infinite join distributive law
Hence $\map \Omega T$ is a frame by definition.
{{qed}}
Theorem: Locale of Topological Space is Locale

:$\map \Omega T$ is a locale

Proof:
By definition of frame of topological space:
:the frame of $T$ is $\map \Omega T$
From Frame of Topological Space is Frame:
:$\map \Omega T$ is a frame
By definition of locale:
:$\map \Omega T$ is a locale
{{qed}}
Theorem: Dilogarithm of One

:$\map {\Li_2} 1 = \map \zeta 2$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Li_2} z
      | r = \sum_{n \mathop = 1}^\infty \frac {z^n} {n^2}
      | c = Power Series Expansion for Spence's Function
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {1^n} {n^2}
      | c = $z := 1$
}}
{{eqn | r = \map \zeta 2
      | c = Basel Problem
}}
{{end-eqn}}
{{qed}}
Category:Examples of Dilogarithm Function
Category:Spence's Function
1stvi8czsl2uk52u4mge1y7iw6x8jr6