论文标题
建设性衡量理论的集合家族
Families of Sets in Constructive Measure Theory
论文作者
论文摘要
我们介绍了建设性主教 - 昌理论的谓词重建的第一步。在Bishop的集合理论的半正式阐述中工作，并援引了固定指数的子集（给定集合）的概念，我们得出了预一体化空间和预先衡量空间的概念。然后，我们构建了与预估计空间相关的简单功能的预一体化空间，以及预一整合空间的$ l^1 $ completion。与Bishop-Cheng量度理论的标准介绍不同，我们的发展是完全谓词，并且避免了可数选择的公理。
We present the first steps of a predicative reconstruction of the constructive Bishop-Cheng measure theory. Working in a semi-formal elaboration of Bishop's set theory and invoking the notion of a set-indexed family of subsets (of a given set), we arrive at notions of a pre-integration space and of a pre-measure space. We then construct the pre-integration space of simple functions associated to a pre-measure space and the $L^1$-completion of a pre-integration space. Unlike the standard presentation of Bishop-Cheng measure theory, our development is completely predicative and avoids the axiom of countable choice.
