The Vitali covering theorem in constructive mathematics
Hannes Diener, Anton Hedin · Journal of Logic and Analysis · 2012
This paper investigates the Vitali Covering Theorem from various constructive angles.A Vitali Cover of a metric space is a cover such that for every point there exists an arbitrarily small element of the cover containing this point.The Vitali Covering Theorem now states, that for any Vitali Cover one can find a finite family of pairwise disjoint sets in the Vitali Cover that cover the entire space up to a set of a given non-zero measure.We will show, by means of a recursive counterexample, that there cannot be a fully constructive proof, but that adding a very weak semi-constructive principle suffices to give such a proof.Lastly, we will show that with an appropriate formalization in formal topology the non-constructive problems can be avoided completely.