aemeasurable_coe_nnreal_ennreal_iff

English

AEMeasurable (fun x => ENNReal.ofNNReal (f x)) μ iff AEMeasurable f μ.

Русский

AEMeasurable (fun x => ENNReal.ofNNReal (f x)) μ эквивалентно AEMeasurable f μ.

LaTeX

$$$\text{AEMeasurable } (\lambda x. (f(x) : ENNReal)) \iff \text{AEMeasurable } f$$$

Lean4

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

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