avewright/proofwiki-math huggingface dataset:
Theorem: Real Numbers are Uncountably Infinite

The set of real numbers $\R$ is uncountably infinite.

Proof:
By Surjection from Natural Numbers iff Countable, a set $A$ is countable {{iff}} there exists a surjection $f: \N \to A$.
Suppose there exists a surjection $f: \N \to \R$.
Then $\forall x \in \R: \exists n \in \N: \map f n = x$ as $f$ is surjective.
Let $d_{n, 0}$ be the integer before the decimal point of $\map f n$.
Similarly, for all $m > 0$, let $d_{n, m}$ be the $m$th digit in the decimal expansion of $\map f n$.
Let $e_0$ be an integer different from $d_{0, 0}$.
Similarly, for all $m > 0$, let $e_m$ be an integer different from $d_{m, m}$.
Specifically, we can define $e_0$ to be $d_{0, 0} + 1$, and:
:$e_m = \begin {cases} 1 & : d_{m, m} \ne 1 \\ 2 & : d_{m, m} = 1 \end {cases}$
Now consider the real number $\ds x = e_0 + \sum_{n \mathop = 1}^\infty \frac {e_n} {10^n}$.
Its decimal expansion is:
:$x = \sqbrk {e_0 . e_1 e_2 e_3 \ldots}_{10}$
Since $e_0 \ne d_{0, 0}$, $x \ne \map f 0$.
Similarly, for each $n \in \N$ such that $n \ge 1$, we have that $e_n \ne d_{n, n}$ and so $x \ne \map f n$.
Thus $x$ is a real number which is not in the set $\set {\map f n: n \in \N}$.
Hence $f$ can not be surjective.
{{qed}}
Theorem: Real Numbers are Uncountably Infinite

The set of real numbers $\R$ is uncountably infinite.

Proof:
By Cantor's Theorem there is no surjection:
:$\N \twoheadrightarrow \powerset \N$
Additionally, we have Power Set of Natural Numbers is not Countable.
Therefore, if we can show that $\powerset \N$ injects into $\R$ then there is no injection $\R \hookrightarrow \N$ and $\R$ is uncountable.
To prove the theorem we construct an injection $f: \powerset \N \to \R$.
For a subset $S \subseteq \N$, let $\chi_S$ be the characteristic function of $S$, and let $d_i = \map {\chi_S} i$ for all $i \in \N$.
By the definition of characteristic function, $\sequence {d_i}_{i \mathop \in \N}$ is an infinite sequence of $1$s and $0$s.
There are two cases: $\sequence {d_i}_{i \mathop \in \N}$ terminates in an infinite sequence of $1$s, or it does not.
Suppose $\sequence {d_i}_{i \mathop \in \N}$ does ''not'' terminate in an infinite sequence of $1$s.
Then $\map f S$ is the binary expansion of the following number in $\hointr 0 1$:
:$0.d_1 d_2 d_3 d_4 \ldots$
Otherwise $\sequence {d_i}_{i \mathop \in \N}$ ''does'' terminate in an infinite sequence of $1$s.
Then $\map f S$ is the integer expressed in binary as:
:$1 d_1 d_2 d_3 \ldots d_k$
where $d_k$ is the last member of the sequence not equal to $1$.
In either case, every subset of $\N$, that is, element of $\powerset \N$, is mapped to an element of $\R$.
That $f$ is an injection follows from the uniqueness statement of Existence of Base-N Representation.
{{qed}}
Theorem: Condition for Point being in Closure

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.
Let $H^-$ denote the closure of $H$ in $T$.
Let $x \in S$.
Then $x \in H^-$ {{iff}} every open neighborhood of $x$ contains a point in $H$.

