avewright/proofwiki-math huggingface dataset:
Theorem: Equality of Ordered Pairs/Necessary Condition

Let $\tuple {a, b}$ and $\tuple {c, d}$ be ordered pairs such that $\tuple {a, b} = \tuple {c, d}$.
Then $a = c$ and $b = d$.

Proof:
First a lemma:
{{:Equality of Ordered Pairs/Lemma}}{{qed|lemma}}
Let $\tuple {a, b} = \tuple {c, d}$.
From the Wiener formalization:
:$\set {\set {\O, \set a}, \set {\set b} } = \set {\set {\O, \set c}, \set {\set d} }$
Let $x \in \set {\set {\O, \set a}, \set {\set b} }$.
Then either:
:$x = \set {\O, \set a}$
or:
:$x = \set {\set b}$
First suppose $x = \set {\O, \set a}$.
Then:
:$x = \set {\O, \set c}$ or $x = \set {\set d}$
{{AimForCont}} $x = \set {\set d}$.
That is:
:$\set {\O, \set a} = \set {\set d}$
Then:
:$\set d = \set a$
and also:
:$\set d = \O$
But that means:
:$a \in \O$
which contradicts the definition of the empty set $\O$.
It follows by Proof by Contradiction that $x \ne \set {\set d}$.
Thus $x = \set {\O, \set c}$.
We have that:
:$x = \set {\O, \set a}$ and $x = \set {\O, \set c}$
and so:
:$\set {\O, \set a} = \set {\O, \set c}$
It follows from the lemma that:
:$\set a = \set c$
Hence from Singleton Equality:
:$a = c$
Now suppose $x = \set {\set b}$.
Then:
:$x = \set {\O, \set c}$ or $x = \set {\set d}$
{{AimForCont}} $x = \set {\O, \set c}$.
That is:
:$\set {\set b} = \set {\O, \set c}$
which means that $\set b = \O$ and $\set b = \set c$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\O, \set c}$.
Thus $x = \set {\set d}$.
We have that:
:$x = \set {\set b}$ and $x = \set {\set d}$
By Singleton Equality:
:$\set b = \set d$
and again by Singleton Equality:
:$b = d$
{{qed}}
Theorem: Equality of Ordered Pairs/Sufficient Condition

Let $\tuple {a, b}$ and $\tuple {c, d}$ be ordered pairs.
Let $a = c$ and $b = d$.
Then:
:$\tuple {a, b} = \tuple {c, d}$

Proof:
Suppose $a = c$ and $b = d$.
Then:
:$\set a = \set c$
and:
:$\set {a, b} = \set {c, d}$
Thus:
:$\set {\set a, \set {a, b} } = \set {\set c, \set {c, d} }$
and so by the Kuratowski formalization:
:$\tuple {a, b} = \tuple {c, d}$
{{qed}}
Theorem: Intersection of Class Exists and is Unique

Let $V$ be a basic universe.
Let $A \subseteq V$ be a class.
Let $\bigcap A$ denote the intersection of $A$.
Then $\bigcap A$ is guaranteed to exist and is unique.

Proof:
By the Axiom of Specification we can create the subclass of $V$:
:$\bigcap A = \set {x \in V: \forall y \in A: x \in y}$
Hence $\bigcap A$ exists.
Suppose $\QQ \subseteq V$ such that $\QQ$ and $\bigcap A$ are both the intersection of $A$.
Then:
:$\QQ = \set {x \in V: \forall y \in A: x \in y}$
Thus:
:$x \in \QQ \implies x \in \bigcap A$
and:
:$x \in \bigcap A \implies x \in \QQ$
Hence by the Axiom of Extension:
:$\QQ = \bigcap A$
and uniqueness has been demonstrated.
{{qed}}
Theorem: Intersection of Non-Empty Class is Set

Let $A$ be a non-empty class.
Let $\bigcap A$ denote the intersection of $A$.
Then $\bigcap A$ is a set.

