avewright/proofwiki-math huggingface dataset:
Theorem: Limit to Infinity of Binomial Coefficient over Power

Let $k \in \R \setminus \set {-1, -2, -3, \dotsc}$.
Then:
:$\ds \lim_{r \mathop \to \infty} \dfrac {\dbinom r k} {r^k} = \frac 1 {\map \Gamma {k + 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{r \mathop \to \infty} \frac {\dbinom r k} {r^k}
      | r = \lim_{r \mathop \to \infty} \frac {\map \Gamma {r + 1} } {\map \Gamma {k + 1} \map \Gamma {r - k + 1} r^k}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \lim_{r \mathop \to \infty} \frac 1 {\map \Gamma {k + 1} } \frac {\sqrt {2 \pi r} \paren {r / e}^r} {\sqrt {2 \pi \paren {r - k} } \paren {\paren {r - k} / e}^{r - k} r^k}
      | c = Stirling's Formula for Gamma Function; first term
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} } \lim_{r \mathop \to \infty} \sqrt {\frac r {r - k} } \paren {\frac r e}^r \paren {\frac e {r - k} }^{r - k} \frac 1 {r^k}
      | c = $\sqrt {2 \pi}$ cancels
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} } \lim_{r \mathop \to \infty} \sqrt {\frac r {r - k} } \frac 1 {e^k} \frac {r^{r - k} } {\paren {r - k}^{r - k} }
      | c = Exponent Combination Laws: Quotient of Powers
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} } \frac 1 {e^k} \lim_{r \mathop \to \infty} \frac {r^{r - k + \frac 1 2} } {\paren {r - k}^{r - k + \frac 1 2} }
      | c = Product of Powers
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} } \frac 1 {e^k} \lim_{r \mathop \to \infty} \frac {r^{r - k + \frac 1 2} } {\paren {r - k}^{r - k + \frac 1 2} } \times \frac {\paren {\frac 1 r}^{r - k + \frac 1 2} } {\paren {\frac 1 r}^{r - k + \frac 1 2} }
      | c = multiplying top and bottom by $\paren {\frac 1 r}^{r - k + \frac 1 2}$ 
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} } \frac 1 {e^k} \lim_{r \mathop \to \infty} \frac 1 {\paren {1 - k / r}^r \times \paren {1 - k / r}^{\frac 1 2 - k} }
      | c = Product of Powers
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} } \frac 1 {e^k} \frac 1 {e^{-k} }
      | c = {{Defof|Euler's Number}} $e^{-k} = \lim_{r \mathop \to \infty} \paren {1 - k / r}^r$
}}
{{eqn | r = \frac 1 {\map \Gamma {k + 1} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Limit to Infinity of Binomial Coefficient over Power/Integer

Let $k \in \N$.
Then:
:$\ds \lim_{r \mathop \to \infty} \frac {\dbinom r k} {r^k} = \frac 1 {k!}$

Proof:
{{begin-eqn}}
{{eqn | q = \forall r \in \R
      | l = \frac {\dbinom r k} {r^k}
      | r = \frac 1 {k !} \cdot \frac {r^{\underline k} } {r^k}
      | c = {{Defof|Binomial Coefficient/Real Numbers|Binomial Coefficient}}
}}
{{eqn | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \frac {r - j} r
      | c = {{Defof|Falling Factorial}}, {{Defof|Integer Power}}
}}
{{eqn | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \paren {1 - \frac j r}
}}
{{eqn | ll = \leadsto
      | l = \lim_{r \mathop \to \infty} \frac {\dbinom r k} {r^k}
      | r = \lim_{r \mathop \to \infty} \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \paren {1 - \frac j r}
}}
{{eqn | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \lim_{r \mathop \to \infty} \paren {1 - \frac j r}
      | c = Product Rule for Real Sequences
}}
{{eqn | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} \paren {1 - j \lim_{r \mathop \to \infty} \frac 1 r}
      | c = Combined Sum Rule for Real Sequences
}}
{{eqn | r = \frac 1 {k !} \prod_{j \mathop = 0}^{k - 1} 1
      | c = Sequence of Reciprocals is Null Sequence
}}
{{eqn | r = \frac 1 {k !}
}}
{{end-eqn}}
{{qed}}
Category:Limit to Infinity of Binomial Coefficient over Power
1j5x4bybippnp0rum1fl7m1er17zz3j
Theorem: Cover is Cover of Subset

Let $S$ be a set.
Let $\CC$ be a cover of $S$.
Let $T \subseteq S$ be a subset of $S$.
Then, $\CC$ is a cover of $T$.

Proof:
By definition of a cover:
:$\ds S \subseteq \bigcup C$
But then, by Subset Relation is Transitive:
:$\ds T \subseteq \bigcup C$
Therefore, $C$ is a cover of $T$ by definition.
{{qed}}
Category:Covers
gwxoy47g2air474ny30lt1cw1t9uby5
Theorem: Outer Jordan Content is Monotone

Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space.
Suppose that $A \subseteq B$.
Then:
:$\map {m^*} A \le \map {m^*} B$
where $m^*$ denotes the outer Jordan content.

Proof:
Let $C$ be a finite covering of $B$ by closed rectangles.
Since $A \subseteq B$, by Cover is Cover of Subset:
:$C$ is a finite covering of $A$ by closed rectangles.
Therefore, by definition of the outer Jordan content:
:$\ds \map {m^*} A \le \sum_{R \mathop \in C} \map V R$
But, since $C$ was arbitrary:
:$\map {m^*} A$ is a lower bound of $\ds \set {\sum_{R \mathop \in C} \map V R : C}$
where $C$ ranges over all finite coverings of $B$ by closed rectangles.
Hence, by definition of outer Jordan content, and of infimum:
:$\map {m^*} A \le \map {m^*} B$
{{qed}}
Category:Outer Jordan Content
Category:Measure Theory
4ymjzu2lbhhxqbn396z27vxr0jh92fn
Theorem: Inner Jordan Content is Monotone

Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space.
Suppose that $A \subseteq B$.
Then:
:$\map {m_*} A \le \map {m_*} B$
where $m_*$ denotes the inner Jordan content.

Proof:
Let $R \subseteq \R^n$ be a closed $n$-rectangle that contains $B$.
Then, by Subset Relation is Transitive, $R$ contains $A$ as well.
By Set Difference with Subset is Superset of Set Difference:
:$R \setminus B \subseteq R \setminus A$
So, by Outer Jordan Content is Monotone:
:$\map {m^*} {R \setminus B} \le \map {m^*} {R \setminus A}$
Therefore:
:$\map V R - \map {m^*} {R \setminus B} \ge \map V R - \map {m^*} {R \setminus A}$
Hence the result, by definition of inner Jordan content.
{{qed}}
Category:Jordan Content
tg606muf684ghptbtu2amu86hy84mly
Theorem: Union of Covers is Cover of Union

Let $\sequence {S_i}_{i \in I}$ be an indexed family of sets.
For each $i \in I$, let $\CC_i$ be a cover of $S_i$.
Then, $\ds \bigcup_{i \mathop \in I} \CC_i$ is a cover of $\ds \bigcup_{i \mathop \in I} S_i$.

Proof:
Let $\ds x \in \bigcup_{i \mathop \in I} S_i$ be arbitrary.
By definition of union, there is some $i \in I$ such that:
:$x \in S_i$
Then, by definition of cover, there is some $C \in \CC_i$ such that:
:$x \in C$
But, by definition of union:
:$\ds C \in \bigcup_{i \mathop \in I} \CC_i$
Hence, there is some $\ds C \in \bigcup_{i \mathop \in I} \CC_i$ such that $x \in C$.
As $x$ was arbitrary, the result follows from the definition of cover.
{{qed}}
Category:Covers
dai7wfug993yt5mlflqjnrkh6xvhnt7
Theorem: Outer Jordan Content is Subadditive

Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space.
Then:
:$\map {m^*} {A \cup B} \le \map {m^*} A + \map {m^*} B$
where $m^*$ denotes the outer Jordan content.

Proof:
Let $\epsilon > 0$ be arbitrary.
By Characterizing Property of Infimum of Subset of Real Numbers, select:
:$C$ to be a finite covering of $A$ by closed $n$-rectangles such that:
::$\ds \sum_{R \mathop \in C} \map V R < \map {m^*} A + \frac \epsilon 2$
:$D$ to be a finite covering of $B$ by closed $n$-rectangles such that:
::$\ds \sum_{R \mathop \in D} \map V R < \map {m^*} B + \frac \epsilon 2$
Define $E = C \cup D$.
By Union of Finite Sets is Finite, $E$ is a finite set of closed $n$-rectangles.
So, by Union of Covers is Cover of Union:
:$C \cup D$ is a finite covering of $A \cup B$ by closed $n$-rectangles.
We have:
{{begin-eqn}}
{{eqn | l = \map {m^*} {A \cup B}
      | o = \le
      | r = \sum_{R \mathop \in E} \map V R
      | c = {{Defof|Outer Jordan Content}}
}}
{{eqn | r = \sum_{R \mathop \in C \cup D} \map V R
}}
{{eqn | o = \le
      | r = \sum_{R \mathop \in C} \map V R + \sum_{R \mathop \in D} \map V R
      | c = $\map V R$ is non-negative, so any double-counted elements only increase the sum
}}
{{eqn | o = <
      | r = \map {m^*} A + \map {m^*} B + \epsilon
}}
{{end-eqn}}
As $\epsilon > 0$ was arbitrary, it follows from Real Plus Epsilon that:
:$\map {m^*} {A \cup B} \le \map {m^*} A + \map {m^*} B$
{{qed}}
Category:Outer Jordan Content
lh1dvvk6kdup09ggwkr68ii88zlwdon
Theorem: Jordan Content is Monotone

Let $A, B \subseteq \R^n$ be bounded subspaces of Euclidean $n$-space.
Suppose that $A \subseteq B$.
Further suppose that the Jordan content of both $A$ and $B$ exists.
Then:
:$\map m A \le \map m B$
where $m$ denotes the Jordan content.

Proof:
By definition of the Jordan content:
:$\map m A = \map {m^*} A$
:$\map m B = \map {m^*} B$
where $m^*$ denotes the outer Jordan content.
The result follows from Outer Jordan Content is Monotone.
{{qed}}
Category:Jordan Content
qssstvz29iq77ap9a1s53n4kcsaml15
Theorem: Set of Intersections with Superset is Cover

Let $S$ be a set.
Let $\CC$ be a cover of $S$.
Let $T \supseteq S$ be a superset of $S$.
Then:
:$\set {C \cap T : C \in \CC}$
is a cover of $S$.

Proof:
Let $x \in S$ be arbitrary.
By definition of cover, there is some $C \in \CC$ such that:
:$x \in C$
By definition of superset:
:$x \in T$
Therefore, by definition of intersection:
:$x \in C \cap T$
As $x \in S$ was arbitrary, the result follows.
{{qed}}
Category:Covers
Category:Set Intersection
srrtqp72vfb03dmcu68n0idngxtkb1d
Theorem: Inner Jordan Content is Well-Defined

Let $M \subseteq \R^n$ be a bounded subspace of Euclidean $n$-space.
Let:
{{begin-eqn}}
{{eqn | l = R
      | r = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i}
}}
{{eqn | l = R'
      | r = \prod_{i \mathop = 1}^n \closedint {a'_i} {b'_i}
}}
{{end-eqn}}
be closed $n$-rectangles that contain $M$.
Then:
:$\map V R - \map {m^*} {R \setminus M} = \map V {R'} - \map {m^*} {R' \setminus M}$
where $\map V R$ denotes the content of a rectangle.
Therefore, the inner Jordan content of $M$ is independent of the rectangle $R$ used to define it.

Proof:
{{WLOG}}, suppose that $R$ and $R'$ differ in only a single bound.
We will give the proof for the case where $a_k < a'_k$, and all other bounds are equivalent; the other cases are symmetric.
Under this assumption:
:$\ds R = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i}$
:$\ds R' = \prod_{i \mathop = 1}^{k - 1} \closedint {a_i} {b_i} \times \closedint {a'_k} {b_k} \times \prod_{i \mathop = k + 1}^n \closedint {a_i} {b_i}$
Let:
:$\ds r = \prod_{i \mathop = 1}^{k - 1} \openint {a_i} {b_i} \times \openint {a_k} {a'_k} \times \prod_{i \mathop = k + 1}^n \openint {a_i} {b_i}$
so that:
:$r \cap R' = \O$
Then, by Outer Jordan Content of Subdivision, taking all $a_i, b_i$ as well as $a'_k$ in the subdivision, we have:
:$\map {m^*} {R \setminus M} = \map {m^*} {r \cap \paren {R \setminus M}} + \map {m^*} {R'^\circ \cap \paren {R \setminus M}}$
Since $M \subseteq R'$ and $r \subseteq R$:
:$r \cap \paren {R \setminus M} = r$
and since $R'^\circ \subseteq R$:
:$R'^\circ \cap \paren {R \setminus M} = R'^\circ \setminus M$
Therefore:
:$\map {m^*} {R \setminus M} = \map {m^*} r + \map {m^*} {R'^\circ \setminus M}$
By Outer Jordan Content of Open Rectangle:
:$\ds \map {m^*} r = \paren {a'_i - a_i} \prod_{i \mathop \ne k} \paren {b_i - a_i}$
and so:
:$\map {m^*} r = \map V R - \map V {R'}$
Moreover, by Outer Jordan Content of Subdivision, taking $a_i, b_i$ except for $a_k$, as well as $a'_k$:
:$\map {m^*} {R' \setminus M} = \map {m^*} {R'^\circ \cap \paren {R' \setminus M}}$
in which:
:$R'^\circ \cap \paren {R' \setminus M} = R'^\circ \setminus M$
From the above, we determine:
:$\map {m^*} {R \setminus M} = \map V R - \map V {R'} + \map {m^*} {R' \setminus M}$
and the result follows.
{{qed}}
Category:Jordan Content
d6lgxa0l01a4meuj6jr2m8acc5xiwmk
Theorem: Euler Phi Function of 5

:$\map \phi 5 = 4$

Proof:
From Euler Phi Function of Prime:
:$\map \phi p = p - 1$
As $5$ is a prime number it follows that:
:$\map \phi 5 = 5 - 1 = 4$
{{qed}}
Category:Examples of Euler Phi Function
Category:5
aiv01ec8b4bv1w67p6ve471m97yt5fr
Theorem: Axes of Symmetry of Kappa Curve

Let $\KK$ be a kappa curve expressed in Cartesian coordinates as:
:$x^4 + x^2 y^2 = a^2 y^2$
$\KK$ has two axes of bilateral symmetry:
:the $x$-axis
:the $y$-axis.

Proof:
We have:
:$(1): \quad x^4 + x^2 y^2 = a^2 y^2$
;Symmetry about the $y$-axis
Substituting $-x$ for $x$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \paren {-x}^4 + \paren {-x}^2 y^2
      | r = x^4 + x^2 y^2
      | c = 
}}
{{eqn | r = a^2 y^2
      | c = 
}}
{{end-eqn}}
Thus if $\tuple {x, y}$ satisfies $(1)$, then $\tuple {-x, y}$ also satisfies $(1)$.
{{qed|lemma}}
;Symmetry about the $x$-axis
Substituting $-y$ for $y$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \paren x^4 + \paren x^2 \paren {-y}^2
      | r = x^4 + x^2 y^2
      | c = 
}}
{{eqn | r = a^2 y^2
      | c = 
}}
{{end-eqn}}
Thus if $\tuple {x, y}$ satisfies $(1)$, then $\tuple {x, -y}$ also satisfies $(1)$.
Therefore $\KK$ is invariant under the transformations:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \mapsto
      | r = \tuple {-x, y}
}}
{{eqn | l = \tuple {x, y}
      | o = \mapsto
      | r = \tuple {x, -y}
}}
{{end-eqn}}
so $\KK$ has bilateral symmetry about the $x$-axis and the $y$-axis.
{{qed}}
Theorem: Asymptotes of Kappa Curve

