HasDerivOn

Stream: Is there code for X?

[Alex Kontorovich]

We have HasDerivAt; is there a reason not to have HasDerivOn (mimicking DifferentiableOn)? Something like:

def HasDerivOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F]
    [NormedSpace 𝕜 F] (f f' : 𝕜 → F) (s : Set F) : Prop :=
  ∀ x ∈ s, HasDerivAt f (f' x) x

[Anatole Dedecker]

HasDerivOn would presumably be defined in terms of docs#HasDerivWithinAt instead. In any case, I think that most of the time it would be more painful to use because you’d end up with a lot of unnecessary lambdas.