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 ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdv class D
1 vs setvar s
2 cc class ℂ
3 2 cpw class 𝒫 ℂ
4 vf setvar f
5 cpm class ↑ 𝑝𝑚
6 1 cv setvar s
7 2 6 5 co class ℂ ↑ 𝑝𝑚 s
8 vx setvar x
9 cnt class int
10 ctopn class TopOpen
11 ccnfld class ℂ fld
12 11 10 cfv class TopOpen ⁡ ℂ fld
13 crest class ↾ 𝑡
14 12 6 13 co class TopOpen ⁡ ℂ fld ↾ 𝑡 s
15 14 9 cfv class int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s
16 4 cv setvar f
17 16 cdm class dom ⁡ f
18 17 15 cfv class int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f
19 8 cv setvar x
20 19 csn class x
21 vz setvar z
22 17 20 cdif class dom ⁡ f ∖ x
23 21 cv setvar z
24 23 16 cfv class f ⁡ z
25 cmin class −
26 19 16 cfv class f ⁡ x
27 24 26 25 co class f ⁡ z − f ⁡ x
28 cdiv class ÷
29 23 19 25 co class z − x
30 27 29 28 co class f ⁡ z − f ⁡ x z − x
31 21 22 30 cmpt class z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x
32 climc class lim ℂ
33 31 19 32 co class z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
34 20 33 cxp class x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
35 8 18 34 ciun class ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
36 1 4 3 7 35 cmpo class s ∈ 𝒫 ℂ , f ∈ ℂ ↑ 𝑝𝑚 s ⟼ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x
37 0 36 wceq wff D = s ∈ 𝒫 ℂ , f ∈ ℂ ↑ 𝑝𝑚 s ⟼ ⋃ x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f x × z ∈ dom ⁡ f ∖ x ⟼ f ⁡ z − f ⁡ x z − x lim ℂ x