Let $\KK$ be a kappa curve expressed in Cartesian coordinates as:
:$x^4 + x^2 y^2 = a^2 y^2$
$\KK$ has two asymptotes:
:the line $x = a$
:the line $x = -a$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = x^4 + x^2 y^2
      | r = a^2 y^2
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = x^4
      | r = y^2 \paren {a^2 - x^2}
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = y^2
      | r = \dfrac {x^4} {a^2 - x^2}
      | c = dividing top and bottom by $a^2 - x^2$
}}
{{end-eqn}}
As $x \to a$, we have $a^2 - x^2 \to 0$ while $x^4 \to a^4 \ne 0$, so:
:$\ds \lim_{x \mathop \to a} y^2 \to \infty$
and therefore:
:$\ds \lim_{x \mathop \to a} \size y \to \infty$
Thus $\KK$ approaches the line $x = a$.
{{qed|lemma}}
Similarly, as $x \to -a$, we have $a^2 - x^2 \to 0$ while $x^4 \to a^4 \ne 0$, so again:
:$\ds \lim_{x \mathop \to -a} y^2 \to \infty$
and therefore:
:$\ds \lim_{x \mathop \to -a} \size y \to \infty$
Thus $\KK$ approaches the line $x = -a$.
{{qed|lemma}}
Therefore the kappa curve has asymptotes $x = a$ and $x = -a$.
{{qed}}
Theorem: Kappa Curve has Double Cusp at Origin

