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.
On Thu, Jan 9, 2020 at 5:52 AM 'fl' via Metamath <[email protected]> wrote: > > There's no difference. He used a notation based on relationships rather > than functions. > > That's unfortunate in my opinion. The usual semantics should be retained. > > -- > FL > > -- > 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/4746e0aa-8b89-4689-b6f9-a9d7d58dc55d%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4746e0aa-8b89-4689-b6f9-a9d7d58dc55d%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvjJ%3Dsha%2BVcR7hzE-emjMkoY_b8%2B194JRU05Y-1OzHOqQ%40mail.gmail.com.
