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?)

`apply/derivable1P/derivable1_diffP`

did the job, albeit I had to prove `( *:%R^~ v)`

is differentiable myself..

abab9579 has marked this topic as resolved.

Didn't `differentiableZl`

do the job?

Feel free to PR add the missing lemma to the library.

Oh, `differentiableZl`

works. Dunno why I could not see it before.. Thank you!

By the way, can I know why `is_diff_scalel`

is restricted to scaling `R`

?

abab9579 said:

Oh,

`differentiableZl`

works. Dunno why I could not see it before.. Thank you!

By the way, can I know why`is_diff_scalel`

is restricted to scaling`R`

?

I think it's a mistake and one can generalize for `x : V`

.

https://github.com/math-comp/analysis/pull/736

Last updated: Jun 25 2024 at 19:01 UTC