aestronglyMeasurable' — Mathlib

English

From interval-integrability, f is AEStronglyMeasurable on μ restricted to Ioc b a.

Русский

Из интервалной интегрируемости следует AEStronglyMeasurable f на μ, ограниченной Ioc b a.

LaTeX

$$$\operatorname{IntervalIntegrable}(f,\mu,a,b) \Rightarrow \operatorname{AEStronglyMeasurable}(f,\mu|_{Ioc(b,a)})$$$

Lean4

protected theorem aestronglyMeasurable' (h : IntervalIntegrable f μ a b) :
    AEStronglyMeasurable f (μ.restrict (Ioc b a)) :=
  h.2.aestronglyMeasurable

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