Locally complete space is topologically equivalent to a complete space

Question

Can someone please tell me where I can find a citeable reference for the following result:

Call the metric space $(X, d)$ "locally complete" if for every $x \in X$ there a neighbourhood of $x$ which is complete under $d$.

If $(X,d)$ is locally complete and separable then there exists a metric $d'$ on $X$ such that $(X,d) \to (X,d')$ is a homeomorphism and $(X, d')$ is complete.

This result follows immediately from Alexandrov's theorem that a $G_\delta$ subset of a Polish space is Polish, but I'd rather find a statement in the literature of the above more straightforward result if there is one.

Answer 1

For a reference: this paper has a reference [30] that has a proof. The author cites your result and refers to it. I don't have access to these papers, so I cannot verify exactly.

Answer 2

This is not a reference but a short direct proof.

Let $\bar X$ be the completion of $X$. Define $f:X\to\mathbb R$ by $f(x)=dist(x,\bar X\setminus X)$. Obviously $f$ is continuous, and the local completeness implies that $f$ is strictly positive.

Let $X'\subset X\times\mathbb R$ be the graph of $1/f$. Then $X'$ is homeomorphic to $X$ and complete for the following reason:

If $\{p_n\}$ is a Cauchy sequence in $X'$, then the first coordinates of $p_n$ are a Cauchy sequence in $X$. Hence they converge to a point of $\bar X$. This point cannot be in $\bar X\setminus X$ because the second coordinates of $p_n$ are bounded.

The metric on $X\times\mathbb R$ can be defined as the sum of two coordinate distances (any other common definition will work too).

Answer 3

The result you want to prove also follows directly from Choquet's characterization of completely metrizable metric spaces as those for which the second player has a winning strategy in the "strong Choquet game". See Kechris, Classical descriptive set theory. The usual proof of this characterization uses Alexandrov's theorem, though, so it may not be what you are looking for.