Theorems · Theorem · measure theory

MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict

∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : α → Prop},
  s =ᵐ[μ] t → ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x

If two measurable sets are ae_eq then any proposition that is almost everywhere true on one is almost everywhere true on the other

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

2 results in Mathlib

Foundations

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