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

Definition df-der 25808
 Description: Derivative of a function at . Meaningful when the domain of is an interval of , belongs to the domain of , the domain of is not and the values of are in . Bourbaki doesn't explain why he requires the domain of be an interval. Here are some hints. The domain of is an interval, belongs to the domain of and guarantee is not an isolated point in (df-islpt 25687). We have (indif2 3425) but since is not an isolated point in and what is the condition required by trfil2 17598. And in this case the class is a filter. This latter condition is required by df-flimfrs 25682 and this definition is used by df-der 25808. This sort of derivative might be extended easily to work with functions whose domain is a field and whose values are in a topological vector space whose scalars are in . The topologies would be changed accordingly. The domain of would be a neighborhood of . Experimental. (Contributed by FL, 29-May-2014.)
Assertion
Ref Expression
df-der
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-der
StepHypRef Expression
1 cder 25807 . 2
2 vn . . 3
3 vi . . 3
4 cn 9762 . . 3
5 cintvl 25799 . . 3
6 vf . . . 4
7 vp . . . 4
8 cr 8752 . . . . . 6
9 c1 8754 . . . . . . 7
102cv 1631 . . . . . . 7
11 cfz 10798 . . . . . . 7
129, 10, 11co 5874 . . . . . 6
13 cmap 6788 . . . . . 6
148, 12, 13co 5874 . . . . 5
153cv 1631 . . . . 5
1614, 15, 13co 5874 . . . 4
177cv 1631 . . . . . 6
18 vx . . . . . . 7
1917csn 3653 . . . . . . . 8
2015, 19cdif 3162 . . . . . . 7
2118cv 1631 . . . . . . . . . 10
226cv 1631 . . . . . . . . . 10
2321, 22cfv 5271 . . . . . . . . 9
2417, 22cfv 5271 . . . . . . . . 9
25 cmcv 25767 . . . . . . . . . 10
2610, 25cfv 5271 . . . . . . . . 9
2723, 24, 26co 5874 . . . . . . . 8
28 cmin 9053 . . . . . . . . 9
2921, 17, 28co 5874 . . . . . . . 8
30 cdivcv 25794 . . . . . . . . 9
3110, 30cfv 5271 . . . . . . . 8
3227, 29, 31co 5874 . . . . . . 7
3318, 20, 32cmpt 4093 . . . . . 6
3417, 33cop 3656 . . . . 5
35 cioo 10672 . . . . . . . . . . 11
3635crn 4706 . . . . . . . . . 10
37 ctg 13358 . . . . . . . . . 10
3836, 37cfv 5271 . . . . . . . . 9
3918, 12, 38cmpt 4093 . . . . . . . 8
40 ctopx 25647 . . . . . . . 8
4139, 40cfv 5271 . . . . . . 7
42 cflimfrs 25681 . . . . . . 7
4341, 38, 42co 5874 . . . . . 6
4420, 43cfv 5271 . . . . 5
4534, 44cfv 5271 . . . 4
466, 7, 16, 15, 45cmpt2 5876 . . 3
472, 3, 4, 5, 46cmpt2 5876 . 2
481, 47wceq 1632 1
 Colors of variables: wff set class This definition is referenced by:  isder  25810
 Copyright terms: Public domain W3C validator