Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable

∀ {α : Type u_1} {E : Type u_5} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : TopologicalSpace E] [TopologicalSpace.MetrizableSpace E] (hm : m ≤ m₀),
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → f =ᵐ[μ] g → f =ᵐ[μ.trim hm] g

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace.MetrizableSpace