Theorems · Theorem · measure theory

ae_restrict_of_ae_restrict_inter_Ioo

∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {s : Set ℝ} {p : ℝ → Prop},
  (∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ.restrict (s ∩ Set.Ioo a b), p x) → ∀ᵐ (x : ℝ) ∂μ.restrict s, p x

Consider a real set s. If a property is true almost everywhere in s ∩ (a, b) for all a, b ∈ s, then it is true almost everywhere in s. Formulated with μ.restrict. See also ae_of_mem_of_ae_of_mem_inter_Ioo.

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.NullSingletonClass