Is a sequentially compact (non-metrizable) uniform space totally bounded? First some topological definitions in terms of nets and sequences:
A topological space $(X, \tau)$ is


*

*compact iff every net has a convergent subnet

*sequentially compact iff every sequence has a convergent subsequence


A uniform space $(X, \mathcal{U})$ is


*

*totally bounded iff every net has a Cauchy subnet

*complete iff every Cauchy net converges

*sequentially complete iff every Cauchy sequence converges


If $(X, \mathcal{U})$ is a uniform space and $\tau$ its induced topology then
it is known that $(X, \tau)$ is compact iff $(X, \mathcal{U})$ is totally bounded and complete.
I found in "Topological Uniform Structures" by Warren Page on p. 44, Example 6.2 the statement: "A sequentially compact uniform space is sequentially complete and totally bounded".
Questions:


*

*Is this statement true?

*Is this statement true if $(X, \mathcal{U})$ is the uniform space corresponding to a topological vector space $(X, \tau)$?


I don't think that total boundedness is implied by sequential compactness (how should one argue about nets if one has only information about sequences, e.g. in the open ordinal $[0, \omega_1)$?). The statement should be rather of the form "A sequentially compact uniform space is sequentially complete and sequentially totally bounded"
where $(X, \mathcal{U})$ is sequentially totally bounded should be defined as "every sequence has a Cauchy subsequence".
Remarks:


*

*If $(X, \tau)$ is metrizable then the statement is true since compactness is equivalent to sequential compactness. (It also holds if $X$ is a Banach space equipped with its non-metrizable weak topology by Eberlein-Smulian.)

*It seems to me that the notion of "sequential total boundedness" is not common in the literature. In ncatlab this notion is referred to as "sequential precompactness".
 A: Suppose that $(X,\mathcal{U})$ is sequentially compact. So there exists some $N \in \mathcal{U}$ (some entourage) such that $X$ cannot be covered by finitely many $B(x,N)$. So pick $x_0 \in X$, note that $B(x_0, N)$ does not cover $X$ so there is some $x_1 \notin B(x_0,N)$. By recursion, if we have constructed points $x_0,\ldots, x_n$ then we find some $x_{n+1}$ that is not in $\cup_{i=0}^n B(x_i, N)$, as the latter cannot cover $X$. 
This sequence $(x_n)$ we constructed this way has a convergent subsequence, by sequential compactness, so $x_{n_k} \rightarrow p$, for some $p \in X$. Then pick some entourage $N'$ such that $N' \circ N' \subseteq N$, then $B(p,N')$ contains a tail of the subsequence, so some $x_{n_{k_1}}, x_{n_{k_2}}, k_1 < k_2$ such that $x_{n_{k_1}}, x_{n_{k_2}} \in B(p,N')$ which implies that $x_{n_{k_2}} \in B(x_{n_{k_1}}, N)$, contradicting how we chose the sequence. 
So a sequentially compact (or even limit point compact) uniform space is totally bounded. It's certainly sequentially complete (as a convergent subsequence is certainly Cauchy..). 
Added I thought we needed an equivalence, so I wrote
For the converse (a try!) suppose we have a totally bounded and sequentially complete space $(X,\mathcal{U})$. If we have some sequence $(x_n)$, then suppose it has no convergent subsequence (striving for a contradiction), or we can even assume it has no Cauchy subsequence, using sequential completeness. This means that for every subsequence of our sequence there is some entourage $N$ such that infinitely many members of that subsequence are not $N$-close. I think that starting with the complete sequence and the above $N$, find $N'$, an entourage in $\mathcal{U}$, with $N' \circ N' \subseteq N$, and total  boundedness gives us a finite cover by finitely many $N'$-balls, we have a subsequence that lives in one of the balls, and which are (by how $N'$ is chosen) $N$-close. This subsequence has its own entourage $N^(1)$ as above, and we can continue recursively again. But I don't see how to conclude this line of reasoning with a final contradiction, though. We get thinner and thinner and closer and closer subsequences, but we have no first countability or some such property to exploit. 
So left to right I see but right to left not yet. Maybe someone has ideas?
Added Is there an easy counterexample for the reverse ($\omega_1$ isn't one, maybe some other countably compact and sequentially compact but non-compact space, like a $\Sigma$-product? 
