Theorems · Theorem · measure theory

MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    μ s ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (symmDiff U s) < ε

Let μ be a locally finite measure on an R₁ topological space with Borel σ-algebra. If μ is inner regular for finite measure sets with respect to compact sets, then any null measurable set of finite measure can be approximated in measure by an open set. See also Set.exists_isOpen_lt_of_lt and MeasurableSet.exists_isOpen_diff_lt for the case of an outer regular measure.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceMeasureTheory.Measure.InnerRegularCompactLTTopMeasureTheory.IsLocallyFiniteMeasureR1SpaceBorelSpace