Let $\KK$ be a kappa curve expressed in Cartesian coordinates as:
:$x^4 + x^2 y^2 = a^2 y^2$
$\KK$ has a double cusp at the origin.
This double cusp is a double cusp of the first kind.

Proof:
We have {{hypothesis}} that $\KK$ is given by:
:$x^4 + x^2 y^2 = a^2 y^2$
Let us define the real-valued function $F: \R^2 \to \R$:
:$\forall \tuple {x, y} \in \R^2: \map F {x, y} = x^4 + x^2 y^2 - a^2 y^2$
We have:
:$\map F {0, 0} = 0$
so the origin lies on $\KK$.
Computing the partial derivatives of $F$ {{WRT}} $x$ and $y$, we get:
{{begin-eqn}}
{{eqn | l = \frac {\partial F} {\partial x}
      | r = 4 x^3 + 2 x y^2
}}
{{eqn | l = \frac {\partial F} {\partial y}
      | r = 2 x^2 y - 2 a^2 y
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \map {\frac {\partial F} {\partial x} } {0, 0}
      | r = 0
}}
{{eqn | l = \map {\frac {\partial F} {\partial y} } {0, 0}
      | r = 0
}}
{{end-eqn}}
so the origin is a singular point of $\KK$.
{{explain|How?}}
The lowest-degree nonzero homogeneous part of $F$ at $\tuple {0, 0}$ is:
:$-a^2 y^2$
{{explain|define the terminology of the above line: "lowest-degree nonzero homogeneous part"}}
which corresponds to the double line $y = 0$.
{{explain|What is a double line?}}
Hence the origin is a double cusp of the first kind.
{{explain|How have we proven first kind?}}
Moreover, from
:$x^4 = y^2 \paren {a^2 - x^2}$
we obtain, for $x^2 \ne a^2$:
:$y^2 = \dfrac {x^4} {a^2 - x^2}$
As $\tuple {x, y} \to \tuple {0, 0}$ we have:
:$a^2 - x^2 \to a^2$
so:
:$y^2 \sim \dfrac {x^4} {a^2}$
and therefore:
:$y \sim \pm \dfrac {x^2} a$
Thus near the origin $\KK$ consists of two branches meeting with common tangent $y = 0$.
That is, $\KK$ has a double cusp at the origin.
{{explain|We have already stated up above that we have proved the origin to be a double cusp of the first kind, so why did we need again to demonstrate that $\KK$ has a double cusp at the origin?}}
{{qed}}
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ is the rank function of a matroid on $S$.

