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 = ( 𝑠 ∈ { ℝ , ℂ } ↦ { 𝑓 ∈ ( ℂ ↑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 𝑓 ) 𝑥 ) ) ) } )