Measurability of the basic is_R_or_C functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[measurability]
@[measurability]
@[measurability]
theorem
measurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{m : measurable_space α}
{f : α → 𝕜}
(hf : measurable f) :
measurable (λ (x : α), ⇑is_R_or_C.re (f x))
@[measurability]
theorem
ae_measurable.re
{α : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{m : measurable_space α}
{f : α → 𝕜}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ) :
ae_measurable (λ (x : α), ⇑is_R_or_C.re (f x)) μ
@[measurability]
theorem
measurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{m : measurable_space α}
{f : α → 𝕜}
(hf : measurable f) :
measurable (λ (x : α), ⇑is_R_or_C.im (f x))
@[measurability]
theorem
ae_measurable.im
{α : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
{m : measurable_space α}
{f : α → 𝕜}
{μ : measure_theory.measure α}
(hf : ae_measurable f μ) :
ae_measurable (λ (x : α), ⇑is_R_or_C.im (f x)) μ
@[measurability]
theorem
measurable_of_re_im
{α : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[measurable_space α]
{f : α → 𝕜}
(hre : measurable (λ (x : α), ⇑is_R_or_C.re (f x)))
(him : measurable (λ (x : α), ⇑is_R_or_C.im (f x))) :
theorem
ae_measurable_of_re_im
{α : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[measurable_space α]
{f : α → 𝕜}
{μ : measure_theory.measure α}
(hre : ae_measurable (λ (x : α), ⇑is_R_or_C.re (f x)) μ)
(him : ae_measurable (λ (x : α), ⇑is_R_or_C.im (f x)) μ) :
ae_measurable f μ