**analysis** (differential/integral calculus, functional analysis, topology)

metric space, normed vector space

open ball, open subset, neighbourhood

convergence, limit of a sequence

compactness, sequential compactness

continuous metric space valued function on compact metric space is uniformly continuous

…

…

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.

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:

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

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

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:

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

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

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

Every precompact space is a totally bounded space.

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$.

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

Last revised on November 16, 2022 at 21:54:22. See the history of this page for a list of all contributions to it.