measurable_of_measurable_nnreal — Mathlib

English

If f : ENNReal → α is measurable whenever restricted to NNReal (via the map p ↦ f(p)), then f is measurable on ENNReal.

Русский

Если f: ENNReal → α измеримо, когда ограничено до NNReal через f(p), то f измеримо на ENNReal.

LaTeX

$$$\operatorname{Measurable}\bigl(\lambda p. f(p)\bigr) \Rightarrow \operatorname{Measurable} f$$$

Lean4

theorem measurable_of_measurable_nnreal {f : ℝ≥0∞ → α} (h : Measurable fun p : ℝ≥0 => f p) : Measurable f :=
  measurable_of_measurable_on_compl_singleton ∞ (MeasurableEquiv.ennrealEquivNNReal.symm.measurable_comp_iff.1 h)

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