Can someone formalize 'compactness of set' defined as follows?

Question

My text book says

A set K ⊆ R is compact if every sequence in K has a subsequence that converges to a limit that is also in K.

Wondering how to formalize this statement, my trial was this.

($\forall$$a_n$$\in K$) ($\forall$$\epsilon$>0)($\exists$M$\in$N)($\forall$k≥M) |$a_{n_k}$ - $\alpha$ | < $\epsilon$ & $\alpha$ $\in$ K

But, I'm not confident of quantifying sequence.

So, what is an adequate formalization?

Answer 1

To rewrite the condition in text, for all sequences in K, there exists a subsequence, with limit in K. In symbols that's $\forall (a_n) \in K, \exists (i_n), \lim a_{i_n} \in K$ and that's all. You may also want to expand what $\lim \in K$ means. This is the usual $\exists \alpha \in K, \forall \varepsilon, \exists N, \forall n > N, |a_{i_n}-\alpha| < \varepsilon$.

The nice thing about maths is that it's all plug and play. You can start writing the definition of compactness using high level concepts such as a limit. You can later replace the limit with its definition just by renaming the variables it uses.

Answer 2

Conventions. I am experimenting with writing my arrows backwards. Also, write $\omega$ for the least infinite ordinal number. So $\omega = \{0,1,2,3,4,\ldots\}.$ Furthermore, write $f \restriction I$ to denote the restriction of $f$ to $I$. With these conventions in place, a rigorous definition of compactness of subsets of $\mathbb{R}$ can be given as follows.

Definition. Consider $X \subseteq \mathbb{R}$. Then $X$ is compact iff for all functions $f : X \leftarrow \omega,$ there exists $I \subseteq \omega$ such that the following hold.

1. $I$ is cofinal.
2. There exists $x \in X$ such that the sequence $f \restriction I$ converges to $x$.