Proof:
Let
:$X \in \mathscr I$
{{AimForCont}}
:$\exists Y \subseteq X : Y \notin \mathscr I$
Let:
:$Y_0 \subseteq X : \card {Y_0} = \max \set{\card Z : Z \subseteq X \land Z \notin \mathscr I}$
By definition of $\mathscr I$:
:$Y_0 \notin \mathscr I \leadsto \map \rho {Y_0} \ne \card {Y_0}$
From Lemma 2:
:$\map \rho {Y_0} < \card {Y_0}$
As $X \in \mathscr I$ then:
:$Y_0 \ne X$
Hence:
:$Y_0$ is a proper subset of $X$
From Set Difference with Proper Subset:
:$X \setminus Y_0 \ne \O$
Let $y \in X \setminus Y_0$.
We have:
{{begin-eqn}}
{{eqn | l = \card {Y_0} + 1
      | r = \card {Y_0 \cup \set y}
      | c = Corollary of Cardinality of Set Union
}}
{{eqn | r = \map \rho {Y_0 \cup \set y}
      | c = As $\card {Y_0} = \max \set{\card Z : Z \subseteq X \land Z \notin \mathscr I}$
}}
{{eqn | o = \le
      | r = \map \rho {Y_0} + 1
      | c = Rank axiom $(\text R 2)$
}}
{{eqn | o = <
      | r = \card {Y_0} + 1
      | c = As $\map \rho {Y_0} < \card {Y_0}$
}}
{{end-eqn}}
This is a contradiction.
So:
:$\forall Y \subseteq X : Y \in \mathscr I$
Hence:
:$M$ satisfies matroid axiom $(\text I 2)$.
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ is the rank function of a matroid on $S$.

