Theorems · Theorem · measure theory

MeasureTheory.AEEqFun.compMeasurePreserving_comp

∀ {α : Type u_1} {β : Type u_2} {δ : Type u_4} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace δ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {γ : Type u_5}
  {mγ : MeasurableSpace γ} {ξ : MeasureTheory.Measure γ} (g : γ →ₘ[ξ] δ) {f : β → γ}
  (hf : MeasureTheory.MeasurePreserving f ν ξ) {f' : α → β} (hf' : MeasureTheory.MeasurePreserving f' μ ν),
  g.compMeasurePreserving (f ∘ f') ⋯ = (g.compMeasurePreserving f hf).compMeasurePreserving f' hf'

Defined in

Mathlib.MeasureTheory.Function.AEEqFun

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceMeasurableSpace