measurable_deriv — Mathlib

English

The derivative function deriv f is measurable under standard assumptions.

Русский

Функция производной deriv f измерима при обычных допущениях.

LaTeX

$$$$\text{Measurable}(\text{deriv } f).$$$$

Lean4

@[measurability, fun_prop]
theorem measurable_deriv [MeasurableSpace 𝕜] [OpensMeasurableSpace 𝕜] [MeasurableSpace F] [BorelSpace F] (f : 𝕜 → F) :
    Measurable (deriv f) := by simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1

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