Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.pi_map_pi

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.FiniteMeasure (α i)) {β : ι → Type u_3} [inst_2 : (i : ι) → MeasurableSpace (β i)]
  {f : (i : ι) → α i → β i},
  (∀ (i : ι), AEMeasurable (f i) ↑(μ i)) →
    ((MeasureTheory.FiniteMeasure.pi μ).map fun x i => f i (x i)) =
      MeasureTheory.FiniteMeasure.pi fun i => (μ i).map (f i)

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeMeasurableSpaceMeasurableSpace