Theorem measurable_deriv

Modification history

2023-05-29 18:40

Mathlib/Analysis/Calculus/FDerivMeasurable.lean

feat: port Analysis.Calculus.FDerivMeasurable (#4468)

Added measurable_deriv View on Github →