On Thursday, January 9, 2020 at 12:07:11 PM UTC+1, Mario Carneiro 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. >
This worries me because I don't understand this at all... Is it possible that "the derivative of f at x equals A" (you wrote "equals x") yet the function is f not differentiable at x ? Is it a side effect of the coding in set.mm, which makes undefined expressions equal to (/) (so the above can happen only with A = (/) ) ? I had proposed solutions (with of course some drawbacks) so that nonsensical expressions could not be written, or at least not be used, and this situation could be avoided (if I understand it correctly). Second, you write that the derivative is not unique ? Last time I checked, \C was Hausdorff. Or are you using a nonstandard definition for the derivative ? Thanks, Benoît -- 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/a20eaecb-190e-4dc2-ad80-4aa6a508a3e8%40googlegroups.com.