Proof:
From the definition of closure, we have that $H^-$ is the union of $H$ and all the limit points of $H$ in $T$.
By definition, an open neighborhood of $x$ in $T$ is an open set of $T$ which contains $x$.
=== Necessary Condition ===
Let $x \in H^-$.
Then either:
:$(1): \quad x \in H$, in which case every open neighborhood of $x$ in $T$ trivially contains a point in $H$ (that is, $x$ itself);
:$(2): \quad x$ is a limit point of $H$ in $T$.
Suppose $(2)$ holds.
Then it follows directly from the definition of limit point that every open neighborhood of $x$ in $T$ contains a point in $H$ other than $x$.
=== Sufficient Condition ===
Suppose that every open neighborhood of $x$ in $T$ contains a point in $H$.
If $x \in H$, then $x$ is in the union of $H$ and all the limit points of $H$ in $T$.
Hence by definition of closure:
:$x \in H^-$
If $x \notin H$ then $x$ must be a limit point of $H$ by definition.
So again, $x$ is in the union of $H$ and all the limit points of $H$ in $T$.
Hence by definition of closure:
:$x \in H^-$
{{qed}}
Theorem: Condition for Point being in Closure

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.
Let $H^-$ denote the closure of $H$ in $T$.
Let $x \in S$.
Then $x \in H^-$ {{iff}} every open neighborhood of $x$ contains a point in $H$.

Proof:
The condition to be proved is equivalent to showing that $x \in H^-$ {{iff}}, for every open neighborhood $U$ of $x$, the intersection $H \cap U$ is non-empty.
For $U \in \tau$, let $U^{\complement}$ denote the relative complement of $U$ in $S$.
By definition, $U^{\complement}$ is closed in $T$
We have that:
{{begin-eqn}}
{{eqn | l = H \cap U
      | r = \O
}}
{{eqn | ll= \leadstoandfrom
      | l = H
      | o = \subseteq
      | r = U^{\complement}
      | c = Empty Intersection iff Subset of Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = H^-
      | o = \subseteq
      | r = U^{\complement}
      | c = Set Closure is Smallest Closed Set in Topological Space
}}
{{eqn | ll= \leadstoandfrom
      | l = U
      | o = \subseteq
      | r = \paren {H^-}^{\complement}
      | c = Relative Complement inverts Subsets and Relative Complement of Relative Complement
}}
{{eqn | ll= \leadstoandfrom
      | l = H^- \cap U
      | o = =
      | r = \O
      | c = 
}}
{{end-eqn}}
Thus:
:$x \in U \iff x \notin H^-$
The result follows from the Rule of Transposition.
{{qed}}
Theorem: Topological Closure of Subset is Subset of Topological Closure

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq K$ and $K \subseteq S$.
Then:
:$\map \cl H \subseteq \map \cl K$
where $\map \cl H$ denotes the closure of $H$.

Proof:
From Topological Closure is Closed, $\map \cl K$ is closed.
From Set is Subset of its Topological Closure:
:$K \subseteq \map \cl K$
By Subset Relation is Transitive, it follows that:
:$H \subseteq \map \cl K$
Hence, by definition of closure as the smallest closed set that contains $H$:
:$\map \cl H \subseteq \map \cl K$
{{qed}}
Theorem: Topological Closure of Subset is Subset of Topological Closure

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq K$ and $K \subseteq S$.
Then:
:$\map \cl H \subseteq \map \cl K$
where $\map \cl H$ denotes the closure of $H$.

Proof:
From the definition of closure:
:$\map \cl H$ is the union of $H$ and its limit points.
Let $x \in \map \cl H$.
If $x \in H$ then $x \in K \implies x \in \map \cl K$.
Otherwise $x$ is a limit point of $H$.
That is, every open set $U$ of $T$ such that $x \in U$ contains $y \in H$ such that $y \ne x$.
But as $y \in H$ it follows that $y \in K$.
So every open set $U$ of $T$ such that $x \in U$ contains $y \in K$ such that $y \ne x$.
This is the definition for a limit point of $K$.
Thus $x \in \map \cl K$.
{{ExtractTheorem|Extract the above paragraph into something like "Limit Point of Subset is Limit Point" (which proves that $H \subseteq K \implies H' \subseteq K'$). Then use Set Union Preserves Subsets to prove this result.}}
{{qed}}
Theorem: Closure of Topological Closure equals Closure

