Commit 2024-02-10 06:34 b1a09514

feat: everywhere positive sets for a measure (#10139) A set s is everywhere positive with respect to a measure mu if, for every point in s, all its neighborhoods inside s have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).