Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dvap Unicode version

Definition df-dvap 12805
 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 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.) (Revised by Jim Kingdon, 25-Jun-2023.)
Assertion
Ref Expression
df-dvap t # lim
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-dvap
StepHypRef Expression
1 cdv 12803 . 2
2 vs . . 3
3 vf . . 3
4 cc 7625 . . . 4
54cpw 3510 . . 3
62cv 1330 . . . 4
7 cpm 6543 . . . 4
84, 6, 7co 5774 . . 3
9 vx . . . 4
103cv 1330 . . . . . 6
1110cdm 4539 . . . . 5
12 cabs 10776 . . . . . . . . 9
13 cmin 7940 . . . . . . . . 9
1412, 13ccom 4543 . . . . . . . 8
15 cmopn 12164 . . . . . . . 8
1614, 15cfv 5123 . . . . . . 7
17 crest 12130 . . . . . . 7 t
1816, 6, 17co 5774 . . . . . 6 t
19 cnt 12272 . . . . . 6
2018, 19cfv 5123 . . . . 5 t
2111, 20cfv 5123 . . . 4 t
229cv 1330 . . . . . 6
2322csn 3527 . . . . 5
24 vz . . . . . . 7
25 vw . . . . . . . . . 10
2625cv 1330 . . . . . . . . 9
27 cap 8350 . . . . . . . . 9 #
2826, 22, 27wbr 3929 . . . . . . . 8 #
2928, 25, 11crab 2420 . . . . . . 7 #
3024cv 1330 . . . . . . . . . 10
3130, 10cfv 5123 . . . . . . . . 9
3222, 10cfv 5123 . . . . . . . . 9
3331, 32, 13co 5774 . . . . . . . 8
3430, 22, 13co 5774 . . . . . . . 8
35 cdiv 8439 . . . . . . . 8
3633, 34, 35co 5774 . . . . . . 7
3724, 29, 36cmpt 3989 . . . . . 6 #
38 climc 12802 . . . . . 6 lim
3937, 22, 38co 5774 . . . . 5 # lim
4023, 39cxp 4537 . . . 4 # lim
419, 21, 40ciun 3813 . . 3 t # lim
422, 3, 5, 8, 41cmpo 5776 . 2 t # lim
431, 42wceq 1331 1 t # lim
 Colors of variables: wff set class This definition is referenced by:  reldvg  12827  dvfvalap  12829
 Copyright terms: Public domain W3C validator