coe_real_ereal — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{AEMeasurable} f \\mu \\Rightarrow \\operatorname{AEMeasurable}(x \\mapsto (f(x) : \\mathrm{EReal})) \\mu$$$

Lean4

@[measurability]
theorem coe_real_ereal {f : α → ℝ} {μ : Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun x => (f x : EReal)) μ :=
  measurable_coe_real_ereal.comp_aemeasurable hf

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