aemeasurable_derivWithin_Ici — Mathlib

English

The a.e. measurability of the derivative within Ici x holds: AEStronglyMeasurable (derivWithin f (Ici x) x).

Русский

Пусть производная внутри Ici x имеет асимптотически измеримую структуру: AEStronglyMeasurable.

LaTeX

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

Lean4

theorem aemeasurable_derivWithin_Ici [MeasurableSpace F] [BorelSpace F] (μ : Measure ℝ) :
    AEMeasurable (fun x => derivWithin f (Ici x) x) μ :=
  (measurable_derivWithin_Ici f).aemeasurable

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