aestronglyMeasurable — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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