Fix df-dv comment in set.mm and iset.mm

This definition applies to subsets of complex numbers, not just real
numbers.  Same comment is in df-dv in set.mm and df-dvap in iset.mm
so fix it both places.

Author: jkingdon

iset.mm

@@ -136206,17 +136206,17 @@ S C_ ( P ( ball ` D ) T ) ) $=
 
   ${
     $d s f x z w $.
-    $( Define the derivative operator on functions on the reals.  This acts on
-       functions to produce a function that is defined where the original
-       function is differentiable, with value the derivative of the function at
-       these points.  The set ` s ` here is the ambient topological space under
-       which we are evaluating the continuity of the difference quotient.
-       Although the definition is valid for any subset of ` CC ` and is
-       well-behaved when ` s ` contains no isolated points, we will restrict
-       our attention to the cases ` s = RR ` or ` s = CC ` for the majority of
-       the development, these corresponding respectively to real and complex
-       differentiation.  (Contributed by Mario Carneiro, 7-Aug-2014.)  (Revised
-       by Jim Kingdon, 25-Jun-2023.) $)
+    $( Define the derivative operator.  This acts on functions to produce a
+       function that is defined where the original function is differentiable,
+       with value the derivative of the function at these points.  The set
+       ` s ` here is the ambient topological space under which we are
+       evaluating the continuity of the difference quotient.  Although the
+       definition is valid for any subset of ` CC ` and is well-behaved when
+       ` s ` contains no isolated points, we will restrict our attention to the
+       cases ` s = RR ` or ` s = CC ` for the majority of the development,
+       these corresponding respectively to real and complex differentiation.
+       (Contributed by Mario Carneiro, 7-Aug-2014.)  (Revised by Jim Kingdon,
+       25-Jun-2023.) $)
     df-dvap $a |- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |->
       U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) |`t s ) ) ` dom f )
         ( { x } X. ( ( z e. { w e. dom f | w =//= x } |->

set.mm

@@ -334060,16 +334060,16 @@ or are almost disjoint (the interiors are disjoint).  (Contributed by
       if ( z = x , y , ( f ` z ) ) ) e.
         ( ( ( j |`t ( dom f u. { x } ) ) CnP j ) ` x ) } ) $.
 
-    $( Define the derivative operator on functions on the reals.  This acts on
-       functions to produce a function that is defined where the original
-       function is differentiable, with value the derivative of the function at
-       these points.  The set ` s ` here is the ambient topological space under
-       which we are evaluating the continuity of the difference quotient.
-       Although the definition is valid for any subset of ` CC ` and is
-       well-behaved when ` s ` contains no isolated points, we will restrict
-       our attention to the cases ` s = RR ` or ` s = CC ` for the majority of
-       the development, these corresponding respectively to real and complex
-       differentiation.  (Contributed by Mario Carneiro, 7-Aug-2014.) $)
+    $( Define the derivative operator.  This acts on functions to produce a
+       function that is defined where the original function is differentiable,
+       with value the derivative of the function at these points.  The set
+       ` s ` here is the ambient topological space under which we are
+       evaluating the continuity of the difference quotient.  Although the
+       definition is valid for any subset of ` CC ` and is well-behaved when
+       ` s ` contains no isolated points, we will restrict our attention to the
+       cases ` s = RR ` or ` s = CC ` for the majority of the development,
+       these corresponding respectively to real and complex differentiation.
+       (Contributed by Mario Carneiro, 7-Aug-2014.) $)
     df-dv $a |- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |->
       U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f )
         ( { x } X. ( ( z e. ( dom f \ { x } ) |->