Metamath Proof Explorer

Definition df-ana

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)

Ref Expression
Assertion df-ana 
|- Ana = ( s e. { RR , CC } |-> { f e. ( CC ^pm s ) | A. x e. dom f x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cana 
 |-  Ana
1 vs 
 |-  s
2 cr 
 |-  RR
3 cc 
 |-  CC
4 2 3 cpr 
 |-  { RR , CC }
5 vf 
 |-  f
6 cpm 
 |-  ^pm
7 1 cv 
 |-  s
8 3 7 6 co 
 |-  ( CC ^pm s )
9 vx 
 |-  x
10 5 cv 
 |-  f
11 10 cdm 
 |-  dom f
12 9 cv 
 |-  x
13 cnt 
 |-  int
14 ctopn 
 |-  TopOpen
15 ccnfld 
 |-  CCfld
16 15 14 cfv 
 |-  ( TopOpen ` CCfld )
17 crest 
 |-  |`t
18 16 7 17 co 
 |-  ( ( TopOpen ` CCfld ) |`t s )
19 18 13 cfv 
 |-  ( int ` ( ( TopOpen ` CCfld ) |`t s ) )
20 cpnf 
 |-  +oo
21 ctayl 
 |-  Tayl
22 7 10 21 co 
 |-  ( s Tayl f )
23 20 12 22 co 
 |-  ( +oo ( s Tayl f ) x )
24 10 23 cin 
 |-  ( f i^i ( +oo ( s Tayl f ) x ) )
25 24 cdm 
 |-  dom ( f i^i ( +oo ( s Tayl f ) x ) )
26 25 19 cfv 
 |-  ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) )
27 12 26 wcel 
 |-  x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) )
28 27 9 11 wral 
 |-  A. x e. dom f x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) )
29 28 5 8 crab 
 |-  { f e. ( CC ^pm s ) | A. x e. dom f x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) ) }
30 1 4 29 cmpt 
 |-  ( s e. { RR , CC } |-> { f e. ( CC ^pm s ) | A. x e. dom f x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) ) } )
31 0 30 wceq 
 |-  Ana = ( s e. { RR , CC } |-> { f e. ( CC ^pm s ) | A. x e. dom f x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) ) } )