precompact space

Precompact spaces


A precompact space is one whose completion is compact. This makes sense for uniform spaces (and more generally for Cauchy spaces) but not for topological spaces.

There is an alternative definition, apparently having nothing to do with completion of compactness, but equivalent (at least in classical mathematics). When necessary to distinguish this, we may call this alternative a totally bounded space.

Precompact subsets (using the induced uniformity?) are one of the useful types of subset of a locally convex topological vector space, particularly with regard to defining topologies on dual spaces.


Let XX be (in the most general situation) a Cauchy space; this includes uniform convergence spaces, uniform spaces, topological groups, topological vector spaces, and metric spaces (among other things) as special cases.

The following definitions are all equivalent even in weak constructive foundations (such as the internal logic of a predicative topos, CETCS, CSEAR, or CZF):


The space XX is precompact if its completion is compact.


The space XX is precompact if every proper filter on XX has a (proper) Cauchy refinement.


The space XX is precompact if every net in XX has a Cauchy subnet (under any definition of ‘subnet’).

The following definition is equivalent for metric spaces (or even Lawvere metric spaces), assuming weak countable choice (which is very weak):


The space XX is sequentially precompact if every sequence in XX has a Cauchy subsequence.

Of course, this definition makes sense for any Cauchy space, but in general it is not equivalent, so useful to distinguish regardless of one's foundations.

The following notion is equivalent for uniform spaces assuming the ultrafilter principle, dependent choice, and excluded middle (a combination which is not quite as strong as the full axiom of choice but pretty close):


The space XX is totally bounded if every uniform cover has a finite subcover.

Since this definition only makes sense for uniform spaces, there is no need to distinguish it from precompactness when doing classical analysis?.

Even in weak foundations, a precompact space is still totally bounded. Conversely, the ultrafilter principle follows if every totally bounded uniform space is precompact (because the generalised Cantor space 2 K2^K is complete and totally bounded for any cardinal number KK). On the other hand, DC and EM alone are enough to show that every totally bounded metric space is precompact. (I don't know to what extent DC and EM are actually relevant to any of this; my reference HAF tacitly assumes them most of the time.)

In any case, we also have this subsidiary notion:


A subset of XX is precompact (or sequentially so, or totally bounded) if it is precompact (or …) for the inherited structure.

Last revised on June 9, 2013 at 13:43:26. See the history of this page for a list of all contributions to it.