complex_ofReal — Mathlib

English

Let f be almost everywhere measurable; then x ↦ (f(x) : ℂ) is almost everywhere measurable.

Русский

Пусть f ~почти всюду измерима; тогда x ↦ (f(x) : ℂ) ~почти всюду измерима.

LaTeX

$$$AEMeasurable\\ f\\ μ \\rightarrow AEMeasurable\\bigl(\\lambda x. (f(x) : \\mathbb{C})\\bigr)\\ μ$$$

Lean4

@[measurability, fun_prop]
protected theorem complex_ofReal {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ}
    (hf : AEMeasurable f μ) : AEMeasurable (fun x ↦ (f x : ℂ)) μ :=
  Complex.measurable_ofReal.comp_aemeasurable hf

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