On Thu, 9 Jan 2020 06:06:59 -0500, Mario Carneiro <[email protected]> wrote: > If you want the function version, look at dvmul. But the relation version > is the core version, because it isn't good enough to know that the > derivative equals x if you don't know the function is also differentiable > at x. Plus the derivative is not unique in certain pathological cases so > you can't actually recover the relation version from the function version > with differentiability side conditions.
I've created a pull request to put this information into set.mm: https://github.com/metamath/set.mm/pull/1397 --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1ipYxa-0005wA-2A%40rmmprod07.runbox.
