coe_nnreal_real — Mathlib

English

If f : α → NNReal is measurable, then x ↦ (f(x)) as real is measurable.

Русский

Если f: α → NNReal измерима, то x ↦ (f(x)) как вещественное число измеримо.

LaTeX

$$$\\\\forall f:\\\\alpha \\\\to \\\\mathbb{R}_{\\ge 0},\\\\;\\\\operatorname{Measurable}(f) \\\\Rightarrow \\\\operatorname{Measurable}(x \\mapsto (f(x) : \\mathbb{R})).$$$

Lean4

@[measurability, fun_prop]
theorem coe_nnreal_real {f : α → ℝ≥0} (hf : Measurable f) : Measurable fun x => (f x : ℝ) :=
  measurable_coe_nnreal_real.comp hf

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