Commit 2024-07-15 20:56 627efab4

View on Github →

feat(Measure/Regular): add lemmas about compact closed sets (#14487) Other changes:

  • Prove that a measurable set can be approximated by an open set.
  • Migrate from OuterRegular.measure_closure_of_isCompact to IsCompact.measure_closure. While neither of these lemmas imply the other, all applications of the former lemma in Mathlib had all the assumptions for the latter.

Estimated changes