Hello, I am lost searching for a lemma giving `differentiable f x -> forall v, derivable f x v`

. If my memory serves correctly, this one holds (while converse does not). Where is the corresponding lemma? (Or is this easily proved in some other way?)

Last updated: Feb 05 2023 at 15:03 UTC