Definition df-ana 24110

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

Step	Hyp	Ref	Expression
1		cana 24108	. 2 class Ana
2		vs	. . 3 setvar s
3		cr 9935	. . . 4 class RR
4		cc 9934	. . . 4 class CC
5	3, 4	cpr 4179	. . 3 class { RR , CC }
6		vx	. . . . . . 7 setvar x
7	6	cv 1482	. . . . . 6 class x
8		vf	. . . . . . . . . 10 setvar f
9	8	cv 1482	. . . . . . . . 9 class f
10		cpnf 10071	. . . . . . . . . 10 class +oo
11	2	cv 1482	. . . . . . . . . . 11 class s
12		ctayl 24107	. . . . . . . . . . 11 class Tayl
13	11, 9, 12	co 6650	. . . . . . . . . 10 class ( s Tayl f )
14	10, 7, 13	co 6650	. . . . . . . . 9 class ( +oo ( s Tayl f ) x )
15	9, 14	cin 3573	. . . . . . . 8 class ( f i^i ( +oo ( s Tayl f ) x ) )
16	15	cdm 5114	. . . . . . 7 class dom ( f i^i ( +oo ( s Tayl f ) x ) )
17		ccnfld 19746	. . . . . . . . . 10 class ℂfld
18		ctopn 16082	. . . . . . . . . 10 class TopOpen
19	17, 18	cfv 5888	. . . . . . . . 9 class ( TopOpen ` ℂfld )
20		crest 16081	. . . . . . . . 9 class ↾t
21	19, 11, 20	co 6650	. . . . . . . 8 class ( ( TopOpen ` ℂfld ) ↾t s )
22		cnt 20821	. . . . . . . 8 class int
23	21, 22	cfv 5888	. . . . . . 7 class ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) )
24	16, 23	cfv 5888	. . . . . 6 class ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) )
25	7, 24	wcel 1990	. . . . 5 wff x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom ( f i^i ( +oo ( s Tayl f ) x ) ) )
26	9	cdm 5114	. . . . 5 class dom f
27	25, 6, 26	wral 2912	. . . 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 7858	. . . . 5 class ^pm
29	4, 11, 28	co 6650	. . . 4 class ( CC ^pm s )
30	27, 8, 29	crab 2916	. . 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 ) ) ) }
31	2, 5, 30	cmpt 4729	. 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 ) ) ) } )
32	1, 31	wceq 1483	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 ) ) ) } )

This definition is referenced by: (None)