measurable_of_measurable_real — Mathlib

English

If f: EReal → α is measurable whenever restricted to the Real part, then f is measurable on EReal.

Русский

Если f: EReal → α измерима при ограничении на вещественную часть, то и на EReal вся функция измерима.

LaTeX

$$$\\text{Measurable}(f) \\Leftarrow \\text{Measurable}(f|_{\\mathbb{R}})$$$

Lean4

theorem measurable_of_measurable_real {f : EReal → α} (h : Measurable fun p : ℝ => f p) : Measurable f :=
  measurable_of_measurable_on_compl_finite {⊥, ⊤} (by simp)
    (MeasurableEquiv.erealEquivReal.symm.measurable_comp_iff.1 h)

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