Theorems · Theorem · functional analysis

MeasureTheory.Lp.compMeasurePreserving_comp

∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  {γ : Type u_8} {mγ : MeasurableSpace γ} {μc : MeasureTheory.Measure γ} {f : β → γ}
  (hf : MeasureTheory.MeasurePreserving f μb μc) {f' : α → β} (hf' : MeasureTheory.MeasurePreserving f' μ μb),
  MeasureTheory.Lp.compMeasurePreserving (f ∘ f') ⋯ =
    (MeasureTheory.Lp.compMeasurePreserving f' hf').comp (MeasureTheory.Lp.compMeasurePreserving f hf)

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupMeasurableSpace