Metamath Proof Explorer


Definition df-dv

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)

Ref Expression
Assertion df-dv โŠขD=sโˆˆ๐’ซโ„‚,fโˆˆโ„‚โ†‘๐‘๐‘šsโŸผโ‹ƒxโˆˆintโกTopOpenโกโ„‚fldโ†พ๐‘กsโกdomโกfxร—zโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’xlimโ„‚x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdv classD
1 vs setvars
2 cc classโ„‚
3 2 cpw class๐’ซโ„‚
4 vf setvarf
5 cpm classโ†‘๐‘๐‘š
6 1 cv setvars
7 2 6 5 co classโ„‚โ†‘๐‘๐‘šs
8 vx setvarx
9 cnt classint
10 ctopn classTopOpen
11 ccnfld classโ„‚fld
12 11 10 cfv classTopOpenโกโ„‚fld
13 crest classโ†พ๐‘ก
14 12 6 13 co classTopOpenโกโ„‚fldโ†พ๐‘กs
15 14 9 cfv classintโกTopOpenโกโ„‚fldโ†พ๐‘กs
16 4 cv setvarf
17 16 cdm classdomโกf
18 17 15 cfv classintโกTopOpenโกโ„‚fldโ†พ๐‘กsโกdomโกf
19 8 cv setvarx
20 19 csn classx
21 vz setvarz
22 17 20 cdif classdomโกfโˆ–x
23 21 cv setvarz
24 23 16 cfv classfโกz
25 cmin classโˆ’
26 19 16 cfv classfโกx
27 24 26 25 co classfโกzโˆ’fโกx
28 cdiv classรท
29 23 19 25 co classzโˆ’x
30 27 29 28 co classfโกzโˆ’fโกxzโˆ’x
31 21 22 30 cmpt classzโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’x
32 climc classlimโ„‚
33 31 19 32 co classzโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’xlimโ„‚x
34 20 33 cxp classxร—zโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’xlimโ„‚x
35 8 18 34 ciun classโ‹ƒxโˆˆintโกTopOpenโกโ„‚fldโ†พ๐‘กsโกdomโกfxร—zโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’xlimโ„‚x
36 1 4 3 7 35 cmpo classsโˆˆ๐’ซโ„‚,fโˆˆโ„‚โ†‘๐‘๐‘šsโŸผโ‹ƒxโˆˆintโกTopOpenโกโ„‚fldโ†พ๐‘กsโกdomโกfxร—zโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’xlimโ„‚x
37 0 36 wceq wffD=sโˆˆ๐’ซโ„‚,fโˆˆโ„‚โ†‘๐‘๐‘šsโŸผโ‹ƒxโˆˆintโกTopOpenโกโ„‚fldโ†พ๐‘กsโกdomโกfxร—zโˆˆdomโกfโˆ–xโŸผfโกzโˆ’fโกxzโˆ’xlimโ„‚x