coe_ereal_ennreal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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