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

Definition df-dv 19756
 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 19752 . 2
2 vs . . 3
3 vf . . 3
4 cc 8990 . . . 4
54cpw 3801 . . 3
62cv 1652 . . . 4
7 cpm 7021 . . . 4
84, 6, 7co 6083 . . 3
9 vx . . . 4
103cv 1652 . . . . . 6
1110cdm 4880 . . . . 5
12 ccnfld 16705 . . . . . . . 8 fld
13 ctopn 13651 . . . . . . . 8
1412, 13cfv 5456 . . . . . . 7 fld
15 crest 13650 . . . . . . 7 t
1614, 6, 15co 6083 . . . . . 6 fldt
17 cnt 17083 . . . . . 6
1816, 17cfv 5456 . . . . 5 fldt
1911, 18cfv 5456 . . . 4 fldt
209cv 1652 . . . . . 6
2120csn 3816 . . . . 5
22 vz . . . . . . 7
2311, 21cdif 3319 . . . . . . 7
2422cv 1652 . . . . . . . . . 10
2524, 10cfv 5456 . . . . . . . . 9
2620, 10cfv 5456 . . . . . . . . 9
27 cmin 9293 . . . . . . . . 9
2825, 26, 27co 6083 . . . . . . . 8
2924, 20, 27co 6083 . . . . . . . 8
30 cdiv 9679 . . . . . . . 8
3128, 29, 30co 6083 . . . . . . 7
3222, 23, 31cmpt 4268 . . . . . 6
33 climc 19751 . . . . . 6 lim
3432, 20, 33co 6083 . . . . 5 lim
3521, 34cxp 4878 . . . 4 lim
369, 19, 35ciun 4095 . . 3 fldt lim
372, 3, 5, 8, 36cmpt2 6085 . 2 fldt lim
381, 37wceq 1653 1 fldt lim
 Colors of variables: wff set class This definition is referenced by:  reldv  19759  dvfval  19786  dvbsss  19791  perfdvf  19792
 Copyright terms: Public domain W3C validator