Theorems · Theorem · measure theory

MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top

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

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

Defined in

Mathlib.MeasureTheory.Measure.EverywherePos

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceOpensMeasurableSpaceMeasureTheory.Measure.InnerRegularCompactLTTop