arXiv · 2207.04000
Families of Sets in Constructive Measure Theory
Abstract
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.
Explore related subjects
Keep this discovery
Max Zeuner. 2022-07-08. Families of Sets in Constructive Measure Theory. https://arxiv.org/abs/2207.04000
Cite the original work for its findings. Save a collection to share your selection of sources.