Let $T$ be a topological space.
Let $H \subseteq T$.
Then:
:$\map \cl {\map \cl H} = \map \cl H$
where $\cl$ denotes the closure of $H$.

Proof:
It follows directly from Set is Subset of its Topological Closure that:
:$\map \cl H \subseteq \map \cl {\map \cl H}$
{{qed|lemma}}
Let $x \in \map \cl {\map \cl H}$.
Then from Condition for Point being in Closure, any $U$ which is open in $T$ such that $x \in U$ contains some $y \in \map \cl H$.
If we consider $U$ as an open set containing $y$, it follows that:
:$U \cap H \ne \O$
Hence $x \in \map \cl H$.
Hence by definition of subset:
:$\map \cl {\map \cl H} \subseteq \map \cl H$
{{qed|lemma}}
Hence the result by definition of set equality.
{{qed}}
Theorem: Topological Closure is Closed

Let $T$ be a topological space.
Let $H \subseteq T$.
Then the closure $\map \cl H$ of $H$ is closed in $T$.

Proof:
From Closure of Topological Closure equals Closure:
:$\map \cl {\map \cl H} = \map \cl H$
From Set is Closed iff Equals Topological Closure, it follows that $\map \cl H$ is closed.
{{qed}}
Theorem: Equivalence of Definitions of Closure of Topological Subspace

{{TFAE|def = Closure (Topology)|view = closure|context = Topology (Mathematical Branch)|contextview = topology}}
Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.

Proof:
=== Definition $1$ is equivalent to Definition $2$ ===
This is proved in Set Closure as Intersection of Closed Sets.
{{qed|lemma}}
Theorem: Closure of Intersection is Subset of Intersection of Closures

Let $T$ be a topological space.
Let $I$ be an indexing set.
Let $\forall i \in I: H_i \subseteq T$.
Then:
:$\ds \map \cl {\bigcap_I H_i} \subseteq \bigcap_I \map \cl {H_i}$
where $\map \cl {H_i}$ denotes the closure of $H_i$.

Proof:
Since $\ds \bigcap_I \map \cl {H_i}$ is an intersection of closed sets, it is closed, from Topology Defined by Closed Sets.
Also, it contains $\ds \bigcap_I H_i$ and so by the main definition of closure also contains $\ds \map \cl {\bigcap_I H_i}$.
{{qed}}
Theorem: Closure of Finite Union equals Union of Closures

Let $T$ be a topological space.
Let $n \in \N$.
Let:
:$\forall i \in \set {1, 2, \ldots, n}: H_i \subseteq T$
Then:
:$\ds \bigcup_{i \mathop = 1}^n \map \cl {H_i} = \map \cl {\bigcup_{i \mathop = 1}^n H_i}$
where $\map \cl {H_i}$ denotes the closure of $H_i$.

Proof:
From Closure of Union contains Union of Closures we have that:
:$\ds \bigcup_{i \mathop = 1}^n \map \cl {H_i} \subseteq \map \cl {\bigcup_{i \mathop = 1}^n H_i}$
We need now to show that: 
:$\ds \bigcup_{i \mathop = 1}^n \map \cl {H_i} \supseteq \map \cl {\bigcup_{i \mathop = 1}^n H_i}$
Let $\ds K = \bigcup_{i \mathop = 1}^n \map \cl {H_i}$ and $\ds H = \bigcup_{i \mathop = 1}^n H_i$.
From Topological Closure is Closed, all of $\map \cl {H_i}$ are closed.
So $K$ is the union of a finite number of closed sets.
So $K$ is itself closed, from Topology Defined by Closed Sets.
From Set is Subset of its Topological Closure:
:$\forall i \in \closedint 1 n: H_i \subseteq \map \cl {H_i}$
and so $H \subseteq K$.
So from Topological Closure of Subset is Subset of Topological Closure:
:$\map \cl H \subseteq \map \cl K$
The result follows.
{{qed}}
Theorem: Compact First-Countable Space is Sequentially Compact

