 Inner regularity of Lebesgue measure

The Lebesgue measure of a measurable set is the supremum of the measures of its compact subsets. In particular, an open set of finite positive measure contains a compact subset with at least half its measure. Together with a finite subcover, this turns a finite Wiener covering lemma estimate into an estimate for arbitrary open superlevel sets.