Theorems · Theorem · measure theory

AEMeasurable.pow

∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} {g : α → γ},
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun x => f x ^ g x) μ

Defined in

Mathlib.MeasureTheory.Group.Arithmetic

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpacePowMeasurablePow