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 = ( 𝑠 ∈ { ℝ , ℂ } ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cana	⊢ Ana
1		vs	⊢ 𝑠
2		cr	⊢ ℝ
3		cc	⊢ ℂ
4	2 3	cpr	⊢ { ℝ , ℂ }
5		vf	⊢ 𝑓
6		cpm	⊢ ↑pm
7	1	cv	⊢ 𝑠
8	3 7 6	co	⊢ ( ℂ ↑pm 𝑠 )
9		vx	⊢ 𝑥
10	5	cv	⊢ 𝑓
11	10	cdm	⊢ dom 𝑓
12	9	cv	⊢ 𝑥
13		cnt	⊢ int
14		ctopn	⊢ TopOpen
15		ccnfld	⊢ ℂfld
16	15 14	cfv	⊢ ( TopOpen ‘ ℂfld )
17		crest	⊢ ↾t
18	16 7 17	co	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 )
19	18 13	cfv	⊢ ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) )
20		cpnf	⊢ +∞
21		ctayl	⊢ Tayl
22	7 10 21	co	⊢ ( 𝑠 Tayl 𝑓 )
23	20 12 22	co	⊢ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 )
24	10 23	cin	⊢ ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) )
25	24	cdm	⊢ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) )
26	25 19	cfv	⊢ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) )
27	12 26	wcel	⊢ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) )
28	27 9 11	wral	⊢ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) )
29	28 5 8	crab	⊢ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) }
30	1 4 29	cmpt	⊢ ( 𝑠 ∈ { ℝ , ℂ } ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) } )
31	0 30	wceq	⊢ Ana = ( 𝑠 ∈ { ℝ , ℂ } ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ∀ 𝑥 ∈ dom 𝑓 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom ( 𝑓 ∩ ( +∞ ( 𝑠 Tayl 𝑓 ) 𝑥 ) ) ) } )