MPE Home 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  =  ( 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 20272 . 2  class Ana
2 vs . . 3  set  s
3 cr 8991 . . . 4  class  RR
4 cc 8990 . . . 4  class  CC
53, 4cpr 3817 . . 3  class  { RR ,  CC }
6 vx . . . . . . 7  set  x
76cv 1652 . . . . . 6  class  x
8 vf . . . . . . . . . 10  set  f
98cv 1652 . . . . . . . . 9  class  f
10 cpnf 9119 . . . . . . . . . 10  class  +oo
112cv 1652 . . . . . . . . . . 11  class  s
12 ctayl 20271 . . . . . . . . . . 11  class Tayl
1311, 9, 12co 6083 . . . . . . . . . 10  class  ( s Tayl  f )
1410, 7, 13co 6083 . . . . . . . . 9  class  (  +oo ( s Tayl  f )
x )
159, 14cin 3321 . . . . . . . 8  class  ( f  i^i  (  +oo (
s Tayl  f ) x ) )
1615cdm 4880 . . . . . . 7  class  dom  (
f  i^i  (  +oo ( s Tayl  f )
x ) )
17 ccnfld 16705 . . . . . . . . . 10  classfld
18 ctopn 13651 . . . . . . . . . 10  class  TopOpen
1917, 18cfv 5456 . . . . . . . . 9  class  ( TopOpen ` fld )
20 crest 13650 . . . . . . . . 9  classt
2119, 11, 20co 6083 . . . . . . . 8  class  ( (
TopOpen ` fld )t  s )
22 cnt 17083 . . . . . . . 8  class  int
2321, 22cfv 5456 . . . . . . 7  class  ( int `  ( ( TopOpen ` fld )t  s ) )
2416, 23cfv 5456 . . . . . 6  class  ( ( int `  ( (
TopOpen ` fld )t  s ) ) `  dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
257, 24wcel 1726 . . . . 5  wff  x  e.  ( ( int `  (
( TopOpen ` fld )t  s ) ) `
 dom  ( f  i^i  (  +oo ( s Tayl  f ) x ) ) )
269cdm 4880 . . . . 5  class  dom  f
2725, 6, 26wral 2707 . . . 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 7021 . . . . 5  class  ^pm
294, 11, 28co 6083 . . . 4  class  ( CC 
^pm  s )
3027, 8, 29crab 2711 . . 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 4268 . 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 1653 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