Abstract:
Studies in the constructive analysis are partially stimulated by the desire to build up a theory which could profitably replace the classical analysis in applications. But for some reasons the constructive analysis nowadays can hardly be studied by those who have never studied the classical mathematics. One of the reasons is as follows. It proves sometimes useful to conceive the system of constructive real numbers as “a part” of the system of classical real numbers, the system of constructive complex numbers as “a part” of the system of classical complex numbers, etc. In the paper a method is proposed for replacing such intuitive considerations by exact treatments which are acceptable in the constructive mathematics. A filling of a (constructive) metric space $X$ is defined to be a (constructive) extension of $X$ supplied with uniform structure which satisfies some conditions (e.g. a metric completion of $X$ is one of its fillings, but generally not maximal). A kind of Borel finite subcovering lemma based on the notion of filling is formulated and applied to investigation of constructive iniformly continuous real-valued functions on compact metric spaces, and constructive functions of complex variable.