Compact First-Countable Space is Sequentially Compact
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can 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: The axiom of choice is implicitly invoked above (discuss) You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by completing it. When this has been done, the template should be removed 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$
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 Proof Wiki by redesigning it.
To discuss this proof in more detail, feel free to use the talk page.
If you are able to fix this proof, then when you have done so you can remove this instance of {{Improve}} from the code.
If you would welcome a second opinion as to whether your improvement is correct, add an invitation to {{Proofread}} the page (see the proofread template for usage).
