ereal_toReal — Mathlib

English

If f: α → EReal is almost everywhere measurable with respect to μ, then x ↦ (f(x)).toReal is almost everywhere measurable with respect to μ.

Русский

Если f: α → EReal измеримо почти всюду по μ, то x ↦ (f(x)).toReal измеримо почти всюду по μ.

LaTeX

$$$\\operatorname{AEMeasurable} f μ \\Rightarrow \\operatorname{AEMeasurable}(x \\mapsto (f(x)).toReal) μ$$$

Lean4

@[measurability, fun_prop]
theorem ereal_toReal {f : α → EReal} {μ : Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun x => (f x).toReal) μ :=
  measurable_ereal_toReal.comp_aemeasurable hf

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