nLab precompact space

Idea

A precompact space is one whose completion is compact. This makes sense for Cauchy spaces, but not for topological spaces. In the context of uniform spaces, precompact spaces are totally bounded spaces.

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:

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’).

We also have this subsidiary notion:

Definition

A subset of $X$ is precompact if it is precompact (or …) for the inherited structure.

Sequential precompactness

Definition

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

Properties

Theorem

Assuming weak countable choice, every sequentially precompact Lawvere metric space is a precompact Lawvere metric space.

 Relation to totally bounded spaces

Theorem

Every precompact space is a totally bounded space.

Theorem

That every totally bounded uniform space is precompact is equivalent to the ultrafilter principle, because the generalised Cantor space $2^K$ is complete and totally bounded for any cardinal number $K$.

Theorem

Assuming excluded middle and dependent choice, 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.)

See also

• compact space

• totally bounded space