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 whyis_diff_scalel
is restricted to scalingR
?
I think it's a mistake and one can generalize for x : V
.
https://github.com/math-comp/analysis/pull/736
Last updated: Mar 29 2024 at 14:01 UTC