Stream: math-comp analysis

Topic: Inverse function and differentiation


view this post on Zulip Laurent Théry (Jun 01 2021 at 18:22):

I've started playing with the exponential in a realType. It is then natural to get the log as the inverse function .
This works well but it seems there is no support to get continuity and differentiability. The file derive.v is a bit scary to me. How should I start if I'd like to add let's say continuity of the inverse function?


Last updated: Aug 11 2022 at 03:02 UTC