theorem
Measurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[IsROrC 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
(hf : Measurable f)
:
Measurable fun (x : α) => IsROrC.re (f x)
theorem
AEMeasurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[IsROrC 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
:
AEMeasurable fun (x : α) => IsROrC.re (f x)
theorem
Measurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[IsROrC 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
(hf : Measurable f)
:
Measurable fun (x : α) => IsROrC.im (f x)
theorem
AEMeasurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[IsROrC 𝕜]
{m : MeasurableSpace α}
{f : α → 𝕜}
{μ : MeasureTheory.Measure α}
(hf : AEMeasurable f)
:
AEMeasurable fun (x : α) => IsROrC.im (f x)
theorem
measurable_of_re_im
{α : Type u_1}
{𝕜 : Type u_2}
[IsROrC 𝕜]
[MeasurableSpace α]
{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}
[IsROrC 𝕜]
[MeasurableSpace α]
{f : α → 𝕜}
{μ : MeasureTheory.Measure α}
(hre : AEMeasurable fun (x : α) => IsROrC.re (f x))
(him : AEMeasurable fun (x : α) => IsROrC.im (f x))
: