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 ∈ ℝ ℂ ⟼ f ∈ ℂ ↑ 𝑝𝑚 s | ∀ x ∈ dom ⁡ f x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cana class Ana
1 vs setvar s
2 cr class ℝ
3 cc class ℂ
4 2 3 cpr class ℝ ℂ
5 vf setvar f
6 cpm class ↑ 𝑝𝑚
7 1 cv setvar s
8 3 7 6 co class ℂ ↑ 𝑝𝑚 s
9 vx setvar x
10 5 cv setvar f
11 10 cdm class dom ⁡ f
12 9 cv setvar x
13 cnt class int
14 ctopn class TopOpen
15 ccnfld class ℂ fld
16 15 14 cfv class TopOpen ⁡ ℂ fld
17 crest class ↾ 𝑡
18 16 7 17 co class TopOpen ⁡ ℂ fld ↾ 𝑡 s
19 18 13 cfv class int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s
20 cpnf class +∞
21 ctayl class Tayl
22 7 10 21 co class s Tayl f
23 20 12 22 co class +∞ s Tayl f x
24 10 23 cin class f ∩ +∞ s Tayl f x
25 24 cdm class dom ⁡ f ∩ +∞ s Tayl f x
26 25 19 cfv class int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x
27 12 26 wcel wff x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x
28 27 9 11 wral wff ∀ x ∈ dom ⁡ f x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x
29 28 5 8 crab class f ∈ ℂ ↑ 𝑝𝑚 s | ∀ x ∈ dom ⁡ f x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x
30 1 4 29 cmpt class s ∈ ℝ ℂ ⟼ f ∈ ℂ ↑ 𝑝𝑚 s | ∀ x ∈ dom ⁡ f x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x
31 0 30 wceq wff Ana = s ∈ ℝ ℂ ⟼ f ∈ ℂ ↑ 𝑝𝑚 s | ∀ x ∈ dom ⁡ f x ∈ int ⁡ TopOpen ⁡ ℂ fld ↾ 𝑡 s ⁡ dom ⁡ f ∩ +∞ s Tayl f x