Proof:
We prove the contrapositive statement:
:$\forall X, Y \subseteq S: Y \notin \mathscr I \land Y \subseteq X \implies X \notin \mathscr I$
Let $X, Y \subseteq S : Y \notin \mathscr I$ and $Y \subseteq X$.
====== Case 1: $Y = X$ ======
Let $Y = X$.
Then $X \notin \mathscr I$.
{{qed|lemma}}
====== Case 2: $Y \subset X$ ======
Let $Y \subset X$.
By definition of $\mathscr I$:
:$\map \rho Y \neq \size Y$
From Lemma 2:
:$\map \rho Y < \size Y$
Let:
:$X \setminus Y = \set{z_1, z_2, \ldots , z_k}$
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X
      | r = \map \rho {Y \cup \set{z_1, z_2, \ldots, z_k} }
}}
{{eqn | o = \le
      | r = \map \rho Y + k
      | c = Repeated application of rank axiom $(\text R 2)$
}}
{{eqn | o = <
      | r = \size Y + k
      | c = Lemma 2
}}
{{eqn | r = \size Y + \size {\set {z_1, z_2, \ldots, z_k} }
      | c = {{Defof|Cardinality of Finite Set}}
}}
{{eqn | r = \size {Y \cup \set {z_1, z_2, \ldots, z_k} }
      | c = Corollary of Cardinality of Set Union
}}
{{eqn | r = \size X
}}
{{end-eqn}}
It follows that $X \notin \mathscr I$.
{{qed|lemma}}
In either case we have:
:$X \notin \mathscr I$
This proves the contrapositive statement:
:$\forall X, Y \subseteq S: Y \notin \mathscr I \land Y \subseteq X \implies X \notin \mathscr I$
It follows that $\mathscr I$ satisfies matroid Axiom $(\text I 2)$.
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ is the rank function of a matroid on $S$.

