Theorems · Theorem · measure theory

nullMeasurableSet_region_between_cc

∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f g : α → ℝ},
  AEMeasurable f μ →
    AEMeasurable g μ →
      ∀ {s : Set α},
        MeasureTheory.NullMeasurableSet s μ →
          MeasureTheory.NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Icc (f p.1) (g p.1)} (μ.prod MeasureTheory.volume)

The region between two a.e.-measurable functions on a null-measurable set is null-measurable; a version for the region together with the graphs of both functions.

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpace