Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-der Unicode version

Definition df-der 25705
Description: Derivative of a function  f at  p. Meaningful when the domain of  f is an interval of  RR,  p belongs to the domain of  f, the domain of  f is not  { p } and the values of  f are in  ( RR  ^m  ( 1 ... n
) ).

Bourbaki doesn't explain why he requires the domain of  f be an interval. Here are some hints. The domain of  f is an interval,  p belongs to the domain of  f and  dom  f  =  { p } guarantee  p is not an isolated point in  dom  f (df-islpt 25584). We have  ( v  i^i  ( dom  f  \  { p } ) )  =  ( ( v  i^i  dom  f
)  \  { p } ) (indif2 3412) but  ( v  i^i  dom  f )  =/=  {
p } since  p is not an isolated point in  dom  f and  ( v  i^i  ( dom  f  \  { p } ) )  =/=  (/) what is the condition required by trfil2 17582. And in this case the class  { u  |  E. v  e.  ( ( nei `  ( topGen `
 ran  (,) )
) `  { p } ) u  =  ( v  i^i  ( dom  f  \  { p } ) ) } is a filter. This latter condition is required by df-flimfrs 25579 and this definition is used by df-der 25705.

This sort of derivative might be extended easily to work with functions  f whose domain is a field  A and whose values are in a topological vector space whose scalars are in  A. The topologies would be changed accordingly. The domain of  f would be a neighborhood of  p. Experimental. (Contributed by FL, 29-May-2014.)

Assertion
Ref Expression
df-der  |-  der  =  ( n  e.  NN ,  i  e.  Intvl  |->  ( f  e.  ( ( RR 
^m  ( 1 ... n ) )  ^m  i ) ,  p  e.  i  |->  ( ( ( (  topX  `  (
x  e.  ( 1 ... n )  |->  (
topGen `  ran  (,) )
) )  fLimfrs  ( topGen ` 
ran  (,) ) ) `  ( i  \  {
p } ) ) `
 <. p ,  ( x  e.  ( i 
\  { p }
)  |->  ( ( ( f `  x ) (  - cv  `  n
) ( f `  p ) ) ( / cv `  n
) ( x  -  p ) ) )
>. ) ) )
Distinct variable group:    i, n, f, p, x

Detailed syntax breakdown of Definition df-der
StepHypRef Expression
1 cder 25704 . 2  class  der
2 vn . . 3  set  n
3 vi . . 3  set  i
4 cn 9746 . . 3  class  NN
5 cintvl 25696 . . 3  class  Intvl
6 vf . . . 4  set  f
7 vp . . . 4  set  p
8 cr 8736 . . . . . 6  class  RR
9 c1 8738 . . . . . . 7  class  1
102cv 1622 . . . . . . 7  class  n
11 cfz 10782 . . . . . . 7  class  ...
129, 10, 11co 5858 . . . . . 6  class  ( 1 ... n )
13 cmap 6772 . . . . . 6  class  ^m
148, 12, 13co 5858 . . . . 5  class  ( RR 
^m  ( 1 ... n ) )
153cv 1622 . . . . 5  class  i
1614, 15, 13co 5858 . . . 4  class  ( ( RR  ^m  ( 1 ... n ) )  ^m  i )
177cv 1622 . . . . . 6  class  p
18 vx . . . . . . 7  set  x
1917csn 3640 . . . . . . . 8  class  { p }
2015, 19cdif 3149 . . . . . . 7  class  ( i 
\  { p }
)
2118cv 1622 . . . . . . . . . 10  class  x
226cv 1622 . . . . . . . . . 10  class  f
2321, 22cfv 5255 . . . . . . . . 9  class  ( f `
 x )
2417, 22cfv 5255 . . . . . . . . 9  class  ( f `
 p )
