Abstract:
The paper establishes the existence of a non-complete constructive metric space, complete with respect to each element of some class of measure 1 in the Cantor space, containing all Martin-Löf random sequences. It is proved that any constructive metric space defined in a standard way on an invariant set of constructive reals and complete with respect to each element of some class of measure 1 is complete. An example of a constructive metric space is constructed in which every fundamental sequence converges, but there is no class of measure 1 such that the space is complete with respect to each of its elements.