measurable_of_re_im — Mathlib

English

If Re(f) and Im(f) are measurable, then f is measurable.

Русский

Если Re(f) и Im(f) измеримы, то f измерима.

LaTeX

$$$ (\\text{Measurable}(\\operatorname{Re} \\circ f)) \\land (\\text{Measurable}(\\operatorname{Im} \\circ f)) \\Rightarrow \\text{Measurable}(f) $$$

Lean4

theorem measurable_of_re_im (hre : Measurable fun x => RCLike.re (f x)) (him : Measurable fun x => RCLike.im (f x)) :
    Measurable f :=
  by
  convert
    Measurable.add (M := 𝕜) (RCLike.measurable_ofReal.comp hre) ((RCLike.measurable_ofReal.comp him).mul_const RCLike.I)
  exact (RCLike.re_add_im _).symm

Похожие утверждения