Theorems · Theorem · measure theory

MeasureTheory.MeasurePreserving.aestronglyMeasurable_comp_iff

∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace γ] {β : Type u_4} {f : α → β} {mα : MeasurableSpace α}
  {μa : MeasureTheory.Measure α} {mβ : MeasurableSpace β} {μb : MeasureTheory.Measure β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasurableEmbedding f →
      ∀ {g : β → γ}, MeasureTheory.AEStronglyMeasurable (g ∘ f) μa ↔ MeasureTheory.AEStronglyMeasurable g μb

Defined in

Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace