ennreal_ofReal — Mathlib

English

Let f be AEMeasurable with respect to μ. Then the function x ↦ ENNReal.ofReal(f(x)) is AEMeasurable with respect to μ.

Русский

Пусть f измеримо почти всюду по мере μ. Тогда x ↦ ENNReal.ofReal(f(x)) измеримо почти всюду по μ.

LaTeX

$$$\operatorname{AEMeasurable} f \mu \Rightarrow \operatorname{AEMeasurable}\left(x \mapsto \mathrm{ENNReal.ofReal}(f(x))\right) \mu$$$

Lean4

@[measurability, fun_prop]
theorem ennreal_ofReal {f : α → ℝ} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x ↦ ENNReal.ofReal (f x)) μ :=
  ENNReal.continuous_ofReal.measurable.comp_aemeasurable hf

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