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

Definition df-ana 20274
 Description: Define the set of analytic functions, which are functions such that the Taylor series of the function at each point converges to the function in some neighborhood of the point. (Contributed by Mario Carneiro, 31-Dec-2016.)
Assertion
Ref Expression
df-ana Ana fldt Tayl
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ana
StepHypRef Expression
1 cana 20272 . 2 Ana
2 vs . . 3
3 cr 8991 . . . 4
4 cc 8990 . . . 4
53, 4cpr 3817 . . 3
6 vx . . . . . . 7
76cv 1652 . . . . . 6
8 vf . . . . . . . . . 10
98cv 1652 . . . . . . . . 9
10 cpnf 9119 . . . . . . . . . 10
112cv 1652 . . . . . . . . . . 11
12 ctayl 20271 . . . . . . . . . . 11 Tayl
1311, 9, 12co 6083 . . . . . . . . . 10 Tayl
1410, 7, 13co 6083 . . . . . . . . 9 Tayl
159, 14cin 3321 . . . . . . . 8 Tayl
1615cdm 4880 . . . . . . 7 Tayl
17 ccnfld 16705 . . . . . . . . . 10 fld
18 ctopn 13651 . . . . . . . . . 10
1917, 18cfv 5456 . . . . . . . . 9 fld
20 crest 13650 . . . . . . . . 9 t
2119, 11, 20co 6083 . . . . . . . 8 fldt
22 cnt 17083 . . . . . . . 8
2321, 22cfv 5456 . . . . . . 7 fldt
2416, 23cfv 5456 . . . . . 6 fldt Tayl
257, 24wcel 1726 . . . . 5 fldt Tayl
269cdm 4880 . . . . 5
2725, 6, 26wral 2707 . . . 4 fldt Tayl
28 cpm 7021 . . . . 5
294, 11, 28co 6083 . . . 4
3027, 8, 29crab 2711 . . 3 fldt Tayl
312, 5, 30cmpt 4268 . 2 fldt Tayl
321, 31wceq 1653 1 Ana fldt Tayl
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator