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

Definition df-ana 19751
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 19749 . 2  class Ana
2 vs . . 3  set  s
3 cr 8752 . . . 4  class  RR
4 cc 8751 . . . 4  class  CC
53, 4cpr 3654 . . 3  class  { RR ,  CC }
6 vx . . . . . . 7  set  x
76cv 1631 . . . . . 6  class  x
8 vf . . . . . . . . . 10  set  f
98cv 1631 . . . . . . . . 9  class  f
10 cpnf 8880 . . . . . . . . . 10  class  +oo
112cv 1631 . . . . . . . . . . 11  class  s
12 ctayl 19748 . . . . . . . . . . 11  class Tayl
1311, 9, 12co 5874 . . . . . . . . . 10  class  ( s Tayl  f )
1410, 7, 13co 5874 . . . . . . . . 9  class  (  +oo ( s Tayl  f )
x )
159, 14cin 3164 . . . . . . . 8  class  ( f  i^i  (  +oo (
s Tayl  f ) x ) )
1615cdm 4705 . . . . . . 7  class  dom  (
f  i^i  (  +oo ( s Tayl  f )
x ) )
17 ccnfld 16393 . . . . . . . . . 10  classfld
18 ctopn 13342 . . . . . . . . . 10  class  TopOpen
1917, 18cfv 5271 . . . . . . . . 9  class  ( TopOpen ` fld )
20 crest 13341 . . . . . . . . 9  classt
2119, 11, 20co 5874 . . . . . . . 8  class  ( (
TopOpen ` fld )t  s )
22 cnt 16770 . . . . . . . 8  class  int
2321, 22cfv 5271 . . . . . . 7  class  ( int `  ( ( TopOpen ` fld )t  s ) )
2416, 23cfv 5271 . . . . . 6  class  ( ( int `  ( (
TopOpen ` fld )t  s ) ) `  dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
257, 24wcel 1696 . . . . 5  wff  x  e.  ( ( int `  (
( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
269cdm 4705 . . . . 5  class  dom  f
2725, 6, 26wral 2556 . . . 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 6789 . . . . 5  class  ^pm
294, 11, 28co 5874 . . . 4  class  ( CC 
^pm  s )
3027, 8, 29crab 2560 . . 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 4093 . 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 1632 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