Theorems · Theorem · measure theory

MeasureTheory.meas_le_ae_eq_meas_lt

∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {R : Type u_3} [inst_1 : LinearOrder R]
  [inst_2 : MeasurableSpace R] (ν : MeasureTheory.Measure R) [MeasureTheory.NullSingletonClass ν] (g : α → R),
  (fun t => μ {a | t ≤ g a}) =ᵐ[ν] fun t => μ {a | t < g a}

Defined in

Mathlib.MeasureTheory.Integral.Layercake

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceLinearOrderMeasurableSpaceMeasureTheory.NullSingletonClass