Proof:
Let $V$ denote the basic universe such that $A \subseteq V$.
We are given that $A$ is non-empty.
Then $\exists x \in A$ where $x$ is a set.
By definition of intersection of class, every element of $\bigcap A$ is an element of all elements of $A$.
Thus:
:$\bigcap A \subseteq x$
We are given that $A$ is a subclass of the basic universe $V$.
Thus $x \in V$ by definition of basic universe.
By the {{axiom-link|Swelledness}}, $V$ is a swelled class.
By definition of swelled class, every subclass of a set $x \in V$ is a set.
It follows $\bigcap A$ is a set.
{{Qed}}
Theorem: Intersection of Non-Empty Class is Set

Let $A$ be a non-empty class.
Let $\bigcap A$ denote the intersection of $A$.
Then $\bigcap A$ is a set.

Proof:
Since $A$ is a non-empty class, there exists $S \in A$.
Since $S$ is an element of a class, it is not a proper class, and is thus a set.
By definition of class intersection:
:$x \in \bigcap A \implies x \in S$
By the subclass definition:
:$\bigcap A \subseteq S$
By Subclass of Set is Set, $\bigcap A$ is a set.
{{qed}}
Theorem: Intersection of Empty Set/Class Theory

Let $V$ be a basic universe.
Let $\O$ denote the empty class.
Then the intersection of $\O$ is $V$:
:$\bigcap \O = V$

Proof:
By definition of $V$, we have:
:$\bigcap \O \subseteq V$
By definition of empty class, there exists no set $x \in V$ which is an element of $\O$.
Hence it is vacuously true that every element of $V$ is an element of every element of $\O$.
Therefore every $x \in V$ is an element of $\bigcap \O$.
Therefore:
:$V \subseteq \bigcap \O$
It follows by definition of class equality that:
:$\bigcap \O = V$
{{qed}}
Theorem: Union of Subclass is Subclass of Union of Class

Let $A$ and $B$ be classes.
Let $\bigcup A$ and $\bigcup B$ denote the union of $A$ and union of $B$ respectively.
Let $A$ be a subclass of $B$:
:$A \subseteq B$
Then $\bigcup A$ is a subclass of $\bigcup B$:
:$\bigcup A \subseteq \bigcup B$

Proof:
Let $x \in \bigcup A$.
Then:
:$\exists y \in A: x \in y$
But as $A \subseteq B$ it follows that $y \in B$.
That is:
:$\exists y \in B: x \in y$
That is:
:$x \in \bigcup B$
Hence the result by definition of subclass.
{{Qed}}
Theorem: Intersection of Class is Subset of Intersection of Subclass

Let $V$ be a basic universe.
Let $A$ and $B$ be classes of $V$:
:$A \subseteq V, B \subseteq V$
such that it is not the case that $A = B = \O$.
Let $\bigcap A$ and $\bigcap B$ denote the intersection of $A$ and intersection of $B$ respectively.
Let $A$ be a subclass of $B$:
:$A \subseteq B$
Then $\bigcap B$ is a subset of $\bigcap A$:
:$\bigcap B \subseteq \bigcap A$

Proof:
First we consider the degenerate case where $A = B = \O$.
By Intersection of Empty Class we have that:
:$\bigcap \O = V$
Thus we have:
:$\bigcap B = \bigcap A = V$
and neither $\bigcap B$ nor $\bigcap A$ are in fact sets.
So while in this case $\bigcap B \subseteq \bigcap A$, $\bigcap B$ is a subclass of $\bigcap A$ and not actually a subset.
{{qed|lemma}}
Next we cover the case where $A = \O$ is the empty class.
It is noted that Empty Class is Subclass of All Classes, and so $A \subseteq B$.
By Intersection of Empty Class we have that:
:$\bigcap A = V$
and so by definition of basic universe $\bigcap B \subseteq V$.
By Intersection of Non-Empty Class is Set, $\bigcap B$ is a set.
By definition of basic universe:
:$\bigcap B \in V$
By the {{axiom-link|Transitivity}}, $V$ is transitive.
Hence as $\bigcap B \in V$ it follows that:
:$\bigcap B \subseteq V$
and the result holds.
{{qed|lemma}}
By Intersection of Non-Empty Class is Set, both $\bigcap A$ and $\bigcap B$ are sets.
Let $x \in \bigcap B$.
Then:
:$\forall y \in B: x \in y$
That is:
:$y \in B \implies x \in y$
But as $A \subseteq B$, we have that:
:$y \in A \implies y \in B$
and therefore:
:$y \in A \implies x \in y$
That is:
:$\forall y \in A: x \in y$
and so by definition of intersection:
:$x \in \bigcap A$
Hence the result by definition of subset.
{{Qed}}
Theorem: Union of Transitive Class is Subclass

Let $A$ be a transitive class.
Let $\bigcup A$ denote the union of $A$.
Then:
:$\bigcup A \subseteq A$

Proof:
Let $A$ be transitive.
Let $x \in \bigcup A$.
Then by definition:
:$\exists y \in A: x \in y$
By definition of transitive class:
:$x \in y \land y \in A \implies x \in A$
and so:
:$x \in A$
Hence the result by definition of subclass.
Theorem: Union of Class is Subclass implies Class is Transitive

Let $A$ be a class.
Let $\bigcup A$ denote the union of $A$.
Let:
:$\bigcup A \subseteq A$
Then $A$ is transitive.

Proof:
Let $\bigcup A \subseteq A$.
Let $x \in \bigcup A$.
Then by definition:
:$\exists y \in A: x \in y$
By definition of subclass:
:$x \in A$
Thus we have that:
:$x \in y \land y \in A \implies x \in A$
It follows by definition that $A$ is a transitive class.
Theorem: Union of Transitive Class is Transitive

Let $A$ be a class.
Let $\bigcup A$ denote the union of $A$.
Let $A$ be transitive.
Then $\bigcup A$ is also transitive.

Proof:
Let $A$ be transitive.
By Class is Transitive iff Union is Subclass:
:$\bigcup A \subseteq A$
By Union of Subclass is Subclass of Union of Class:
:$\map \bigcup {\bigcup A} \subseteq \bigcup A$
Then by Class is Transitive iff Union is Subclass:
:$\bigcup A$ is transitive.
{{qed}}
Theorem: Union of Transitive Class is Transitive

Let $A$ be a class.
Let $\bigcup A$ denote the union of $A$.
Let $A$ be transitive.
Then $\bigcup A$ is also transitive.

Proof:
Let $A$ be transitive.
Let $x \in \bigcup A$.
By Class is Transitive iff Union is Subclass we have that:
:$\bigcup A \subseteq A$
Thus by definition of subclass:
:$x \in A$
As $A$ is transitive:
:$x \subseteq A$
Let $z \in x$.
As $x \subseteq A$, it follows by definition of subclass that:
:$z \in A$
Thus we have that:
:$\exists x \in A: z \in x$
and so by definition of union of class:
:$z \in \bigcup A$
Thus we have that:
:$z \in x \implies z \in \bigcup A$
and so by definition of subclass:
:$x \subseteq \bigcup A$
Thus we have that:
:$x \in \bigcup A \implies x \subseteq \bigcup A$
Hence $\bigcup A$ is a transitive class by definition.
{{qed}}
Theorem: Union of Class is Transitive if Every Element is Transitive

Let $A$ be a class.
Let $\bigcup A$ denote the union of $A$.
Let $A$ be such that every element of $A$ is transitive.
Then $\bigcup A$ is also transitive.

Proof:
Let $A$ be such that every $y \in A$ is transitive.
Let $x \in \bigcup A$.
Then $x$ is an element of some element $y$ of $A$.
We have {{hypothesis}} that $y$ is transitive.
Hence, by definition of transitive class:
:$x \subseteq y$
Because $y \in A$, by definition of union of class:
:$y \subseteq \bigcup A$
So:
:$x \subseteq \bigcup A$
As this is true for all $x \in A$, it follows by definition that $\bigcup A$ is transitive.
{{qed}}
Theorem: Set Difference with Set Difference is Union of Set Difference with Intersection/Corollary

:$T \setminus \paren {S \setminus T} = T$

