Commit 2023-09-07 19:25 f599dc21

feat: measurability of the derivative of a function depending on a parameter (#6903) We reuse the main results that were proved for functions not depending on a parameter (but we need to tweak the definition of the set A to let it cover all cases, replacing a large inequality by a strict one).