aestronglyMeasurable_derivWithin_Ioi

English

The AE-strong measurability of the derivative within Ioi holds: AEStronglyMeasurable (derivWithin f (Ioi x) x).

Русский

AE-строгое измерение производной внутри Ioi выполняется.

LaTeX

$$AEStronglyMeasurable (fun x => derivWithin f (Ioi x) x)$$

Lean4

theorem aestronglyMeasurable_derivWithin_Ioi (μ : Measure ℝ) :
    AEStronglyMeasurable (fun x => derivWithin f (Ioi x) x) μ :=
  (stronglyMeasurable_derivWithin_Ioi f).aestronglyMeasurable

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