Theorems · Theorem · measure theory

MeasureTheory.StronglyMeasurable.ae_eq_trim_iff

∀ {α : 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 =ᵐ[μ.trim hm] g ↔ f =ᵐ[μ] g)

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace.MetrizableSpace