# Documentation

Mathlib.MeasureTheory.Function.SpecialFunctions.IsROrC

# Measurability of the basic IsROrC functions #

theorem IsROrC.measurable_re {𝕜 : Type u_1} [] :
Measurable IsROrC.re
theorem IsROrC.measurable_im {𝕜 : Type u_1} [] :
Measurable IsROrC.im
theorem Measurable.re {α : Type u_1} {𝕜 : Type u_2} [] {m : } {f : α𝕜} (hf : ) :
Measurable fun x => IsROrC.re (f x)
theorem AEMeasurable.re {α : Type u_1} {𝕜 : Type u_2} [] {m : } {f : α𝕜} {μ : } (hf : ) :
AEMeasurable fun x => IsROrC.re (f x)
theorem Measurable.im {α : Type u_1} {𝕜 : Type u_2} [] {m : } {f : α𝕜} (hf : ) :
Measurable fun x => IsROrC.im (f x)
theorem AEMeasurable.im {α : Type u_1} {𝕜 : Type u_2} [] {m : } {f : α𝕜} {μ : } (hf : ) :
AEMeasurable fun x => IsROrC.im (f x)
theorem IsROrC.measurable_ofReal {𝕜 : Type u_2} [] :
Measurable IsROrC.ofReal
theorem measurable_of_re_im {α : Type u_1} {𝕜 : Type u_2} [] [] {f : α𝕜} (hre : Measurable fun x => IsROrC.re (f x)) (him : Measurable fun x => IsROrC.im (f x)) :
theorem aemeasurable_of_re_im {α : Type u_1} {𝕜 : Type u_2} [] [] {f : α𝕜} {μ : } (hre : AEMeasurable fun x => IsROrC.re (f x)) (him : AEMeasurable fun x => IsROrC.im (f x)) :