Definition df-ana 26412

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

Distinct variable group:   𝑓,𝑠,𝑥

Detailed syntax breakdown of Definition df-ana

Step	Hyp	Ref	Expression
1		cana 26410	. 2 class Ana
2		vs	. . 3 setvar 𝑠
3		cr 11152	. . . 4 class ℝ
4		cc 11151	. . . 4 class ℂ
5	3, 4	cpr 4633	. . 3 class {ℝ, ℂ}
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1536	. . . . . 6 class 𝑥
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1536	. . . . . . . . 9 class 𝑓
10		cpnf 11290	. . . . . . . . . 10 class +∞
11	2	cv 1536	. . . . . . . . . . 11 class 𝑠
12		ctayl 26409	. . . . . . . . . . 11 class Tayl
13	11, 9, 12	co 7431	. . . . . . . . . 10 class (𝑠 Tayl 𝑓)
14	10, 7, 13	co 7431	. . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
15	9, 14	cin 3962	. . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
16	15	cdm 5689	. . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17		ccnfld 21382	. . . . . . . . . 10 class ℂfld
18		ctopn 17468	. . . . . . . . . 10 class TopOpen
19	17, 18	cfv 6563	. . . . . . . . 9 class (TopOpen‘ℂfld)
20		crest 17467	. . . . . . . . 9 class ↾t
21	19, 11, 20	co 7431	. . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22		cnt 23041	. . . . . . . 8 class int
23	21, 22	cfv 6563	. . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
24	16, 23	cfv 6563	. . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
25	7, 24	wcel 2106	. . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
26	9	cdm 5689	. . . . 5 class dom 𝑓
27	25, 6, 26	wral 3059	. . . 4 wff ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28		cpm 8866	. . . . 5 class ↑pm
29	4, 11, 28	co 7431	. . . 4 class (ℂ ↑pm 𝑠)
30	27, 8, 29	crab 3433	. . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
31	2, 5, 30	cmpt 5231	. 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
32	1, 31	wceq 1537	1 wff Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})

This definition is referenced by: (None)