Definition df-ana 26339

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 26337	. 2 class Ana
2		vs	. . 3 setvar 𝑠
3		cr 11028	. . . 4 class ℝ
4		cc 11027	. . . 4 class ℂ
5	3, 4	cpr 4557	. . 3 class {ℝ, ℂ}
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1546	. . . . . 6 class 𝑥
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1546	. . . . . . . . 9 class 𝑓
10		cpnf 11167	. . . . . . . . . 10 class +∞
11	2	cv 1546	. . . . . . . . . . 11 class 𝑠
12		ctayl 26336	. . . . . . . . . . 11 class Tayl
13	11, 9, 12	co 7356	. . . . . . . . . 10 class (𝑠 Tayl 𝑓)
14	10, 7, 13	co 7356	. . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
15	9, 14	cin 3882	. . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
16	15	cdm 5618	. . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17		ccnfld 21347	. . . . . . . . . 10 class ℂfld
18		ctopn 17375	. . . . . . . . . 10 class TopOpen
19	17, 18	cfv 6485	. . . . . . . . 9 class (TopOpen‘ℂfld)
20		crest 17374	. . . . . . . . 9 class ↾t
21	19, 11, 20	co 7356	. . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22		cnt 23000	. . . . . . . 8 class int
23	21, 22	cfv 6485	. . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
24	16, 23	cfv 6485	. . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
25	7, 24	wcel 2119	. . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
26	9	cdm 5618	. . . . 5 class dom 𝑓
27	25, 6, 26	wral 3053	. . . 4 wff ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28		cpm 8764	. . . . 5 class ↑pm
29	4, 11, 28	co 7356	. . . 4 class (ℂ ↑pm 𝑠)
30	27, 8, 29	crab 3391	. . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
31	2, 5, 30	cmpt 5153	. 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
32	1, 31	wceq 1547	1 wff Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})

This definition is referenced by: (None)