ereal_toENNReal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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