ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dvap Unicode version

Definition df-dvap 12805
Description: 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.)
Assertion
Ref Expression
df-dvap  |-  _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 }  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x ) ) )
Distinct variable group:    f, s, x, z, w

Detailed syntax breakdown of Definition df-dvap
StepHypRef Expression
1 cdv 12803 . 2  class  _D
2 vs . . 3  setvar  s
3 vf . . 3  setvar  f
4 cc 7625 . . . 4  class  CC
54cpw 3510 . . 3  class  ~P CC
62cv 1330 . . . 4  class  s
7 cpm 6543 . . . 4  class  ^pm
84, 6, 7co 5774 . . 3  class  ( CC 
^pm  s )
9 vx . . . 4  setvar  x
103cv 1330 . . . . . 6  class  f
1110cdm 4539 . . . . 5  class  dom  f
12 cabs 10776 . . . . . . . . 9  class  abs
13 cmin 7940 . . . . . . . . 9  class  -
1412, 13ccom 4543 . . . . . . . 8  class  ( abs 
o.  -  )
15 cmopn 12164 . . . . . . . 8  class  MetOpen
1614, 15cfv 5123 . . . . . . 7  class  ( MetOpen `  ( abs  o.  -  )
)
17 crest 12130 . . . . . . 7  classt
1816, 6, 17co 5774 . . . . . 6  class  ( (
MetOpen `  ( abs  o.  -  ) )t  s )
19 cnt 12272 . . . . . 6  class  int
2018, 19cfv 5123 . . . . 5  class  ( int `  ( ( MetOpen `  ( abs  o.  -  ) )t  s ) )
2111, 20cfv 5123 . . . 4  class  ( ( int `  ( (
MetOpen `  ( abs  o.  -  ) )t  s ) ) `  dom  f
)
229cv 1330 . . . . . 6  class  x
2322csn 3527 . . . . 5  class  { x }
24 vz . . . . . . 7  setvar  z
25 vw . . . . . . . . . 10  setvar  w
2625cv 1330 . . . . . . . . 9  class  w
27 cap 8350 . . . . . . . . 9  class #
2826, 22, 27wbr 3929 . . . . . . . 8  wff  w #  x
2928, 25, 11crab 2420 . . . . . . 7  class  { w  e.  dom  f  |  w #  x }
3024cv 1330 . . . . . . . . . 10  class  z
3130, 10cfv 5123 . . . . . . . . 9  class  ( f `
 z )
3222, 10cfv 5123 . . . . . . . . 9  class  ( f `
 x )
3331, 32, 13co 5774 . . . . . . . 8  class  ( ( f `  z )  -  ( f `  x ) )
3430, 22, 13co 5774 . . . . . . . 8  class  ( z  -  x )
35 cdiv 8439 . . . . . . . 8  class  /
3633, 34, 35co 5774 . . . . . . 7  class  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) )
3724, 29, 36cmpt 3989 . . . . . 6  class  ( z  e.  { w  e. 
dom  f  |  w #  x }  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) )
38 climc 12802 . . . . . 6  class lim CC
3937, 22, 38co 5774 . . . . 5  class  ( ( z  e.  { w  e.  dom  f  |  w #  x }  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x )
4023, 39cxp 4537 . . . 4  class  ( { x }  X.  (
( z  e.  {
w  e.  dom  f  |  w #  x }  |->  ( ( ( f `
 z )  -  ( f `  x
) )  /  (
z  -  x ) ) ) lim CC  x
) )
419, 21, 40ciun 3813 . . 3  class  U_ x  e.  ( ( int `  (
( MetOpen `  ( abs  o. 
-  ) )t  s ) ) `  dom  f
) ( { x }  X.  ( ( z  e.  { w  e. 
dom  f  |  w #  x }  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x ) )
422, 3, 5, 8, 41cmpo 5776 . 2  class  ( 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 }  |->  ( ( ( f `
 z )  -  ( f `  x
) )  /  (
z  -  x ) ) ) lim CC  x
) ) )
431, 42wceq 1331 1  wff  _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 }  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x ) ) )
Colors of variables: wff set class
This definition is referenced by:  reldvg  12827  dvfvalap  12829
  Copyright terms: Public domain W3C validator