Let $T = \struct {S, \tau}$ be a compact first-countable topological space.
Then every infinite sequence in $S$ has a convergent subsequence; that is, $T$ is sequentially compact.

Proof:
Let $\sequence {x_n}_{n \mathop \in \N}$ be an infinite sequence in $S$.
{{AimForCont}} that $\sequence {x_n}_{n \mathop \in \N}$ does not have a convergent subsequence.
By Accumulation Point of Infinite Sequence in First-Countable Space is Subsequential Limit, it follows that $\sequence {x_n}_{n \mathop \in \N}$ does not have an accumulation point in $S$.
Thus, for each $x \in S$, we can select an open set $U_x$ such that $x \in U_x$ and $U_x$ only contains $x_n$ for finitely many $n \in \N$.
The set $\UU = \set {U_x : x \in X}$ is clearly an open cover for $S$.
{{wtd|The axiom of choice is implicitly invoked above}}
By the definition of a compact space, there exists a finite subcover $\set {U_{x_1}, U_{x_2}, \ldots, U_{x_m} }$ of $\UU$ for $X$.
Then $U_{x_1} \cup U_{x_2} \cup \cdots \cup U_{x_m}$ contains all of $S$ since it is a cover.
However, each open set in this union only contains $x_n$ for a finite number of $n$, and this is a finite union of sets.
So the union only contains $x_n$ for finitely many $n$.
This implies that $x_n \in X$ for only finitely many $n \in \N$.
This is a contradiction, since $\sequence {x_n}$ is a sequence in $S$, and so $x_n \in S$ for all $n \in \N$.
{{qed}}
{{Improve|To prove this in ZF, one could simply use Compact Space is Countably Compact and Countably Compact First-Countable Space is Sequentially Compact.}}
Category:First-Countable Spaces
Category:Compact Topological Spaces
Category:Sequentially Compact Spaces
5cuyftyerk6e494vk6cntjgyut4cf5j
Theorem: Compact First-Countable Space is Sequentially Compact

Let $T = \struct {S, \tau}$ be a compact first-countable topological space.
Then every infinite sequence in $S$ has a convergent subsequence; that is, $T$ is sequentially compact.

Proof:
Follows directly from:
: Infinite Sequence in Countably Compact Space has Accumulation Point
: Accumulation Point of Infinite Sequence in First-Countable Space is Subsequential Limit
{{qed}}
Theorem: Compact First-Countable Space is Sequentially Compact

Let $T = \struct {S, \tau}$ be a compact first-countable topological space.
Then every infinite sequence in $S$ has a convergent subsequence; that is, $T$ is sequentially compact.

Proof:
Let $T = \struct {S, \tau}$ be a countably compact first-countable topological space.
By definition of sequentially compact, it is sufficient to show that every infinite sequence in $S$ has a convergent subsequence.
Let $\sequence {s_n}$ be any sequence in $S$.
By Infinite Sequence in Countably Compact Space has Accumulation Point, $\sequence {s_n}$ has an accumulation point $p \in S$.
As $T$ is first-countable, $p$ has a countable local basis, say:
:$\set {V_n: V_1 \supseteq V_2 \supseteq V_3 \supseteq \cdots}$
Then a subsequence $\sequence {s_{n_i} }$, where $s_{n_i} \in V_i$, converges to $p$.
{{handwaving|This last statement is "by intimidation"; justification needed}}
{{qed}}
Theorem: Closure of Open Ball in Metric Space

Let $M = \struct {A, d}$ be a metric space.
Let $\map {B_\epsilon} x$ be an open $\epsilon$-ball in $M$.
Let $y \in \map \cl {\map {B_\epsilon} x}$, where $\cl$ denotes the closure of $\map {B_\epsilon} x$.
Then $\map d {x, y} \le \epsilon$.

Proof:
Suppose $\map d {x, y} > \epsilon$.
Then $\map {B_{\map d {x, y} - \epsilon} } y$ is an open set containing $y$ and not meeting $\map {B_\epsilon} x$.
Hence:
:$y \notin \map \cl {\map {B_\epsilon} x}$
{{qed}}
Theorem: Nowhere Dense iff Complement of Closure is Everywhere Dense