Proof:
Let:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
It is to be shown that:
:* $\quad \mathscr I$ satisfies the matroid axioms
and
:* $\quad \rho$ is the rank function of the matroid $M = \struct{S, \mathscr I}$
==== Matroid Axioms ====
===== Matroid Axiom $(\text I 1)$ =====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 4}}{{qed|lemma}}
===== Matroid Axiom $(\text I 2)$ =====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5/Proof 1}}{{qed|lemma}}
===== Matroid Axiom $(\text I 3)$ =====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 6}}{{qed|lemma}}
==== $\rho$ is Rank Function ====
Let $\rho_M$ be the rank function of the matroid $M = \struct{S, \mathscr I}$.
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 8}}{{qed}}
Theorem: Formulation 1 Rank Axioms Implies Rank Function of Matroid

Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 1}}
Then $\rho$ is the rank function of a matroid on $S$.

Proof:
=== Lemma 1 ===
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 1}}
=== Lemma 2 ===
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 2}}
=== Lemma 3 ===
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 3}}
Let:
:$\mathscr I = \set{X \subseteq S : \map \rho X = \card X}$
It is to be shown that:
:* $\quad \mathscr I$ satisfies the matroid axioms
and
:* $\quad \rho$ is the rank function of the matroid $M = \struct{S, \mathscr I}$
=== Matroid Axioms ===
==== Matroid Axiom $(\text I 1)$ ====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5}}{{qed|lemma}}
==== Matroid Axiom $(\text I 2)$ ====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 5/Proof 2}}{{qed|lemma}}
==== Matroid Axiom $(\text I 4)$ ====
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 7}}{{qed|lemma}}
We have proven that $\mathscr I$ satisifies the matroid axioms.
It follows that $M = \struct{S, \mathscr I}$ is a matroid by definition.
=== $\rho$ is Rank Function ===
Let $\rho_M$ be the rank function of the matroid $M = \struct{S, \mathscr I}$.
{{:Formulation 1 Rank Axioms Implies Rank Function of Matroid/Lemma 8}}{{qed}}
Theorem: Rank Function of Matroid Satisfies Formulation 2 Rank Axioms

