Commit 2022-06-03 16:16 d63246c0
View on Github →feat(analysis/calculus/fderiv_measurable): the right derivative is measurable (#14527) We already know that the full Fréchet derivative is measurable. In this PR, we follow the same proof to show that the right derivative of a function defined on the real line is also measurable (the target space may be any complete vector space).