# Precompact spaces

## Idea

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.

## Definitions

Let $X$ 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):

###### Definition

The space $X$ is precompact if its completion is compact.

###### Definition

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

###### Definition

The space $X$ is precompact if every net in $X$ 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):

###### Definition

The space $X$ is sequentially precompact if every sequence in $X$ 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):

###### Definition

The space $X$ 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^K$ is complete and totally bounded for any cardinal number $K$). 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:

###### Definition

A subset of $X$ 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.