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 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 is precompact if its completion is compact.
The space is precompact if every proper filter on has a (proper) Cauchy refinement.
The space is precompact if every net in has a Cauchy subnet (under any definition of ‘subnet’).
We also have this subsidiary notion:
A subset of is precompact if it is precompact (or …) for the inherited structure.
The space is sequentially precompact if every sequence in 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 is complete and totally bounded for any cardinal number .
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.