Sequential compactness and filters I'm trying to work with the many equivalent definitions of compactness for a topological space $X$; in particular,



*Every (proper) filter on $X$ has a (proper) convergent refinement.


I'll be referring to this property as filter-compactness for convenience, and also because it looks very much like sequential compactness.
*Edit to include some other definitions here:

A filter on $X$ is said to be proper if it does not have the empty set as a member.
Let $X$ be a set and let $\mathcal{F}$ be a filter on $X$. If $\mathcal{G}$ is another filter on $X$ such that $\mathcal{F}$ is a subset of $\mathcal{G}$, then $\mathcal{G}$ is said to be a refinement of $\mathcal{F}$.
A filter $\mathcal{F}$ on a topological space $X$ is convergent if there exists $x \in X$ such that $\mathcal{F}$ refines the neighbourhood filter $N_x$ of $x$, which is defined by
$$ N_x = \{\, A \subseteq X \mid A \text{ contains an open neighbourhood of $x$ in $X$}\, \} $$

It is clear to me that filter-compactness and sequential compactness are equivalent for metric spaces because both are equivalent to open-set compactness. However, I'm hoping for a direct proof, since the two definitions seem so similar. Here's what I've managed:

Let $X$ be a metric space and suppose that $X$ is filter-compact. Let $(x_n)_{n \in \mathbb{N}}$ be a sequence in $X$, and let $\mathcal{F}$ denote the elementary filter associated with $(x_n)_{n \in \mathbb{N}}$, which is defined by
$$\mathcal{F} = \{\, A \subseteq X \mid A \text{ contains all but finitely many of the } x_n\, \}.$$
Since $X$ is filter-compact, there is a convergent refinement $\mathcal{G}$ of $\mathcal{F}$.

It'd be good if $\mathcal{G}$ were the elementary filter associated with some subsequence. But that doesn't seem to be true in general, considering refinements can be very large. I'm not able to get anything for the converse either.

Following notation used in Eric's answer:
Replace the sets $A_n \in \mathcal{G}$ by their closures in $X$. There exists $r > 0$ such that the open ball $B(x, r)$ is a subset of $A$. Since $d(A_n) \to 0$, we have $d(\bigcap_{k=1}^n A_k) \to 0$ as well. Thus there exists $N \in \mathbb{N}$ such that $d(\bigcap_{k=1}^N A_k) < r/2 < r \le d(A)$.
The set $B := \bigcap_{k=1}^N A_k$ is closed in $X$ and the tail sequence $(x_n)_{n \ge N}$ is contained in $B$, so the limit point $x$ belongs to $B$. It follows from $d(B) < r$ that we have $B \subseteq A$.
Finally, since $B$ is a member of $\mathcal{G}$, we have $A \in \mathcal{G}$ also. This suggests that $\mathcal{G}$ is convergent (to $x$), a contradiction.

 A: You are right that $\mathcal{G}$ need not be the filter associated with a subsequence, and in fact in need not even contain the filter associated with any convergent subsequence.  Instead you can just observe that if a refinement of $\mathcal{F}$ converges to a point $x$, then $x$ is an accumulation point of $\mathcal{F}$, meaning that every neighborhood of $x$ has nonempty intersection with every element of the filter $\mathcal{F}$.  When $\mathcal{F}$ is the elementary filter associated with a sequence $(x_n)$, that exactly means that $x$ is an accumulation point of the sequence in the usual sense.  So, in a metric space (or more generally a first-countable space), this implies some subsequence of $(x_n)$ converges to $x$.
The converse is harder, since it essentially amounts to proving that sequential compactness implies compactness for metric spaces (the implication from filter-compactness to compactness is just trivial definition-wrangling).  Here's one way to do it.  Suppose a filter $\mathcal{F}$ on a metric space $X$ has no convergent refinement.  If $X$ is not complete, it is obviously not sequentially compact (take any Cauchy sequence that does not converge, and it cannot have any convergent subsequence).
So, we may assume $X$ is complete.  Now let us take a look at our filter $\mathcal{F}$.  Suppose $\mathcal{F}$ has a refinement $\mathcal{G}$ such that the diameters of elements of $\mathcal{G}$ get arbitrarily close to $0$.  Choose sets $A_n\in G$ such that $\operatorname{diam}(A_n)\to 0$, and choose $x_n\in\bigcap_{m=1}^n A_m$ for each $n$.  Then $(x_n)$ is Cauchy and so converges to some $x\in X$.  But now it is easy to see that every neighborhood of $x$ contains $A_n$ for some $n$.  That means $\mathcal{G}$ converges to $x$, which is a contradiction.
So, no refinement of $\mathcal{F}$ contains elements of arbitrarily small diameter.  Now let $\mathcal{G}$ be an ultrafilter refining $\mathcal{F}$.  In particular, this means that given any finite collection of sets $A_1,\dots,A_n$ with $A_1\cup\dots\cup A_n=X$, some $A_i$ must be in $\mathcal{G}$.  In particular, if $X$ can be covered by finitely many sets of diameter $\leq\epsilon$, then $\mathcal{G}$ must contain a set of diameter $\leq\epsilon$.  So, for some $\epsilon>0$, $X$ cannot be covered by finitely many sets of diameter $\epsilon$.  We can now choose a sequence $(x_n)$ such that $d(x_m,x_n)\geq\epsilon/2$ for all $m\neq n$: having chosen $x_1,\dots,x_{n-1}$, the balls of radius $\epsilon/2$ around $x_1,\dots,x_{n-1}$ cannot cover $X$, so we can choose $x_n$ to be some point which is not in any of them.  It is clear that no subsequence of $(x_n)$ can converge, so $X$ is not sequentially compact.
