aemeasurable_restrict_of_measurable_subtype

English

If s is measurable and f|_s is measurable, then f is AEMeasurable on μ.restrict s.

Русский

Если s измеримо и ограничение f на s измеримо, то f является AЕ-измеримой на μ|_s.

LaTeX

$$$\text{hs : MeasurableSet } s \rightarrow \big( \mathrm{Measurable}(f|_s) \Rightarrow \mathrm{AEMeasurable}(f, \mu\restriction s) \big)$$$

Lean4

theorem aemeasurable_restrict_of_measurable_subtype {s : Set α} (hs : MeasurableSet s)
    (hf : Measurable fun x : s => f x) : AEMeasurable f (μ.restrict s) :=
  (aemeasurable_restrict_iff_comap_subtype hs).2 hf.aemeasurable

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