Let $S$ be a finite set.
Let $\rho$ is the rank function of a matroid $M = \struct{S, \mathscr I}$.
Then $\rho$ satisfies formulation 2 of the rank axioms:
{{:Axiom:Rank Axioms (Matroid)/Definition 2}}

Proof:
==== $\rho$ satisfies $(\text R 4)$ ====
This follows immediately from Bounds for Rank of Subset.
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 5)$ ====
This follows immediately from Rank Function is Increasing.
{{qed|lemma}}
==== $\rho$ satisfies $(\text R 6)$ ====
Let $X, Y \subseteq S$.
Let $A$ be a maximal independent subset of $X \cap Y$.
From Cardinality of Maximal Independent Subset Equals Rank of Set:
:$\card A = \map \rho {X \cap Y}$
From Independent Subset is Contained in Maximal Independent Subset:
:$\exists B \subseteq X \setminus Y : A \cup B$ is a maximal independent subset of $X$
Simiarly from Independent Subset is Contained in Maximal Independent Subset:
:$\exists C \subseteq Y \setminus X : \paren{A \cup B} \cup C$ is a maximal independent subset of $X \cup Y$
and:
:$\card{A \cup B \cup C} = \map \rho {X \cup Y}$
By matroid axiom $(\text I 2)$:
:$A \cup C$ is an independent subset of $Y$.
We have:
{{begin-eqn}}
{{eqn | l = \map \rho X + \map \rho Y
      | o = \ge
      | r = \card{A \cup B} + \card{A \cup C}
      | c = {{Defof|Rank Function (Matroid)|rank function}} $\rho$
}}
{{eqn | r = \card{A \cup B} + \paren{\card A + \card C }
      | c = {{Corollary|Cardinality of Set Union}}
}}
{{eqn | r = \paren{\card{A \cup B} + \card C } + \card A
      | c = Sum of Cardinals is Commutative and Sum of Cardinals is Associative
}}
{{eqn | r = \card{A \cup B \cup C} + \card A
      | c = {{Corollary|Cardinality of Set Union}}
}}
{{eqn | r = \map \rho {X \cup Y} + \map \rho {X \cap Y}
      | c = {{Defof|Rank Function (Matroid)|rank function}} $\rho$
}}
{{end-eqn}}