Theorems · Theorem · measure theory

MeasureTheory.volume_preserving_pi

∀ {ι : Type u_1} [inst : Fintype ι] {α' : ι → Type u_4} {β' : ι → Type u_5}
  [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α' i)] [inst_2 : (i : ι) → MeasureTheory.MeasureSpace (β' i)]
  [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume] {f : (i : ι) → α' i → β' i},
  (∀ (i : ι), MeasureTheory.MeasurePreserving (f i) MeasureTheory.volume MeasureTheory.volume) →
    MeasureTheory.MeasurePreserving (fun a i => f i (a i)) MeasureTheory.volume MeasureTheory.volume

Defined in

Mathlib.MeasureTheory.Constructions.Pi

Cited by

4 results in Mathlib

Foundations

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

Assumes

FintypeMeasureTheory.MeasureSpaceMeasureTheory.MeasureSpaceMeasureTheory.SigmaFinite