A Hausdorff completion of a uniform space and its canonical dense map

A Hausdorff completion of a uniform space $(X,\mathcal U)$ is a complete separated uniform space $(\widehat X,\widehat{\mathcal U})$ together with a map $\eta:X\to\widehat X$ satisfying both of the following conditions.

• The image $\eta[X]$ is dense: $\overline{\eta[X]}=\widehat X$ (Interior, closure, boundary, exterior, derived set and isolated point in a topological space).
• The original uniformity is exactly the uniformity pulled back along $\eta$: for every $\widehat E\in\widehat{\mathcal U}$, $(\eta\times\eta)^{-1}[\widehat E]\in\mathcal U$, and for every $E\in\mathcal U$ there is $\widehat E\in\widehat{\mathcal U}$ with $(\eta\times\eta)^{-1}[\widehat E]\subseteq E$.

The first half of the second condition is uniform continuity (Uniformly continuous map between uniform spaces); the second half prevents the completion map from discarding any of the original uniform structure. The map is not required to be injective. It is a uniform embedding (Uniform embedding and uniform isomorphism) exactly when it is injective, and this is the usual completion of a separated uniform space.