Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dv Unicode version

Definition df-dv 19217
 Description: 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 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 and is well behaved when contains no isolated points, we will restrict our attention to the cases or for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.)
Assertion
Ref Expression
df-dv fldt lim
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-dv
StepHypRef Expression
1 cdv 19213 . 2
2 vs . . 3
3 vf . . 3
4 cc 8735 . . . 4
54cpw 3625 . . 3
62cv 1622 . . . 4
7 cpm 6773 . . . 4
84, 6, 7co 5858 . . 3
9 vx . . . 4
103cv 1622 . . . . . 6
1110cdm 4689 . . . . 5
12 ccnfld 16377 . . . . . . . 8 fld
13 ctopn 13326 . . . . . . . 8
1412, 13cfv 5255 . . . . . . 7 fld
15 crest 13325 . . . . . . 7 t
1614, 6, 15co 5858 . . . . . 6 fldt
17 cnt 16754 . . . . . 6
1816, 17cfv 5255 . . . . 5 fldt
1911, 18cfv 5255 . . . 4 fldt
209cv 1622 . . . . . 6
2120csn 3640 . . . . 5
22 vz . . . . . . 7
2311, 21cdif 3149 . . . . . . 7
2422cv 1622 . . . . . . . . . 10
2524, 10cfv 5255 . . . . . . . . 9
2620, 10cfv 5255 . . . . . . . . 9
27 cmin 9037 . . . . . . . . 9
2825, 26, 27co 5858 . . . . . . . 8
2924, 20, 27co 5858 . . . . . . . 8
30 cdiv 9423 . . . . . . . 8
3128, 29, 30co 5858 . . . . . . 7
3222, 23, 31cmpt 4077 . . . . . 6
33 climc 19212 . . . . . 6 lim
3432, 20, 33co 5858 . . . . 5 lim
3521, 34cxp 4687 . . . 4 lim
369, 19, 35ciun 3905 . . 3 fldt lim
372, 3, 5, 8, 36cmpt2 5860 . 2 fldt lim
381, 37wceq 1623 1 fldt lim
 Colors of variables: wff set class This definition is referenced by:  reldv  19220  dvfval  19247  dvbsss  19252  perfdvf  19253
 Copyright terms: Public domain W3C validator