Definition df-ana 26499

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 26497	. 2 class Ana
2		vs	. . 3 setvar 𝑠
3		cr 11102	. . . 4 class ℝ
4		cc 11101	. . . 4 class ℂ
5	3, 4	cpr 4596	. . 3 class {ℝ, ℂ}
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1567	. . . . . 6 class 𝑥
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1567	. . . . . . . . 9 class 𝑓
10		cpnf 11243	. . . . . . . . . 10 class +∞
11	2	cv 1567	. . . . . . . . . . 11 class 𝑠
12		ctayl 26496	. . . . . . . . . . 11 class Tayl
13	11, 9, 12	co 7414	. . . . . . . . . 10 class (𝑠 Tayl 𝑓)
14	10, 7, 13	co 7414	. . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
15	9, 14	cin 3912	. . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
16	15	cdm 5665	. . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17		ccnfld 21505	. . . . . . . . . 10 class ℂfld
18		ctopn 17477	. . . . . . . . . 10 class TopOpen
19	17, 18	cfv 6540	. . . . . . . . 9 class (TopOpen‘ℂfld)
20		crest 17476	. . . . . . . . 9 class ↾t
21	19, 11, 20	co 7414	. . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22		cnt 23157	. . . . . . . 8 class int
23	21, 22	cfv 6540	. . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
24	16, 23	cfv 6540	. . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
25	7, 24	wcel 2150	. . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
26	9	cdm 5665	. . . . 5 class dom 𝑓
27	25, 6, 26	wral 3086	. . . 4 wff ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28		cpm 8828	. . . . 5 class ↑pm
29	4, 11, 28	co 7414	. . . 4 class (ℂ ↑pm 𝑠)
30	27, 8, 29	crab 3423	. . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
31	2, 5, 30	cmpt 5197	. 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
32	1, 31	wceq 1568	1 wff Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})

This definition is referenced by: (None)