Let $T = \struct {S, \tau}$ be a topological space.
Let $H \subseteq S$.
Then $H$ is nowhere dense in $T$ {{iff}} $S \setminus H^-$ is everywhere dense in $T$, where $H^-$ denotes the closure of $H$.
=== Corollary ===
{{:Nowhere Dense iff Complement of Closure is Everywhere Dense/Corollary}}

Proof:
Let:
:$H^\circ$ denote the interior of any $H \subseteq S$
:$H^-$ denote the closure of any $H \subseteq S$.
From the definition, $H$ is nowhere dense in $T$ {{iff}} $\paren {H^-}^\circ = \O$.
From the definition of interior, it follows that $\paren {H^-}^\circ = \O$ {{iff}} every open set of $T$ contains a point of $S \setminus \paren {H^-}$.
Thus $S \setminus \paren {H^-}$ is everywhere dense by definition.
{{qed}}
Theorem: Convergence in Indiscrete Space

Let $\struct {S, \set {S, \O} }$ be an indiscrete space.
Let $\sequence {x_n}$ be any sequence in $S$.
Then $\sequence {x_n}$ converges to any point $x$ of $S$.

Proof:
For any open set $U \subseteq S$ such that $x \in U$, we must have $U = S$.
Hence:
:$\forall n \ge 1: x_n \in U$
The result follows from the definition of a convergent sequence in a topological space.
{{qed}}
Theorem: Totally Bounded Metric Space is Separable

A totally bounded metric space is separable.

Proof:
Let $M = \struct {A, d}$ be a totally bounded metric space.
By the definition of total boundedness, we can use the axiom of countable choice to construct a sequence $\sequence {F_n}_{n \mathop \ge 1}$ such that:
:For all natural numbers $n \ge 1$, $F_n$ is a finite $\paren {1/n}$-net for $M$.
Let $\ds S = \bigcup_{n \mathop \ge 1} F_n$.
From Countable Union of Countable Sets is Countable, it follows that $S$ is countable.
It suffices to prove that $S$ is everywhere dense in $M$.
Let $S^-$ denote the closure of $S$.
Let $x \in X$.
Let $U \subseteq X$ be open in $M$ such that $x \in U$.
By definition, there exists a strictly positive real number $\epsilon$ such that $\map {B_\epsilon} x \subseteq U$.
That is, the open $\epsilon$-ball of $x$ in $M$ is contained in $U$.
By the Axiom of Archimedes, there exists a natural number $n > \dfrac 1 \epsilon$.
That is, $\dfrac 1 n < \epsilon$, and so $\map {B_{1 / n} } x \subseteq \map {B_\epsilon} x$.
Since $\subseteq$ is a transitive relation, we have $\map {B_{1/n} } x \subseteq U$.
By the definition of a net, there exists a $y \in F_n$ such that $x \in \map {B_{1/n} } y$.
By {{Metric-space-axiom|3}}, it follows from the definition of an open ball that $y \in \map {B_{1/n} } x$.
Since $y \in S \cap U$, it follows that $x$ is an adherent point of $S$.
By definition of adherent point:
:$x \in S^-$
That is:
:$X \subseteq S^-$
and so $S$ is everywhere dense in $M$.
{{qed}}
{{ACC}}
Category:Separable Spaces
Category:Totally Bounded Metric Spaces
m9hyl8msv5s0bxz2hlora30jaickbsp
Theorem: Convergent Sequence in T2 Space has Unique Limit

Let $T = \struct {S, \tau}$ be a $T_2$ (Hausdorff) space.
Let $\sequence {x_n}$ be a convergent sequence in $T$.
Then $\sequence {x_n}$ has exactly one limit.

