Metrization of the Uniform Space and Effective Convergence
Mariko Yasugi, Yoshiki Tsujii, Takakazu Mori · Mathematical logic quarterly · 2002
The subject of the present article is the following fact. Consider an effective uniform space. A generally constructed metric from the uniformity has the property that a sequence from the space effectively converges with respect to the uniform topology if and only if it does with respect to the induced metric. This can be shown without assuming the computability of the metric.