Define derivative in iset.mm

[jkingdon]

The basic idea from set.mm does not have obvious problems: ( S _D F ) is a function whose value at x is the limit of ( ( f ` z ) - ( f ` x ) ) / ( z - x ) as z approaches x, and the domain of ( S _D F ) is the interior points of dom F where that limit exists (see for example dvbssntr and dvres).

However, the details in set.mm rely a lot on using decidability of real number equality in places like the if statement in https://us.metamath.org/mpeuni/df-limc.html and dom 𝑓 ∖ {𝑥} in https://us.metamath.org/mpeuni/df-dv.html

It seems like this should be intuitionizable, because the kind of limit here doesn't feel super different from the process at https://us.metamath.org/ileuni/df-cnp.html and related theorems but I'm not sure I quite see how this is supposed to work, or have found any relevant literature references.

[digama0]

I'm pretty sure the if statement in df-limc is eliminable. Rather than reusing the "continuous at a point" predicate, you can just use one of the direct definitions like ellimc2. You will have to grapple with the "neighborhood minus a point" filter for both df-limc and df-dv, but there are other ways to do that and at least insofar as division by zero in df-dv is the reason for the exclusion, you might consider using "apart from zero" instead. Do you have apartness spaces?

[jkingdon]

I'm pretty sure the if statement in df-limc is eliminable. Rather than reusing the "continuous at a point" predicate, you can just use one of the direct definitions like ellimc2.

I guess I'll try https://us.metamath.org/mpeuni/ellimc3.html because it would appear the only change needed is to change negated equality to apartness one place.

You will have to grapple with the "neighborhood minus a point" filter for both df-limc and df-dv, but there are other ways to do that and at least insofar as division by zero in df-dv is the reason for the exclusion, you might consider using "apart from zero" instead.

Well, anything involving division is going to have to have an apart from zero in there somewhere.

Do you have apartness spaces?

Not in the sense of tying apartness to topologies, or defining a notation for a relation between a point and a set. We should be part of the way to being able to define them with things like https://us.metamath.org/ileuni/apcotr.html and I do see a few scattered existing theorems which have things like { y e. CC | y =//= 0 }. As for formalizing things like the results or definitions at https://plato.stanford.edu/entries/mathematics-constructive/supplement2.html or https://ncatlab.org/nlab/show/apartness+space that seems like something to keep in mind, although I guess both of those have generality which we don't strictly need for subsets of complex numbers.

[jkingdon]

Although there are some outstanding issues (most notably #3661 and a number of theorems which rely on that, at least in set.mm), I think based on https://us.metamath.org/ileuni/dvrecap.html , https://us.metamath.org/ileuni/dvexp.html , https://us.metamath.org/ileuni/dvcj.html and others, we can consider the derivative successfully defined.