Nonstandard characterization of compactness I'm trying to write up notes for myself on nonstandard analysis, consulting outside resources as little as possible. I have stumbled upon what seems to be referred to as Robinson's characterization of compactness:
$X$ is compact iff $\forall z \in X^* \ \exists x \in X \ x \approx z$
(Here $X^*$ is the hyperreal extension of the set $X$, and $x \approx z$ means $x$ and $z$ differ by an infinitesimal amount)
I had no issues showing that nonstandard formulations of open, closed, and bounded sets were equivalent to standard definitions. From them it was straightforward to show that a set is compact in the nonstandard sense if and only if it is closed and bounded; then from Heine-Borel we get equivalence to compactness in the standard sense. This is fine, but I find it more satisfying to directly show that the nonstandard formulations are equivalent to the standard ones and only then use the nonstandard definitions to prove classic results. Part of the attraction for me of nonstandard analysis is the ease in which it can be used to prove some results, but it feels a bit like cheating if those results are then needed to show that the new definitions are correct.
I have been able to prove that if $X \subseteq \mathbb{R}$ is compact then it is compact in the nonstandard sense without using Heine-Borel: We start with some hyperreal number $z$ which is not infinitesimally close to any element of $X$. Then we take the set of all open intervals whose extensions do not contain $z$, which is an open covering of $X$ by choice of $z$. By compactness, this has a finite subcovering, $\{U_1, \dots, U_n\}$. By transfer, $\{U_1^*, \dots, U_n^*\}$ covers $X^*$ and so we can conclude that $z \not\in X^*$. The result follows by contraposition. Looking around a bit, this seems to be a common argument.
The issue is in trying to reverse this argument. I can't see how to make it work. The bit of notes I've seen reference a saturation assumption on the nonstandard model in order to prove the other direction. Unless I'm mistaken, the proof via Heine-Borel doesn't need this assumption so it shouldn't be necessary. I'd like to try to finish the proof as much as possible myself, but I'm totally stuck. I'd greatly appreciate a hint.
 A: Take a set $T \subseteq \mathbb{R}$ with an open cover $\mathcal{W}$ that has no finite subcover. I will construct an $h \in \!~^\star T$ that is not infinitesimally close to any element of $T$.
Notice that since $T$ is second-countable, $\mathcal{W}$ definitely has a countable subcover $\mathcal{V}$. Enumerate the countable subcover as $V_0, V_1, V_2, \dots $ and notice that for every $x \in T$ we can find some $n \in \mathbb{N}$ so that $x \in V_n$. However, since $\mathcal{V}$ has no finite subcover, $V_0 \cup V_1 \cup \dots \cup V_m$ always constitutes a proper subset of $T$ for every $m \in \mathbb{N}$.
This means that for all $n \in \mathbb{N}$ we can find a $y \in \mathbb{R}$ such that for all $m < n$, $y \not\in V_m$. By Transfer, the same holds for $\star$-extensions. In particular, picking your favorite hyperinteger $\omega \in \!~^\star \mathbb{N} \setminus \mathbb{N}$, you can find a $h \in \!\!~^\star \mathbb{R}$ such that for all $m < \omega$, $h \not\in \!\!~^\star V_m$. Consequently, $h \not\in \!\!~^\star V_n$ for any $n \in \mathbb{N}$.
If there was some $h' \in T$ infinitesimally close to $h$, then $h'$ would belong to one of the sets $V_n$, i.e. we'd have $h' \in \!\!~^\star V_n$ for some $n \in \mathbb{N}$. But $V_n$ is open, so then $h \in \!\!~^\star V_n$ would follow, a contradiction.
Taking contrapositives, we get that if every element of $\!~^\star T$ is infinitesimally close to some element of $T$, then every open cover of $T$ has a finite subcover.
A: $
\newcommand\ext[1]{{}^{*}\!#1}
\newcommand\std[1]{{}^\sigma\!#1}
\newcommand\Pfin{\mathcal P_{\mathrm{fin}}}
$
Nonstandard Analysis: Theory and Applications (1997) by Arkeryd, Cutland, and Henson, Proposition 7.4 (paraphrased):

*

*Assume a $\kappa$-saturated nonstandard extension. For any internal set $a$ and any (possibly external) $A \subseteq a$, if $|A| < \kappa$ then $A \subseteq b \subseteq a$ for some hyperfinite $b$.

In particular, what we want are for the standard elements of $a$ to be contained in a hyperfinite set; if this is true for all $a$, then the nonstandard extension is called an enlargement. In any case, the point is that in an extension which is saturated enough the following argument goes through.

Let $(X, T)$ be a topological space, and denote the nonstandard extension of e.g. $X$ by $\ext X$. We identity $X$ as a subset of $\ext X$. For any standard set $B$ and $A \subseteq \ext B$, we write
$$
  \std A = \{\ext x \;:\; \ext x \in A\text{ and }x \in B\},
$$
i.e. $\std A$ is the set of standard elements of $A$. The monad $\mu(x)$ of $x \in \ext X$ is
$$
  \mu(x) = \bigcap\{\ext U \;:\; U \in T\text{ and }x \in \ext U\},
$$
and we say $x \simeq y$ if $x \in \mu(y)$. Then $S \subseteq X$ is nonstandard compact if for all $x \in \ext S$ there is $y \in X$ such that $x \simeq y$, i.e. every element of $\ext S$ is nearstandard.
Now supposing $S \subseteq X$ is nonstandard compact, we wish that for every open cover $C$ of $S$ there is a finite subcover. Well, there is hyperfinite $H$ such that $\std C \subseteq H \subseteq \ext C$. If $x \in \ext S$, then by nonstandard compactness there is some $y \in S$ such that $x \simeq y$; but there is $c \in C$ such that $y \in c$, so $x \in \ext c \in \std C \subseteq H$. So $H$ covers $\ext S$. Thus
$$
  \exists H \in \ext\Pfin(C).\; \forall x \in \ext S.\; \exists h \in H.\; x \in h
$$
where $\Pfin(C)$ is the set of all finite subsets of $C$. By transfer,
$$
  \exists H' \in \Pfin(C).\; \forall x \in S.\; \exists h \in H.\; x \in h
$$
and $H'$ is a finite subcover of $C$.

The intuition behind this argument is sort of the following. Nonstandard compactness is a direct generalization of finiteness: a nonstandard set $A$ is finite iff
$$
  \forall x \in A.\; \exists y \in \std A.\; x = y,
$$
and it is nonstandard compact iff
$$
  \forall x \in A.\; \exists y \in \std A.\; x \simeq y.
$$
So in a sense if we "quotient" by $\simeq$, i.e. consider $\{\mu(y) \;:\; y \in \std A\}$, this set is "basically" finite and covers $A$; we just have to make a few adjustments to turn it into an internal set, and doing that we get $H$.
