measurable_coe_nnreal_ennreal_iff

English

The measurability of a function into ENNReal via coe from NNReal is equivalent to measurability of the original NNReal-valued function.

Русский

Измеримость функции в ENNReal через включение из NNReal равна измеримости исходной NNReal-функции.

LaTeX

$$$\big( (\lambda x. (f(x) : ENNReal)) \text{ is measurable} \big) \iff (\lambda x. f(x) \text{ is measurable})$$$

Lean4

@[simp, norm_cast]
theorem measurable_coe_nnreal_ennreal_iff {f : α → ℝ≥0} : (Measurable fun x => (f x : ℝ≥0∞)) ↔ Measurable f :=
  ⟨fun h => h.ennreal_toNNReal, fun h => h.coe_nnreal_ennreal⟩

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