Theorems · Theorem · measure theory

MeasureTheory.Measure.everywherePosSubset_ae_eq

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α] [μ.InnerRegular], MeasurableSet s → μ.everywherePosSubset s =ᵐ[μ] s

In a space with an inner regular measure, any measurable set coincides almost everywhere with its everywhere positive subset.

Defined in

Mathlib.MeasureTheory.Measure.EverywherePos

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.Measure.InnerRegular