Intersection of nested sequence of non-empty compact sets is non-empty (using sequential compactness) Let $(X,d)$ be a metric space, and let $K_1, K_2, K_3, \ldots$ be a sequence of non-empty compact sets in this metric space such that $$K_1 \supseteq K_2 \supseteq K_3 \supseteq \cdots$$ Then the intersection $\bigcap_{n=1}^\infty K_n$ is non-empty. I am aware of the standard proof of this fact using covering compactness, but I am wondering if there is a proof that uses instead sequential compactness.
My attempt is the following. Since each $K_n$ is non-empty, we can pick some point $x_n \in K_n$ for each $n$ (this requires the axiom of choice). Now consider the sequence $(x_n)_{n=1}^\infty$. By the nesting property, we have $x_n \in K_1$ for each $n$. Since $K_1$ is compact, this means there is a convergent subsequence $(x_{n_j})_{j=1}^\infty$ which converges to a point $p \in K_1$. We will now show that in fact $p \in K_n$ for each $n$, which would prove that $p \in \bigcap_{n=1}^\infty K_n$ (hence, the intersection is non-empty). Let $n$ be arbitrary. We have $n_j \geq j$ so if $j \geq n$ then $n_j \geq n$. By the nesting property, this means that $x_{n_j} \in K_n$ for all $j \geq n$. Thus $(x_{n_j})_{j=n}^\infty$ is a sequence of points in $K_n$ which converges to $p$. Since $K_n$ is compact, it is closed, so $p \in K_n$.
It seems to me that the proof goes through, but all the proofs I could find online used covering compactness, which made me nervous that somehow using sequential compactness here doesn't work. I would be curious to hear if the proof above goes through (and if not, whether there is another way to use sequential compactness).
 A: Your proof is indeed correct. As you noticed, it requires the axiom of choice, and that's perhaps the reason why it is avoided.
A: My short answer is that I believe your proof is correct. Once you have a sequence of points $y_i\in K_i$ which converges (which you have properly shown exists) you just note that this means the point $y$ to which it converges must be in $K_n$ for any $n$ you choose, by exactly the argument you gave. It's quite good.
A: For an alternate proof for those who come across this in the future (I know you mentioned you already have seen this proof):
Let $K_1 \supset K_2 \supset ...$ be compact non-empty subspaces of a metric space. Then they're all closed. And define open sets (in $K_1$ with respect to the subspace topology on $K_1$), for each $n \in \Bbb{Z}^+$,
$$U_n:=K_1 \setminus K_n.$$
Then
$$\bigcup_{n \in \Bbb{Z}^+}U_n = K_1 \setminus \bigcap_{n \in \Bbb{Z}^+} K_n$$
Let us suppose now toward a contradiction that the intersection is empty. Then $K_1 = \bigcup_{n \in \Bbb{Z}^+} U_n$. Then $\{U_n\}_{n \in \Bbb{Z}^+}$ is an open cover for $K_1$ which is compact and thus there exists some $k \in \Bbb{Z}^+$ such that
$$K_1 = \bigcup_{j=1}^k U_{n_j}.$$
As the $K_n$ are decreasing, the $U_n$ are increasing and one can define
$$M:= \max \{n_1,n_2,...,n_k\}.$$
Then as the $U_n$ are increasing it follows that
$$K_1 = \bigcup_{j=1}^kU_{n_j}=U_M.$$
But then
$$K_M = K_1 \setminus U_M=\emptyset.$$
This contradicts the $K_n$ being nonempty.