Proof:
From the definition of convergent sequence, we have that $\sequence {x_n}$ converges to at least one limit.
{{AimForCont}} $l$ and $m$ are both limits of $\sequence{x_n}$.
As $T$ is a $T_2$ (Hausdorff) space, there exist $U, V \in \tau$ such that:
:$l \in U, m \in V$ and $U \cap V = \O$
Then, from the definition of convergent sequence:
{{begin-eqn}}
{{eqn | q = \exists N_U \in \R
      | l = n > N_U
      | o = \implies
      | r = x_n \in U
}}
{{eqn | q= \exists N_V \in \R
      | l = n > N_V
      | o = \implies
      | r = x_n \in V
}}
{{end-eqn}}
Taking $N = \max \set {N_U, N_V}$ we then have:
:$\exists N \in \R: n > N \implies x_n \in U, x_n \in V$
But $U \cap V = \O$.
From that contradiction we can see that there can be no such two distinct $l$ and $m$.
Hence the result.
{{qed}}
Theorem: Metric Space is T2

A metric space $M = \struct {A, d}$ is a $T_2$ (Hausdorff) space.

Proof:
Let $x, y \in A: x \ne y$.
Then from Distinct Points in Metric Space have Disjoint Open Balls, there exist open $\epsilon$-balls $\map {B_\epsilon} x$ and $\map {B_\epsilon} y$ which are disjoint open sets containing $x$ and $y$ respectively.
Hence the result by the definition of $T_2$ (Hausdorff) space.
{{qed}}
Theorem: Metric Space is T2

A metric space $M = \struct {A, d}$ is a $T_2$ (Hausdorff) space.

Proof:
{{AimForCont}} $M$ is not Hausdorff.
That is, there are $x, y \in A: x \ne y$ such that:
:$\forall \epsilon \in \R_{>0}: \exists z \in \map {B_\epsilon} x \cap \map {B_\epsilon} y$
where $\map {B_\epsilon} x$ denote the open $\epsilon$-ball of $x$ in $M$.
Let $r = \dfrac {\map d {x, y} } 2$.
Let $z \in \map {B_r} x \cap \map {B_r} y$.
Then:
{{begin-eqn}}
{{eqn | l = z
      | o = \in
      | r = \map {B_r} x \cap \map {B_r} y
}}
{{eqn | ll= \leadsto
      | l = z
      | o = \in
      | r = \map {B_r} x
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land
      | l = z
      | o = \in
      | r = \map {B_r} y
}}
{{eqn | ll= \leadsto
      | l = \map d {x, z}
      | o = <
      | r = r
      | c = {{Defof|Open Ball}}
}}
{{eqn | lo= \land
      | l = \map d {y, z}
      | o = <
      | r = r
}}
{{eqn | ll= \leadsto
      | l = \map d {x, z} + \map d {y, z}
      | o = <
      | r = 2 r
}}
{{eqn | ll= \leadsto
      | l = \map d {x, z} + \map d {y, z}
      | o = <
      | r = \map d {x, y}
}}
{{end-eqn}}
This contradicts {{Metric-space-axiom|2}}.
Thus, $M$ has to be Hausdorff.
{{qed}}
Theorem: Convergent Real Sequence has Unique Limit

Let $\sequence {s_n}$ be a real sequence.
Then $\sequence {s_n}$ can have at most one limit.

Proof:
{{AimForCont}} that $\sequence {s_n}$ converges to $l$ and also to $m$.
That is, suppose that:
:$\ds \lim_{n \mathop \to \infty} x_n = l$
and:
:$\ds \lim_{n \mathop \to \infty} x_n = m$
{{WLOG}}, assume that $l \ne m$.
Let:
:$\epsilon = \dfrac {\size {l - m} } 2$
As $l \ne m$, it follows that $\epsilon > 0$.
As $\sequence {s_n} \to l$:
:$\exists N_1 \in \N: \forall n \in \N: n > N_1: \size {s_n - l} < \epsilon$
Similarly, since $\sequence {s_n} \to m$:
:$\exists N_2 \in \N: \forall n \in \N: n > N_2: \size {s_n - m} < \epsilon$
Now set $N = \max \set {N_1, N_2}$.
We have:
{{begin-eqn}}
{{eqn | l = \size {l - m}
      | r = \size {l - s_N + s_N - m}
      | c = 
}}
{{eqn | o = \le
      | r = \size {l - s_N} + \size {s_N - m}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = <
      | r = 2 \epsilon
      | c = 
}}
{{eqn | r = \size {l - m}
      | c = 
}}
{{end-eqn}}
This constitutes a contradiction.
It follows from Proof by Contradiction that $l = m$.
{{qed}}
Theorem: Convergent Real Sequence has Unique Limit

