Theorems · Theorem · measure theory

IsOpen.exists_lt_isClosed

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.WeaklyRegular] ⦃U : Set α⦄, IsOpen U → ∀ {r : ENNReal}, r < μ U → ∃ F ⊆ U, IsClosed F ∧ r < μ F

If μ is a weakly regular measure, then any open set can be approximated by a closed subset.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

0 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceMeasureTheory.Measure.WeaklyRegular