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

Definition df-ana 19735
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  =  ( s  e.  { RR ,  CC }  |->  { f  e.  ( CC  ^pm  s )  |  A. x  e.  dom  f  x  e.  ( ( int `  ( ( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) ) } )
Distinct variable group:    f, s, x

Detailed syntax breakdown of Definition df-ana
StepHypRef Expression
1 cana 19733 . 2  class Ana
2 vs . . 3  set  s
3 cr 8736 . . . 4  class  RR
4 cc 8735 . . . 4  class  CC
53, 4cpr 3641 . . 3  class  { RR ,  CC }
6 vx . . . . . . 7  set  x
76cv 1622 . . . . . 6  class  x
8 vf . . . . . . . . . 10  set  f
98cv 1622 . . . . . . . . 9  class  f
10 cpnf 8864 . . . . . . . . . 10  class  +oo
112cv 1622 . . . . . . . . . . 11  class  s
12 ctayl 19732 . . . . . . . . . . 11  class Tayl
1311, 9, 12co 5858 . . . . . . . . . 10  class  ( s Tayl  f )
1410, 7, 13co 5858 . . . . . . . . 9  class  (  +oo ( s Tayl  f )
x )
159, 14cin 3151 . . . . . . . 8  class  ( f  i^i  (  +oo (
s Tayl  f ) x ) )
1615cdm 4689 . . . . . . 7  class  dom  (
f  i^i  (  +oo ( s Tayl  f )
x ) )
17 ccnfld 16377 . . . . . . . . . 10  classfld
18 ctopn 13326 . . . . . . . . . 10  class  TopOpen
1917, 18cfv 5255 . . . . . . . . 9  class  ( TopOpen ` fld )
20 crest 13325 . . . . . . . . 9  classt
2119, 11, 20co 5858 . . . . . . . 8  class  ( (
TopOpen ` fld )t  s )
22 cnt 16754 . . . . . . . 8  class  int
2321, 22cfv 5255 . . . . . . 7  class  ( int `  ( ( TopOpen ` fld )t  s ) )
2416, 23cfv 5255 . . . . . 6  class  ( ( int `  ( (
TopOpen ` fld )t  s ) ) `  dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
257, 24wcel 1684 . . . . 5  wff  x  e.  ( ( int `  (
( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
269cdm 4689 . . . . 5  class  dom  f
2725, 6, 26wral 2543 . . . 4  wff  A. x  e.  dom  f  x  e.  ( ( int `  (
( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
28 cpm 6773 . . . . 5  class  ^pm
294, 11, 28co 5858 . . . 4  class  ( CC 
^pm  s )
3027, 8, 29crab 2547 . . 3  class  { f  e.  ( CC  ^pm  s )  |  A. x  e.  dom  f  x  e.  ( ( int `  ( ( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) ) }
312, 5, 30cmpt 4077 . 2  class  ( s  e.  { RR ,  CC }  |->  { f  e.  ( CC  ^pm  s
)  |  A. x  e.  dom  f  x  e.  ( ( int `  (
( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) ) } )
321, 31wceq 1623 1  wff Ana  =  ( s  e.  { RR ,  CC }  |->  { f  e.  ( CC  ^pm  s )  |  A. x  e.  dom  f  x  e.  ( ( int `  ( ( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator