avewright/proofwiki-math huggingface dataset:
Theorem: Expectation of Negative Binomial Distribution/Type 1

Let $X$ be a discrete random variable with the type 1 negative binomial distribution with parameters $n$ and $p$.
Then the expectation of $X$ is given by:
:$\expect X = \dfrac n p$

Proof:
From Probability Generating Function of Negative Binomial Distribution (Type 1), we have:
:$\map {\Pi_X} s = \paren {\dfrac {p s} {1 - q s} }^n$
where $q = 1 - p$.
From Expectation of Discrete Random Variable from PGF, we have:
:$\expect X  = \map {\Pi'_X} 1$
We have:
{{begin-eqn}}
{{eqn | l = \map {\Pi'_X} s
      | r = \map {\frac \d {\d s} } {\frac {p s} {1 - q s} }^n
      | c = 
}}
{{eqn | r = n p \paren {\frac {\paren {p s}^{n - 1} } {\paren {1 - q s}^{n + 1} } }
      | c = First Derivative of PGF of Negative Binomial Distribution (Type 1)
}}
{{end-eqn}}
Plugging in $s = 1$:
{{begin-eqn}}
{{eqn | l = \map {\Pi'_X} 1
      | r = n p \paren {\frac {p^{n - 1} } {\paren {1 - q}^{n + 1} } }
      | c = 
}}
{{eqn | r = n p \paren {\frac {p^{n - 1} } {p^{n + 1} } }
      | c = as $p = 1 - q$
}}
{{eqn | ll= \leadsto
      | l = \expect X
      | r = \frac n p
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Derivatives of PGF of Negative Binomial Distribution/Type 1

Let $X$ be a discrete random variable with the type $1$ negative binomial distribution with parameters $n$ and $p$.
Then the derivatives of the PGF of $X$ {{WRT|Differentiation}} $s$ are:
:$\dfrac {\d^k} {\d s^k} \map {\Pi_X} s = ...$

Proof:
The Probability Generating Function of Negative Binomial Distribution (Type 1) is:
:$\map {\Pi_X} s = \paren {\dfrac {p s} {1 - q s} }^n$
We have that for a given type $1$ negative binomial distribution , $n, p$ and $q$ are constant.
{{ProofWanted}}
Category:Derivatives of PGF of Negative Binomial Distribution
Category:Negative Binomial Distribution (Type 1)
Category:Derivatives of PGFs
caawaiu7gczlo1r7hmluz1j0c2fntm3
Theorem: First Derivative of PGF of Negative Binomial Distribution/Type 1

Let $X$ be a discrete random variable with the type 1 negative binomial distribution (second form) with parameters $n$ and $p$.
Then the first derivative of the PGF of $X$ {{WRT|Differentiation}} $s$ is:
:$\dfrac \d {\d s} \map {\Pi_X} s = n p \paren {\dfrac {\paren {p s}^{n - 1} } {\paren {1 - q s}^{n + 1} } }$

Proof:
The Probability Generating Function of Negative Binomial Distribution (Type 1) is:
:$\map {\Pi_X} s = \paren {\dfrac {p s} {1 - q s} }^n$
We have that for a given type 1 negative binomial distribution, $n, p$ and $q$ are constant.
Thus we have:
{{begin-eqn}}
{{eqn | l = \frac \d {\d s} \map {\Pi_X} s
      | r = \frac \d {\d s} \paren {\frac {p s} {1 - q s} }^n
      | c = 
}}
{{eqn | r = n \paren {\frac {p s} {1 - q s} }^{n - 1} \frac \d {\d s} \paren {\frac {p s} {1 - q s} }
      | c = Power Rule for Derivatives and Chain Rule for Derivatives
}}
{{eqn | r = n \paren {\frac {p s} {1 - q s} }^{n - 1} \paren {\frac {\paren {1 - q s} \frac \d {\d s} \paren {p s} - p s \frac \d {\d s} \paren {1 - q s} } {\paren {1 - q s}^2} }
      | c = Quotient Rule for Derivatives and Chain Rule for Derivatives
}}
{{eqn | r = n \paren {\frac {p s} {1 - q s} }^{n - 1} \paren {\frac {\paren {1 - q s} p - p s \paren {-q} } {\paren {1 - q s}^2} }
      | c = Power Rule for Derivatives where $n = 1$
}}
{{eqn | r = n \paren {\frac {p s} {1 - q s} }^{n - 1} \paren {\frac {p - p q s + p q s} {\paren {1 - q s}^2} }
      | c = 
}}
{{eqn | r = n \paren {\frac {p s} {1 - q s} }^{n - 1} \paren {\frac p {\paren {1 - q s}^2} }
      | c = 
}}
{{eqn | r = n p \paren {\frac {\paren {p s}^{n - 1} } {\paren {1 - q s}^{n + 1} } }
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:First Derivative of PGF of Negative Binomial Distribution
Category:Negative Binomial Distribution (Type 1)
Category:Derivatives of PGFs
7yld5ft2bks3wxoa37gl3sasjwvujjj
Theorem: Nth Derivative of Reciprocal of Mth Power/Corollary

The $n$th derivative of $\dfrac 1 x$ {{WRT|Differentiation}} $x$ is:
:$\dfrac {\d^n} {\d x^n} \dfrac 1 x = \dfrac {\paren {-1}^n n!} {x^{n + 1} }$
where $n!$ denotes $n$ factorial.

Proof:
Follows directly from Nth Derivative of Reciprocal of Mth Power by putting $m = 1$.
{{Qed}}
Category:Derivatives
Category:Reciprocals
5esfog7mo3vmt4mb8i0vdfikz5koxty
Theorem: First Derivative of PGF of Negative Binomial Distribution/Type 2

Let $X$ be a discrete random variable with the type 2 negative binomial distribution with parameters $n$ and $p$.
Then the first derivative of the PGF of $X$ {{WRT|Differentiation}} $s$ is:
:$\dfrac \d {\d s} \map {\Pi_X} s = \dfrac {n p} q \paren {\dfrac q {1 - p s} }^{n + 1}$

Proof:
The Probability Generating Function of Negative Binomial Distribution (Type 2) is:
:$\map {\Pi_X} s = \paren {\dfrac q {1 - p s} }^n$
We have that for a given type 2 negative binomial distribution, $n, p$ and $q$ are constant.
Thus we have:
{{begin-eqn}}
{{eqn | l = \frac \d {\d s} \map {\Pi_X} s
      | r = \map {\frac \d {\d s} } {\paren {\dfrac q {1 - p s} }^n}
      | c = 
}}
{{eqn | r = n \paren {\frac q {1 - p s} }^{n - 1} \map {\frac \d {\d s} } {\frac q {1 - p s} }
      | c = Power Rule for Derivatives and Chain Rule for Derivatives
}}
{{eqn | r = n \paren {\frac q {1 - p s} }^{n - 1} \paren {-p} \paren {\frac {-q} {\paren {1 - p s}^2} }
      | c = Power Rule for Derivatives and Chain Rule for Derivatives
}}
{{eqn | r = \frac {n p} q \paren {\frac q {1 - p s} }^{n + 1}
      | c = simplifying
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:First Derivative of PGF of Negative Binomial Distribution
Category:Negative Binomial Distribution (Type 2)
Category:Derivatives of PGFs
ky3fgjuq7uzxsry88usd1ldm76jf2ts
Theorem: Expectation of Negative Binomial Distribution/Type 2

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

Proof:
From Probability Generating Function of Negative Binomial Distribution (Type 2):
:$\map {\Pi_X} s = \paren {\dfrac q {1 - p s} }^r$
From Expectation of Discrete Random Variable from PGF:
:$\expect X = \map {\Pi'_X} 1$
We have:
{{begin-eqn}}
{{eqn | l = \map {\Pi'_X} s
      | r = \map {\frac \d {\d s} } {\paren {\dfrac q {1 - p s} }^r}
      | c =
}}
{{eqn | r = \dfrac {r p} q \paren {\dfrac q {1 - p s} }^{r + 1}
      | c = First Derivative of PGF of Negative Binomial Distribution (Type 2)
}}
{{end-eqn}}
Plugging in $s = 1$:
{{begin-eqn}}
{{eqn | l= \map {\Pi'_X} 1
      | r= \frac {r p} q \paren {\frac q {1 - p} }^{r + 1}
      | c=
}}
{{eqn | r = \frac {r p} q \paren {\frac q q}^{r + 1}
      | c = as $p = 1 - q$
}}
{{eqn | ll= \leadsto
      | l = \expect X
      | r = \frac {r p} q
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Closure Condition for Hausdorff Space

Let $\struct {S, \tau}$ be a topological space.
Then $\struct {S, \tau}$ is a Hausdorff space {{iff}}:
:For all $x, y \in S$ such that $x \ne y$, there exists an open set $U$ such that $x \in U$ and $y \notin U^-$, where $U^-$ is the closure of $U$.

Proof:
=== Necessary Condition ===
Let $\struct {S, \tau}$ be a Hausdorff space.
Let $x, y \in S$ with $x \ne y$.
Then by the definition of Hausdorff space there exist open sets $U, V \subseteq S$ such that:
:$x \in U$
:$y \in V$
:$U \cap V = \O$
By Empty Intersection iff Subset of Complement, $U \subseteq S \setminus V$.
By definition, $S \setminus V$ is closed.
Thus by definition of closure:
:$U^- \subseteq S \setminus V$
Since $y \in V$, by definition of relative complement it follows that $y \notin S \setminus V$.
By definition of subset, $y \notin U^-$.
{{qed|lemma}}
Theorem: Derivatives of PGF of Negative Binomial Distribution/Type 2

Let $X$ be a discrete random variable with the type $2$ negative binomial distribution with parameters $n$ and $p$.
Then the derivatives of the PGF of $X$ {{WRT|Differentiation}} $s$ are:
:$\dfrac {\d^k} {\d s^k} \map {\Pi_X} s = \dfrac {n^{\overline k} p^k} {q^k} \paren {\dfrac q {1 - p s} }^{n + k}$
where:
:$n^{\overline k}$ is the rising factorial: $n^{\overline k} = n \paren {n + 1} \paren {n + 2} \cdots \paren {n + k - 1}$
:$q = 1 - p$

Proof:
Proof by induction:
The Probability Generating Function of Negative Binomial Distribution (Type 2) is:
:$\ds \map {\Pi_X} s = \paren {\frac q {1 - p s} }^n$
For all $k \in \N_{> 0}$, let $\map P k$ be the proposition:
:$\dfrac {\d^k} {\d s^k} \map {\Pi_X} s = \dfrac {n^{\overline k} p^k} {q^k} \paren {\dfrac q {1 - p s} }^{n + k}$
Theorem: Second Derivative of PGF of Negative Binomial Distribution/Type 2

Let $X$ be a discrete random variable with the type $2$ negative binomial distribution with parameters $n$ and $p$.
Then the second derivative of the PGF of $X$ {{WRT|Differentiation}} $s$ is:
:$\dfrac {\d^2} {\d s^2} \map {\Pi_X} s = \dfrac {n \paren {n + 1} p^2} {q^2} \paren {\dfrac q {1 - p s} }^{n + 2}$
where $q = 1 - p$.

Proof:
The Probability Generating Function of Negative Binomial Distribution (Type 2) is:
:$\map {\Pi_X} s = \paren {\dfrac q {1 - p s} }^n$
From Derivatives of PGF of Negative Binomial Distribution: Type 2:
:$(1): \quad \dfrac {\d^k} {\d s^k} \map {\Pi_X} s = \dfrac {n^{\overline k} p^k} {q^k} \paren {\dfrac q {1 - p s} }^{n + k}$
where:
:$n^{\overline k}$ is the rising factorial: $n^{\overline k} = n \paren {n + 1} \paren {n + 2} \cdots \paren {n + k - 1}$
:$q = 1 - p$
Putting $k = 2$ in $(1)$ above yields the required solution.
{{qed}}
Category:Second Derivative of PGF of Negative Binomial Distribution
Category:Negative Binomial Distribution (Type 2)
Category:Derivatives of PGFs
r15o8owoet01fgzwy63pqe5p1h2v6xf
Theorem: Variance of Negative Binomial Distribution/Type 1

Let $X$ be a discrete random variable with the type $1$ negative binomial distribution with parameters $r$ and $p$.
Then the variance of $X$ is given by:
:$\var X = \dfrac {r q} {p^2}$
where $q = 1 - p$.

Proof:
From Variance of Discrete Random Variable from PGF:
:$\var X = \map {\Pi' '_X} 1 + \mu - \mu^2$
where $\mu = \expect X$ is the expectation of $X$.
From the Probability Generating Function of Negative Binomial Distribution (Type 1):
:$\map {\Pi_X} s = \dfrac {p s} {1 - q s}$
From Expectation of Negative Binomial Distribution (Type 1):
:$\mu = \dfrac r p$
From Second Derivative of PGF of Negative Binomial Distribution (Type 1):
:$\dfrac {\d^2} {\d s^2} \map {\Pi_X} s = \paren {\dfrac {p s} {1 - q s} }^{r + 2} \paren {\dfrac {r \paren {r - 1} + 2 r q s} {\paren {p s^2}^2} }$
Putting $s = 1$ and using the formula $\map {\Pi' '_X} 1 + \mu - \mu^2$:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \paren {\frac p {1 - q} }^{r + 2} \paren {\frac {r \paren {n - 1} + 2 n q} {p^2} } + \frac r p - \frac {r^2} {p^2}
      | c = 
}}
{{eqn | r = \paren {\frac p p}^{r + 2} \paren {\frac {r \paren {r - 1} + 2 r q} {p^2} } + \frac {r \paren {1 - q} } {p^2} - \frac {r^2} {p^2}
      | c = as $q = 1 - p$ and so $p = 1 - q$
}}
{{eqn | r = \frac {r^2 - r + 2 r q + r - r q - r^2} {p^2}
      | c = gathering terms and multiplying out
}}
{{eqn | r = \frac {r q} {p^2}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: PGF of Sum of Independent Discrete Random Variables/General Result

Let:
:$Z = X_1 + X_2 + \cdots + X_n$
where each of $X_1, X_2, \ldots, X_n$ are independent discrete random variables with PGFs $\map {\Pi_{X_1} } s, \map {\Pi_{X_2} } s, \ldots, \map {\Pi_{X_n} } s$.
Then:
:$\ds \map {\Pi_Z} s = \prod_{j \mathop = 1}^n \map {\Pi_{X_j} } s$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \map {\Pi_Z} s = \prod_{j \mathop = 1}^m \map {\Pi_{X_j} } s$
whenever $m \le n$
$\map P 1$ is true, as this just says $\map {\Pi_{X_1} } s = \map {\Pi_{X_1} } s$.
Theorem: Disjoint Compact Sets in Hausdorff Space have Disjoint Neighborhoods/Lemma

Let $\struct {S, \tau}$ be a Hausdorff space.
Let $C$ be a compact subspace of $S$.
Let $x \in S \setminus C$.
Then there exist open sets $U$ and $V$ such that $x \in U$, $C \subseteq V$, and $U \cap V = \O$.

Proof:
Let $\FF$ be the set of all ordered pairs $\tuple {A, B}$ such that $A$ and $B$ are open, $x \in A$, and $A \cap B = \O$.
As a set of ordered pairs, $\FF$ constitutes a relation on $\tau$:
:$\FF \subseteq \tau \times \tau$
By the definition of Hausdorff space, for each $y \in C$ there exists an element $\tuple {A, B} \in \FF$ such that $y \in B$.
Thus the image of $\FF$ covers $C$.
By the definition of compactness, there exists a finite subset $\GG \subseteq \FF$ such that:
:$\ds C \subseteq V = \bigcup \Img \GG$
{{explain|This does not follow directly. See the parent page for an outline of how the principle of finite choice leads to it.}}
Then $\Preimg \GG$ is also finite, so by the definition of a topology:
:$\ds U = \bigcap \Preimg \GG$ is open.
Then $x \in U$, $C \subseteq V$, and $U \cap V = \O$.
{{qed}}
Category:Disjoint Compact Sets in Hausdorff Space have Disjoint Neighborhoods
pale7t5fiairun6t7me7247p3s2xybf
Theorem: Sum of Independent Binomial Random Variables

Let $X$ and $Y$ be discrete random variables with a binomial distribution:
:$X \sim \Binomial m p$
and
:$Y \sim \Binomial n p$
Let $X$ and $Y$ be independent.
Then their sum $Z = X + Y$ is distributed as:
:$Z \sim \Binomial {m + n} p$

Proof:
From Probability Generating Function of Poisson Distribution, we have that the probability generating functions of $X$ and $Y$ are given by:
:$\map {\Pi_X} s = \paren {q + p s}^m$
:$\map {\Pi_Y} s = \paren {q + p s}^n$
respectively.
Now because of their independence, we have:
{{begin-eqn}}
{{eqn | l = \map {\Pi_{X + Y} } s
      | r = \map {\Pi_X} s \map {\Pi_Y} s
      | c = PGF of Sum of Independent Discrete Random Variables
}}
{{eqn | r = \paren {q + p s}^m \paren {q + p s}^n
      | c = Definition of $X$ and $Y$
}}
{{eqn | r = \paren {q + p s}^{m + n}
      | c = Product of Powers
}}
{{end-eqn}}
This is the probability generating function for a discrete random variable with a binomial distribution:
:$\Binomial {m + n} p$
Therefore:
:$Z = X + Y \sim \Binomial {m + n} p$
{{qed}}
Theorem: Field has Algebraic Closure

Every field has an algebraic closure.

Proof:
Let $F$ be a field.
Let $\FF$ be the collection of all extensions of $F$. 
{{explain|Is $\FF$ a set or a proper class? It is not obvious that this collection is "small enough" to be a set, and I was unable to find a proof of this on ProofWiki.<br/>(On the other hand, does it matter which it is? // Yes, because Zorn's lemma only covers the case of it being a set.)}}
Define an ordering on $\FF$ thus:
:$\forall K, L \in \FF: K \preceq L \iff L$ is an extension of $K$.
Let $C$ be a chain in $\FF$.
Let $\ds E = \bigcup_{K \mathop \in C} K$.
$E$ satisfies all field axioms, so $E \in \FF$.
{{explain|Why does $E$ satisfy all field axioms?}}
By Set is Subset of Union, $E$ is an upper bound for $C$. 
By Zorn's Lemma, $C$ has a maximal element $m$.
Then $m$ is an algebraic closure of $F$.
{{explain|Why is this an algebraic closure of $F$?}}
{{qed}}
{{BPI}}
Category:Field Theory
dgzdpdj2ah1m5xkjilfbbj2vtbqto3m
Theorem: Point Finite Set of Open Sets in Separable Space is Countable

Let $\struct {X, \tau}$ be a separable space.
Let $\FF$ be a point finite set of open sets of $X$.
Then $\FF$ is countable.

Proof:
Since $\struct {X, \tau}$ is separable, $X$ has a countable everywhere dense subset $S$.
{{WLOG}}, assume that $\O \notin \FF$.
By the definition of point finite, $\set {V \in \FF: x \in V}$ is finite for each $x \in S$.
From Open Set Characterization of Denseness, each element of $\FF$ contains an element of $S$.
From Union of Set of Sets when a Set Intersects All:
:$\FF = \ds \bigcup_{x \mathop \in S} \set {V \in \FF: x \in V}$
Thus by Countable Union of Finite Sets is Countable, $\FF$ is countable.
{{qed}}
Category:Topology
p4hej3bsxrqio158g6062yrw75chyke
Theorem: Countable Union of Finite Sets is Countable

The following statements are equivalent in $\mathrm{ZF}^-$:
:The Axiom of Countable Choice for Finite Sets holds.
:The union of any countable set of finite sets is countable.

Proof:
=== Axiom of Countable Choice for Finite Sets implies Countable Union Condition for Finite Sets ===
Suppose that the Axiom of Countable Choice for Finite Sets holds.
Let $\FF$ be a countable set of non-empty finite sets.
Then $\FF$ is either finite or countably infinite.
If $\FF$ is finite, then $\bigcup \FF$ is finite by Finite Union of Finite Sets is Finite, and thus countable.
Suppose instead that $\FF$ is countably infinite.
Then there is a bijection $\mathbf f: \N \to \FF$.
Written in the family notation, this means that $\mathbf f = \family {F_m}_{m \mathop \in \N}$, with the properties that:
:$\forall m \in \N: F_m \in \FF$
:for all $F \in \FF$ there is exactly one $m \in \N$ such that $F = F_m$
Hence $\ds \bigcup \FF$ is the same thing as $\ds \bigcup \limits_{m \mathop \in \N} F_m$.
Each $F \in \FF$ is finite..
Also, {{hypothesis}}, each $F \in \FF$ is non-empty.
Hence the cardinality $k$ of $F$ is a (strictly) positive integer $k \ge 1$.
By definition of set equivalence, there exists a bijection $\set {0, \ldots, k - 1} \to F$.
Let $\map \BB F$ be the (non-empty) set of all such bijections $\set {0, \ldots, k - 1} \to F$.
Then by Cardinality of Set of Bijections:
:$\map \BB F$ is finite.
The family $\family {\map \BB {F_m} }_{m \mathop \in \N}$ is then a countable family of non-empty finite sets.
By the axiom of countable choice for finite sets the family $\family {\map \BB {F_m} }_{m \mathop \in \N}$ has a choice function:
:$\mathbf q = \family {q_m}_{m \mathop \in \N}$
Each $q_m$ is thus a bijection $\set {0, \ldots, \card {F_m} - 1} \to F_m$.
Define a mapping $\ds \gamma: \N^2 \to \bigcup_{m \mathop \in \N} F_m$ as:
:$\forall m, n \in \N: \map \gamma {m, n} = \begin {cases}
\map {q_m} n & : n \le \card {F_m}-1 \\
\map {q_0} 0 & : \text {otherwise}
\end {cases}$
Every $\ds x \in \bigcup_{m \mathop \in \N} F_m$ is element of some $F_m \in \FF$.
Thereby $x$ is the image of some integer $n \le \card {F_m} - 1$ under the map $q_m$.
$x$ is then of the form $\map \gamma {m, n}$ for some $\tuple {m, n} \in \N^2$.
Since $x \in \bigcup_{m \mathop \in \N} F_m$ is arbitrary, $\gamma$ is surjective.
Finally, let $\sigma$ be some surjection $\N \to \N^2$.
From Cartesian Product of Countable Sets is Countable, such a map exists.
By Composite of Surjections is Surjection $\gamma \circ \sigma$ is a surjection $\N \to \bigcup \FF$.
Hence $\gamma \circ \sigma$ is countable.
{{qed|lemma}}
Theorem: Reverse Triangle Inequality/Normed Vector Space

Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Then:
:$\forall x, y \in X: \norm {x - y} \ge \size {\norm x - \norm y}$

Proof:
Let $d$ denote the metric induced by $\norm {\, \cdot \,}$, that is:
:$\map d {x, y} = \norm {x - y}$
From Metric Induced by Norm is Metric we have that $d$ is indeed a  metric.
Then, from the Reverse Triangle Inequality as applied to metric spaces:
:$\forall x, y, z \in X: \size {\norm {x - z} - \norm {y - z} } \le \norm {x - y}$
Then:
:$\forall x, y \in X: \size {\norm x - \norm y} = \size {\norm {x - 0} - \norm {y - 0} } \le \norm {x - y}$.
{{qed}}
Theorem: Equivalence of Forms of Axiom of Countable Choice

The following forms of the Axiom of Countable Choice are equivalent in $\mathrm{ZF}^-$:
{{explain|$\mathrm{ZF}^-$}}

Proof:
=== Form 1 implies Form 2 ===
Suppose that Axiom of Countable Choice: Form 1 holds.
Let $S$ be a countable set of non-empty sets.
Then $S$ is either finite or countably infinite.
If $S$ is finite, then it has a choice function by the Principle of Finite Choice.
Suppose instead that $S$ is countably infinite.
Then there exists a bijection $f: \N \to S$.
Thus by Form 1, there exists a mapping $g: \N \to \bigcup S$ such that:
:$\forall n \in \N: g \left({n}\right) \in f \left({n}\right)$
Then $g \circ f^{-1}: S \to \bigcup S$ is a choice function for $S$.
As every countable set has a choice function, Axiom of Countable Choice: Form 2 holds.
{{qed|lemma}}
Theorem: GCD from Generator of Ideal

Let $m, n \in \Z$, with either $m \ne 0$ or $n \ne 0$.
Let $I = \ideal {m, n}$ be the ideal generated by $m$ and $n$.
Let $d$ be a non-negative generator for the principal ideal $I$.
Then:
:$\gcd \set {m, n} =  d$
where $\gcd \set {m, n}$ denotes the greatest common divisor of $m$ and $n$.

Proof:
First we show that such an element $d$ exists.
By Ring of Integers is Principal Ideal Domain there exists a generator $e$ of $I$.
If $e < 0$, then since the units of $\Z$ are $\set {\pm 1}$, we have by definition that $-e$ is an associate of $e$.
Therefore by $(3)$ of Principal Ideals in Integral Domain $-e > 0$ is also a generator of $I$.
In particular setting $d = \max \set {e, -e}$, $d$ is a non-negative generator of $I$.
By Bézout's Identity, we are required to show that $d$ is the smallest positive integer combination of $m$ and $n$.
By definition:
:$I = \set {a m + b n: a, b \in \Z}$
Thus we are required to show that $d$ is the smallest positive element of $I$.
Suppose that $d' \le d$ is a positive element of $I$, not larger than $d$.
By hypothesis $d$ generates $I$, so there exists $a \in \Z$ such that $d' = ad$.
Since $d > 0$, we can therefore write $a = \dfrac {d'} d \in \Q$.
Moreover, because $d' > 0$, by $(6)$ of Properties of Ordered Ring we have:
:$0 = \dfrac 0 d < \dfrac {d'} d$
Using the hypothesis that $d' \le d$, we have the pair of inequalities:
:$0 < a = \dfrac {d'} d \le 1$
By the definition we have $a \in \Z$, so this shows that $\dfrac {d'} d = 1$.
It follows that $d' = d$.
Therefore there is no positive element of $I$ smaller than $d$.
{{Qed}}
Category:Greatest Common Divisor
2tomow20daqrvnxy44ku0leqp66cdpp
Theorem: Finite Union of Finite Sets is Finite

Let $S$ be a finite set of finite sets.
Then the union of $S$ is finite.

Proof:
The proof proceeds by induction.
Let $S$ be a finite set with cardinality $n$.
If $n = 0$ then $S = \O$, so $\bigcup S = \O$, which is finite.
Suppose that an arbitrary finite set with cardinality $n$ of finite sets has a finite union.
Let $S$ have cardinality $n^+$.
Then there is a bijection $f: n^+ \to S$.
Then:
:$\ds \bigcup S = \bigcup_{k \mathop \in n^+} \map f k = \bigcup_{k \mathop \in n} \map f k \cup \map f n$
{{explain|Explain in detail.}}
By Union of Finite Sets is Finite, $\bigcup S$ is finite.
{{qed}}
Theorem: Finite Union of Finite Sets is Finite

Let $S$ be a finite set of finite sets.
Then the union of $S$ is finite.

Proof:
Let $S = \set {A_1, \ldots, A_n}$ such that $A_k$ is finite $\forall k = 1, \ldots, n$.
Set:
: $m = \max \set {\card {A_1}, \ldots, \card {A_n} }$
Then:
: $\ds \card {\bigcup_{k \mathop = 1}^n A_k} \le \sum_{k \mathop = 1}^n \card {A_k} \le \sum_{k \mathop = 1}^n m = n m$
{{explain|needs to invoke a link to result that shows $\card {\bigcup_{k \mathop {{=}} 1}^n A_k} \le \sum_{k \mathop {{=}} 1}^n \card {A_k}$}}
Hence the result.
{{qed}}
Theorem: Open Set Characterization of Denseness

Let $\struct {X, \tau}$ be a topological space.
Let $S \subseteq X$.
Then $S$ is (everywhere) dense in $X$ {{iff}} every non-empty ($\tau$-)open set contains an element of $S$.

Proof:
=== Necessary Condition ===
Let $S$ be everywhere dense in $X$.
Let $U$ be open and non-empty.
Then $U$ has an element $x$.
Since $S$ is everywhere dense in $X$, $x \in S^-$, the closure of $S$.
By Equivalence of Definitions of Adherent Point of Set, every open neighborhood of $x$ contains an element of $S$.
Thus in particular, $U$ contains an element of $S$.
{{qed|lemma}}
Theorem: Union of Set of Sets when a Set Intersects All

Let $F$ be a set of sets.
Let $S$ be a set or class.
Suppose that:
:$\forall A \in F: A \cap S \ne \O$
Then:
:$\ds F = \bigcup_{x \mathop \in S} \set {A \in F: x \in A}$

Proof:
Suppose that $B \in F$.
Then $B \cap S$ has an element $x_B$.
Thus:
:$B \in \set {A \in F: x_B \in A}$
By the definition of union:
:$\ds B \in \bigcup_{x \mathop \in S} \set {A \in F: x \in A}$
Suppose instead that:
:$\ds B \in \bigcup_{x \mathop \in S} \set {A \in F: x \in A}$
Then by the definition of union, there exists an $x_B \in S$ such that:
:$B \in \set {A \in F: x_B \in A} \subseteq F$
Thus $B \in F$.
We have shown that:
:$\ds \forall B: \paren {B \in F \iff B \in \bigcup_{x \mathop \in S} \set {A \in F: x \in A} }$
Therefore by definition of set equality:
:$\ds F = \bigcup_{x \mathop \in S} \set {A \in F: x \in A}$
{{qed}}
Category:Set Union
qtmohjuy7nb04ci58hyvi9otao3x8p2