25 cmcv 25664 . . . . . . . . . 10  class  - cv
2610, 25cfv 5255 . . . . . . . . 9  class  (  - cv  `  n )
2723, 24, 26co 5858 . . . . . . . 8  class  ( ( f `  x ) (  - cv  `  n
) ( f `  p ) )
28 cmin 9037 . . . . . . . . 9  class  -
2921, 17, 28co 5858 . . . . . . . 8  class  ( x  -  p )
30 cdivcv 25691 . . . . . . . . 9  class  / cv
3110, 30cfv 5255 . . . . . . . 8  class  ( / cv `  n )
3227, 29, 31co 5858 . . . . . . 7  class  ( ( ( f `  x
) (  - cv  `  n ) ( f `
 p ) ) ( / cv `  n
) ( x  -  p ) )
3318, 20, 32cmpt 4077 . . . . . 6  class  ( x  e.  ( i  \  { p } ) 
|->  ( ( ( f `
 x ) (  - cv  `  n
) ( f `  p ) ) ( / cv `  n
) ( x  -  p ) ) )
3417, 33cop 3643 . . . . 5  class  <. p ,  ( x  e.  ( i  \  {
p } )  |->  ( ( ( f `  x ) (  - cv  `  n ) ( f `  p ) ) ( / cv `  n ) ( x  -  p ) ) ) >.
35 cioo 10656 . . . . . . . . . . 11  class  (,)
3635crn 4690 . . . . . . . . . 10  class  ran  (,)
37 ctg 13342 . . . . . . . . . 10  class  topGen
3836, 37cfv 5255 . . . . . . . . 9  class  ( topGen ` 
ran  (,) )
3918, 12, 38cmpt 4077 . . . . . . . 8  class  ( x  e.  ( 1 ... n )  |->  ( topGen ` 
ran  (,) ) )
40 ctopx 25544 . . . . . . . 8  class  topX
4139, 40cfv 5255 . . . . . . 7  class  (  topX  `  ( x  e.  ( 1 ... n ) 
|->  ( topGen `  ran  (,) )
) )
42 cflimfrs 25578 . . . . . . 7  class  fLimfrs
4341, 38, 42co 5858 . . . . . 6  class  ( ( 
topX  `  ( x  e.  ( 1 ... n
)  |->  ( topGen `  ran  (,) ) ) )  fLimfrs  (
topGen `  ran  (,) )
)
4420, 43cfv 5255 . . . . 5  class  ( ( (  topX  `  ( x  e.  ( 1 ... n )  |->  ( topGen ` 
ran  (,) ) ) ) 
fLimfrs  ( topGen `  ran  (,) )
) `  ( i  \  { p } ) )
4534, 44cfv 5255 . . . 4  class  ( ( ( (  topX  `  (
x  e.  ( 1 ... n )  |->  (
topGen `  ran  (,) )
) )  fLimfrs  ( topGen ` 
ran  (,) ) ) `  ( i  \  {
p } ) ) `
 <. p ,  ( x  e.  ( i 
\  { p }
)  |->  ( ( ( f `  x ) (  - cv  `  n
) ( f `  p ) ) ( / cv `  n
) ( x  -  p ) ) )
>. )
466, 7, 16, 15, 45cmpt2 5860 . . 3  class  ( f  e.  ( ( RR 
^m  ( 1 ... n ) )  ^m  i ) ,  p  e.  i  |->  ( ( ( (  topX  `  (
x  e.  ( 1 ... n )  |->  (
topGen `  ran  (,) )
) )  fLimfrs  ( topGen ` 
ran  (,) ) ) `  ( i  \  {
p } ) ) `
 <. p ,  ( x  e.  ( i 
\  { p }
)  |->  ( ( ( f `  x ) (  - cv  `  n
) ( f `  p ) ) ( / cv `  n
) ( x  -  p ) ) )
>. ) )
472, 3, 4, 5, 46cmpt2 5860 . 2  class  ( n  e.  NN ,  i  e.  Intvl  |->  ( f  e.  ( ( RR  ^m  ( 1 ... n
) )  ^m  i
) ,  p  e.  i  |->  ( ( ( (  topX  `  ( x  e.  ( 1 ... n )  |->  ( topGen ` 
ran  (,) ) ) ) 
fLimfrs  ( topGen `  ran  (,) )
) `  ( i  \  { p } ) ) `  <. p ,  ( x  e.  ( i  \  {
p } )  |->  ( ( ( f `  x ) (  - cv  `  n ) ( f `  p ) ) ( / cv `  n ) ( x  -  p ) ) ) >. ) ) )
481, 47wceq 1623 1  wff  der  =  ( n  e.  NN ,  i  e.  Intvl  |->  ( f  e.  ( ( RR 
^m  ( 1 ... n ) )  ^m  i ) ,  p  e.  i  |->  ( ( ( (  topX  `  (
x  e.  ( 1 ... n )  |->  (
topGen `  ran  (,) )
) )  fLimfrs  ( topGen ` 
ran  (,) ) ) `  ( i  \  {
p } ) ) `
 <. p ,  ( x  e.  ( i 
\  { p }
)  |->  ( ( ( f `  x ) (  - cv  `  n
) ( f `  p ) ) ( / cv `  n
) ( x  -  p ) ) )
>. ) ) )
Colors of variables: wff set class
This definition is referenced by:  isder  25707
  Copyright terms: Public domain W3C validator