Compact First-Countable Space is Sequentially Compact

This article needs to be linked to other articles. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

Theorem

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$.

Aiming for a contradiction, suppose 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$.

Work In Progress In particular: The axiom of choice is implicitly invoked above You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{WIP}} from the code.

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$.

$\blacksquare$

Although this article appears correct, it's inelegant. There has to be a better way of doing it. In particular: To prove this in ZF, one could simply use Compact Space is Countably Compact and Countably Compact First-Countable Space is Sequentially Compact. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Improve}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.