Theorems · Theorem · measure theory

MeasureTheory.AEEqFun.compQuasiMeasurePreserving_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.Measure.QuasiMeasurePreserving f ν ξ) {f' : α → β}
  (hf' : MeasureTheory.Measure.QuasiMeasurePreserving f' μ ν),
  g.compQuasiMeasurePreserving (f ∘ f') ⋯ = (g.compQuasiMeasurePreserving f hf).compQuasiMeasurePreserving f' hf'

Defined in

Mathlib.MeasureTheory.Function.AEEqFun

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceMeasurableSpace