Theorems · Theorem · measure theory

MeasureTheory.Measure.dense_of_ae

∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {p : X → Prop}, (∀ᵐ (x : X) ∂μ, p x) → Dense {x | p x}

A property satisfied almost everywhere is satisfied on a dense subset.

Defined in

Mathlib.MeasureTheory.Measure.OpenPos

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasureTheory.Measure.IsOpenPosMeasure