Proof:
From Set Difference with Set Difference is Union of Set Difference with Intersection:
:$R \setminus \paren {S \setminus T} = \paren {R \setminus S} \cup \paren {R \cap T}$
where $R, S, T$ are sets.
Hence:
{{begin-eqn}}
{{eqn | l = T \setminus \paren {S \setminus T}
      | r = \paren {T \setminus S} \cup \paren {T \cap T}
      | c = Set Difference with Set Difference is Union of Set Difference with Intersection
}}
{{eqn | r = \paren {T \setminus S} \cup T
      | c = Set Intersection is Idempotent
}}
{{eqn | r = T
      | c = Set Difference Union First Set is First Set
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Set Union
Category:Set Difference with Set Difference is Union of Set Difference with Intersection
c91i05wxolxkcrt24u9atyj7ws80hye
Theorem: Power Set Exists and is Unique

Let $V$ be a basic universe.
Let $x \in V$ be a set.
Let $\powerset x$ denote the power set of $x$.
Then $\powerset x$ is guaranteed to exist and is unique.

Proof:
By the {{axiom-link|Specification|Classes}} an arbitrary subclass of $x$ can be created.
Hence we can create the class of all such subclasses.
Hence $\powerset x$ exists.
Let $\powerset x$, $\map \QQ x$ both be power sets of $x$.
From definition of power sets:
:$\forall T$:
::$T \in \powerset x \iff T \subseteq x$
::$T \in \map \QQ x \iff T \subseteq x$
From Biconditional is Commutative and Biconditional is Transitive:
:$T \in \powerset x \iff T \in \map \QQ x$
By the {{axiom-link|Extension|Classes}}:
:$\powerset x = \map \QQ x$
Hence the power set is unique.
{{qed}}
Theorem: Element of Class is Subset of Union of Class

Let $A$ be a class.
Let $\ds \bigcup A$ denote the union of $A$.
Let $x \in A$.
Then:
:$x \subseteq \ds \bigcup A$

Proof:
Let $x \in A$.
By definition of class, $x$ is a set.
Let $y \in x$.
By definition of union of $A$:
:$\ds \bigcup A := \set {y: \exists x \in A: y \in x}$
It follows directly from that definition that:
:$y \in \ds \bigcup A$
The result follows by definition of subset.
{{qed}}
Category:Class Union
acmtwijny3dxqouvgoomb8vmgonkoje
Theorem: Set is Subset of Power Set of Union

Let $x$ be a set of sets.
Let $\bigcup x$ denote the union of $x$.
Let $\powerset {\bigcup x}$ denote the power set of $\bigcup x$.
Then:
:$x \subseteq \powerset {\bigcup x}$

Proof:
Let $z \in x$.
By Element of Class is Subset of Union of Class:
:$z \subseteq \bigcup x$
By definition of power set:
:$z \in \powerset {\bigcup x}$
The result follows by definition of subset.
{{qed}}
Theorem: Set equals Union of Power Set

Let $x$ be a set of sets.
Let $\powerset x$ denote the power set of $x$.
Let $\map \bigcup {\powerset x}$ denote the union of $\powerset x$.
Then:
:$x = \map \bigcup {\powerset x}$

Proof:
From Set is Element of its Power Set:
:$x \in \powerset x$
From Element of Class is Subset of Union of Class it follows that:
:$x \subseteq \map \bigcup {\powerset x}$
{{qed|lemma}}
Let $z \in \map \bigcup {\powerset x}$
Then by definition of unionunion:
:$\exists y \in \powerset x: z \in y$
By definition of $\powerset x$
:$\exists y \subseteq x: z \in y$
But by definition of subset, that means:
:$z \in x$
Thus, again by definition of subset:
:$\map \bigcup {\powerset x} \subseteq x$
{{qed|lemma}}
We have that:
:$x \subseteq \map \bigcup {\powerset x}$
and:
:$\map \bigcup {\powerset x} \subseteq x$
Hence by definition of set equality:
:$x = \map \bigcup {\powerset x}$
{{qed}}
Theorem: Cartesian Product Exists and is Unique

Let $A$ and $B$ be classes.
Let $A \times B$ be the '''cartesian product''' of $A$ and $B$.
Then $A \times B$ exists and is unique.

Proof:
Let $A \times B$ be the cartesian product of $A$ and $B$.
Let $\tuple {x, y} \in A \times B$ such that $\tuple {x, y}$ satisfies the Kuratowski ordered pair formulation.
By Binary Cartesian Product in Kuratowski Formalization contained in Power Set of Power Set of Union:
:$A \times B \subseteq \powerset {\powerset {A \cup B} }$
By Axiom of Specification, there exists a set:
:$C = \set {\tuple {x, y} \in \powerset {\powerset {A \cup B} }: x \in A \land y \in B}$
By definition, $C$ is the cartesian product of $A$ and $B$.
Thus $A \times B$ exists.
By Cartesian Product is Unique, $A \times B$ is unique.
{{qed}}
Theorem: Cartesian Product of Sets is Set

Let $V$ be a basic universe.
Let $A$ and $B$ be sets in $V$.
Then their cartesian product $A \times B$ is also a set.

Proof:
Let $A$ and $B$ be sets in $V$.
Because $V$ is a basic universe, the basic universe axioms apply.
Hence by the axiom of pairing $\set {A, B}$ is a set.
Then by the axiom of unions $\bigcup \set {A, B}$ is also a set.
We have that $A \cup B = \bigcup \set {A, B}$.
By the axiom of powers $\powerset {A \cup B}$ is a set.
Therefore, also by the axiom of powers, so is $\powerset {\powerset {A \cup B} }$.
It remains to be shown that $A \times B$ is a subclass of $\powerset {\powerset {A \cup B} }$.
Let $x \in A \times B$.
Then:
:$x = \tuple {a, b}$
for some $a \in A$ and $b \in B$.
By definition of ordered pair:
:$x = \set {\set a, \set {a, b} }$
From Set is Subset of Union:
:$A \subseteq A \cup B$ and $B \subseteq A \cup B$
Hence by definition of subset:
:$a \in A \cup B$
and:
:$b \in A \cup B$
Thus:
:$\set a \subseteq A \cup B$
and:
:$\set {a, b} \subseteq A \cup B$
Thus by definition of power set:
:$\set a \in \powerset {A \cup B}$
and:
:$\set {a, b} \in \powerset {A \cup B}$
Hence:
:$\set {\set a, \set {a, b} } \subseteq \powerset {A \cup B}$
That is:
:$\tuple {a, b} \subseteq \powerset {A \cup B}$
and so:
:$x \subseteq \powerset {A \cup B}$
which means:
:$x \in \powerset {\powerset {A \cup B} }$
Hence by definition of subclass:
:$A \times B \subseteq \powerset {\powerset {A \cup B} }$
We have that $\powerset {\powerset {A \cup B} }$ is a set.
By the {{axiom-link|Swelledness}} it follows that $A \times B$ is also a set.
{{Qed}}
Theorem: Jordan Curve Theorem/General Result

Let $M$ be a connected manifold of dimension $n - 1$ without boundary.
Let $M$ be embedded in Euclidean space $\R^n$.
Then $M$ divides $\R^n$ into an inside and an outside.

Proof:
{{proof wanted}}
{{Namedfor|Marie Ennemond Camille Jordan}}
Theorem: Real Function with Positive Derivative is Increasing

Let:
:$\forall x \in \openint a b: \map {f'} x \ge 0$
Then $f$ is increasing on $\closedint a b$.

Proof:
Let $c, d \in \closedint a b$ such that $c < d$.
Then $f$ satisfies the conditions of the Mean Value Theorem on $\closedint c d$.
Hence:
:$\exists \xi \in \openint c d: \map {f'} \xi = \dfrac {\map f d - \map f c} {d - c}$
Let $f$ be such that:
:$\forall x \in \openint a b: \map {f'} x \ge 0$
Then:
:$\map {f'} \xi \ge 0$
and hence:
:$\map f d \ge \map f c$
Thus $f$ is increasing on $\closedint a b$.
{{qed}}
Theorem: Real Function with Strictly Positive Derivative is Strictly Increasing

Let:
:$\forall x \in \openint a b: \map {f'} x > 0$
Then $f$ is strictly increasing on $\closedint a b$.

Proof:
Let $c, d \in \closedint a b$ such that $c < d$.
Then $f$ satisfies the conditions of the Mean Value Theorem on $\closedint c d$.
Hence:
:$\exists \xi \in \openint c d: \map {f'} \xi = \dfrac {\map f d - \map f c} {d - c}$
Let $f$ be such that:
:$\forall x \in \openint a b: \map {f'} x > 0$
Then:
:$\map {f'} \xi > 0$
and hence:
:$\map f d > \map f c$
Thus $f$ is strictly increasing on $\closedint a b$.
{{qed}}
Theorem: Real Function with Strictly Negative Derivative is Strictly Decreasing

Let:
:$\forall x \in \openint a b: \map {f'} x < 0$
Then $f$ is strictly decreasing on $\closedint a b$.

Proof:
Let $c, d \in \closedint a b$ such that $c < d$.
Then $f$ satisfies the conditions of the Mean Value Theorem on $\closedint c d$.
Hence:
:$\exists \xi \in \openint c d: \map {f'} \xi = \dfrac {\map f d - \map f c} {d - c}$
Let $f$ be such that:
:$\forall x \in \openint a b: \map {f'} x < 0$
Then:
:$\map {f'} \xi < 0$
and hence:
:$\map f d < \map f c$
Thus $f$ is strictly decreasing on $\closedint a b$.
{{qed}}
Theorem: Real Function with Negative Derivative is Decreasing

Let:
:$\forall x \in \openint a b: \map {f'} x \le 0$
Then $f$ is decreasing on $\closedint a b$.

Proof:
Let $c, d \in \closedint a b$ such that $c < d$.
Then $f$ satisfies the conditions of the Mean Value Theorem on $\closedint c d$.
Hence:
:$\exists \xi \in \openint c d: \map {f'} \xi = \dfrac {\map f d - \map f c} {d - c}$
Let $f$ be such that:
:$\forall x \in \openint a b: \map {f'} x \le 0$
Then:
:$\map {f'} \xi \le 0$
and hence:
:$\map f d \le \map f c$
Thus $f$ is decreasing on $\closedint a b$.
{{qed}}
Theorem: Limit with Rational Epsilon and Delta

Let $\openint a b$ be an open real interval.
Let $c \in \openint a b$.
Let $f: \openint a b \setminus \set c \to \R$ be a real function.
Let $L \in \R$.
Suppose that:
:$\forall \epsilon > 0 \in \Q_{>0}: \exists \delta \in \Q_{>0}: \forall x \in \R: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < \epsilon$
Then the limit of $f$ exists as $x$ tends to $c$, and is equal to $L$.

Proof:
Recall the definition of a limit of a real function:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall x \in \R: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < \epsilon$
Denote by $\map P {\epsilon,\delta}$ the proposition that the above statement holds.
Suppose that $\map P {\epsilon,\delta}$ holds for all rational $\epsilon$ in the interval of interest:
:$\forall \epsilon \in \Q_{>0}: \exists \delta \in \Q_{>0}: \forall x \in \R: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < \epsilon$
Let $\epsilon_0 > 0$ be a real number.
From Between two Real Numbers exists Rational Number, there is some rational $\epsilon_0'$ such that $0 < \epsilon_0' < \epsilon_0$.
Then $\size {\map f x - L} < \epsilon_0'$ implies $\size {\map f x - L} < \epsilon_0$.
Thus $\map P {\epsilon,\delta}$ holding for all rational $\epsilon$ implies $\map P {\epsilon,\delta}$ for all real $\epsilon$.
Now suppose $\map P {\epsilon,\delta}$ has been established for some rational $\epsilon$ and some real $\delta_0$.
From Between two Real Numbers exists Rational Number, there is some rational $\delta_0'$ such that $\size {x-c} < \delta_0' < \delta_0$.
Then $\size {x-c} < \delta_0$ is implied by $\size {x-c} < \delta_0'$
This means $\map P {\epsilon,\delta_0'}$ implies $\map P {\epsilon,\delta_0}$ holds.
We conclude:
:$\map P {\epsilon,\delta}$ holds for all rational $\epsilon$ and $\delta$ in the interval of interest
is a stronger statement than:
:$\map P {\epsilon,\delta}$ holds for all real $\epsilon$ and $\delta$ in the interval of interest.
{{qed}}
Theorem: Limit with Epsilon Powers of 2

Let $\openint a b$ be an open real interval.
Let $c \in \openint a b$.
Let $f: \openint a b \setminus \set c \to \R$ be a real function.
Let $L \in \R$.
Suppose that:
:$\forall n > 0 \in \N: \exists \delta \in \R_{>0}: \forall x \in \R: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < 2^{-n} $
Then the limit of $f$ exists as $x$ tends to $c$, and is equal to $L$.

Proof:
Denote by $\map P {2^{-n},\delta}$ the proposition considered in the theorem exposition:
:$\forall \in \N: \exists \delta \in \R_{>0}: \forall x \in \R: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < 2^{-n} $
Let the limit of $f$ as $x \to c$ exist and equal $L$, as described in the definition of limit:
:$\forall \epsilon \in \R_{>0}: \exists \delta \in \R_{>0}: \forall x \in \R: 0 < \size {x - c} < \delta \implies \size {\map f x - L} < \epsilon$.
Denote by $\map P {\epsilon,\delta}$ the proposition that the above statement holds.
From the Axiom of Archimedes:
:$\forall \epsilon > 0: \exists n \in \N: n > \dfrac 1 \epsilon$.
As $2^n > n$ for all $n$, we have that $2^n > \dfrac 1 \epsilon$.
By Ordering of Reciprocals, $2^{-n} < \epsilon$.
Therefore $\size {\map f x - L} < \epsilon$ is implied by $\size {\map f x - L} < 2^{-n}$.
Thus $\map P {\epsilon,\delta}$ is a weaker statement $\map P {2^{-n},\delta}$ 
{{qed}}
Theorem: Characterization of Probability Density Function

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X: \Omega \to \R$ be a continuous random variable on $\struct {\Omega, \Sigma, \Pr}$.
Let $\Omega_X = \Img X$, the image of $X$.
Let the '''probability density function''' of $X$ is the mapping $f_X: \R \to \closedint 0 1$ be defined as:
:$\forall x \in \R: \map {f_X} x = \begin {cases}
\ds \lim_{\epsilon \mathop \to 0^+} \frac {\map \Pr {x - \frac \epsilon 2 \le X \le x + \frac \epsilon 2} } \epsilon & : x \in \Omega_X \\
0 & : x \notin \Omega_X
\end {cases}$
Suppose that the cumulative distribution function of $X$ defines a continuously differentiable real function $F_X: x \mapsto \map \Pr {X \le x}$.
Then the '''probability density function''' of $X$ is the mapping $f_X: \R \to \closedint 0 1$ satisfies:
:$\dfrac \d {\d x} \map {F_X} x = \map {f_X} x$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \Pr {x - \frac \epsilon 2 \le X \le x + \frac \epsilon 2}
      | r = \map {F_X} {x + \frac \epsilon 2} - \map {F_X} {x - \frac \epsilon 2} + \map \Pr {X = x -\frac \epsilon 2}
}}
{{eqn | r = \map {F_X} {x + \frac \epsilon 2} - \map {F_X} {x - \frac \epsilon 2}   
      | c = Probability of Continuous Random Variable at Single Point is Zero
}}
{{eqn | ll= \leadsto
      | l = \map {f_X} x
      | r = \lim_{\epsilon \mathop \to 0^+} \frac {\map {F_x} {x + \frac \epsilon 2} - \map {F_x} {x - \frac \epsilon 2} } \epsilon
}}
{{eqn | r = \dfrac \d {\d x} \map {F_X} x
      | c = Continuous Derivative as Average of One-Sided Derivatives
}}
{{end-eqn}}
{{qed}}
{{MissingLinks}}