Theorems · Theorem · measure theory

MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen

∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop}
  [inst_1 : TopologicalSpace α] [μ.OuterRegular],
  μ.InnerRegularWRT p IsOpen →
    (∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)) → μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤

If a measure is inner regular (using closed or compact sets) for open sets, then every measurable set of finite measure can be approximated by a (closed or compact) subset.

Defined in

Mathlib.MeasureTheory.Measure.Regular

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceMeasureTheory.Measure.OuterRegular