Commit 2025-12-12 20:02 3f5aae8d

feat: for a regular measure, write the measure of an open set as a supremum of integrals of continuous functions (#32783) There is already such a statement for the measures of compact sets, in the file on uniqueness of Haar measures. This PR also moves them both to a new file.