Theorems · Theorem · measure theory

aemeasurable_of_re_im

∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace α] {f : α → 𝕜}
  {μ : MeasureTheory.Measure α},
  AEMeasurable (fun x => RCLike.re (f x)) μ → AEMeasurable (fun x => RCLike.im (f x)) μ → AEMeasurable f μ

Defined in

Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeMeasurableSpace