ennreal_toReal — Mathlib

English

If f is a.e.-measurable, then its toReal image is a.e.-measurable.

Русский

Если f является а.е.-измеримой, то её toReal образ тоже а.е.-измерим.

LaTeX

$$$\text{AEMeasurable } f \Rightarrow \text{AEMeasurable } (\lambda x. (f(x)).toReal)$$$

Lean4

@[measurability, fun_prop]
theorem ennreal_toReal {f : α → ℝ≥0∞} {μ : Measure α} (hf : AEMeasurable f μ) :
    AEMeasurable (fun x => ENNReal.toReal (f x)) μ :=
  ENNReal.measurable_toReal.comp_aemeasurable hf

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