A short proof of an existence theorem in constructive measure theory

Abstract:

The most important example of an integration space in the constructive measure theory of Bishop and Cheng is the couple $(X,\mu )$, where $X$ is a locally compact metric space and $\mu$ is a nonnegative linear function on the space of continuous functions of compact support on $X$. Bishop and Cheng’s proof that $(X,\mu )$ is indeed an integration space is rather involved. In this paper a much simpler proof is given.