measurable_coe_nnreal_real_iff — Mathlib

English

For f: α → ℝ≥0, the real-valued map x ↦ f(x) is measurable as a function α → ℝ if and only if f is measurable as a function α → ℝ≥0.

Русский

Для f: α → ℝ≥0, отображение x ↦ f(x) как функция α → ℝ измеримо тогда и только тогда, когда f как функция α → ℝ≥0 измеримо.

LaTeX

$$$\operatorname{Measurable} (f : α \to \mathbb{R}_{\ge 0}) \\iff \\operatorname{Measurable} (f : α \to \mathbb{R})$$$

Lean4

@[simp, norm_cast]
theorem measurable_coe_nnreal_real_iff {f : α → ℝ≥0} : Measurable (fun x => f x : α → ℝ) ↔ Measurable f :=
  ⟨fun h => by simpa only [Real.toNNReal_coe] using h.real_toNNReal, Measurable.coe_nnreal_real⟩

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