Definition 2

Tag 0BG5, permanent. Cite it as [Bourbaki, Tag 0BG5].

General Topology, chapter II, § 4. Relations between uniform spaces and compact spaces

A uniform space $X$ is said to be precompact if its Hausdorff completion $\hat{X}$ is compact. A subset $A$ of a uniform space $X$ is said to be a precompact subset if the uniform subspace $A$ of $X$ is precompact.

Thus a subset $A$ of a uniform space $X$ is precompact if and only if the closure of $i(A)$ in $\hat{X}$ is compact ( $i : X \to \hat{X}$ being the canonical map) (§ 3, no. 9, Proposition 18, Corollary 1).

Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.

Cited by

Nothing.

Cites

§ 3, no. 9, Proposition 18
Corollary 1