Let $\sequence {s_n}$ be a real sequence.
Then $\sequence {s_n}$ can have at most one limit.

Proof:
We have that the real number line is a metric space
The result then follows from Convergent Sequence in Metric Space has Unique Limit.
{{qed}}
Theorem: Distinct Points in Metric Space have Disjoint Open Balls

Let $M = \struct {A, d}$ be a metric space.
Let $x, y \in M: x \ne y$.
Then there exist disjoint open $\epsilon$-balls $\map {B_\epsilon} x$ and $\map {B_\epsilon} y$ containing $x$ and $y$ respectively.

Proof:
Let $x, y \in A: x \ne y$.
Then $\map d {x, y} > 0$.
Put $\epsilon = \dfrac {\map d {x, y} } 2$.
Let $\map {B_\epsilon} x$ and $\map {B_\epsilon} y$ be the open $\epsilon$-balls of $x$ and $y$ respectively.
Suppose $\map {B_\epsilon} x$ and $\map {B_\epsilon} y$ are not disjoint.
Then $\exists z \in M$ such that $z \in \map {B_\epsilon} x$ and $z \in \map {B_\epsilon} y$.
Then $\map d {x, z} < \epsilon$ and $\map d {z, y} < \epsilon$.
Hence $\map d {x, z} + \map d {z, y} < 2 \epsilon = \map d {x, y}$.
This contradicts the definition of a metric, so there can be no such $z$.
Hence the open balls must be disjoint.
{{qed}}
Theorem: Sequentially Compact Metric Space is Lindelöf

Let $M = \struct {X, d}$ be a sequentially compact metric space.
Then $M$ is also a Lindelöf space.
That is, from every open cover of $M$, it is possible to extract a countable subcover.

Proof:
Take any open cover $C$ of $M$.
We need to find a countable subset of $C$ which still covers $X$.
We have that a Sequentially Compact Metric Space is Second-Countable.
Thus, by definition, the topology of $M$ has a countable basis.
Let $\BB$ be a countable basis for the topology induced by $d$ of $M$.
Let $x \in X$.
As $C$ covers $X$:
:$\exists U_x \in C: x \in U_x$
As $\BB$ is a basis:
:$\exists B_x \in \BB: x \in B_x \subseteq U_x$
Thus:
:$(1): \quad \forall x \in X: \exists B_x \in \BB: x \in B_x$
Consider the set $\Sigma := \set {B_x: x \in X}$.
$\Sigma$ is a subset of $\BB$.
Hence $\Sigma$ is countable.
As $\Sigma$ contains every $x \in X$ from $(1)$, $\Sigma$ covers $X$.
By construction of $\Sigma$, every open set in $\Sigma$ is contained in some $U \in C$.
For each open set $B \in \Sigma$, choose one $U_B \in C$ such that $B \subseteq U_B$.
{{explain|Does this need AoC or ACC?}}
Let $\UU$ be the set defined as:
:$\UU = \set {U_B: B \in \Sigma}$
As $\UU$ does not have more sets than $\Sigma$, $\UU$ is countable.
We have that:
:$\forall B \in \Sigma: B \subseteq U_B$
Thus it follows that $\UU$ covers $X$.
As:
:$\forall U_B \in \UU: U_B \in C$
$U$ is a countable subcover of $C$.
Thus a countable subcover has been obtained from $C$.
As $C$ is arbitrary, it follows that $M$ is a Lindelöf space.
{{qed}}