aemeasurable_deriv — Mathlib

English

The derivative deriv f is almost everywhere measurable with respect to a given measure μ.

Русский

Производная deriv f измерима почти всюду по отношению к мере μ.

LaTeX

$$$$\text{AEMeasurable}(\text{deriv } f)\,\mu.$$$$

Lean4

theorem aemeasurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜] [MeasurableSpace F] [BorelSpace F] (f : 𝕜 → F)
    (μ : Measure 𝕜) : AEMeasurable (deriv f) μ :=
  (measurable_deriv f).aemeasurable

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