Definition df-ana 24946

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 24944	. 2 class Ana
2		vs	. . 3 setvar 𝑠
3		cr 10538	. . . 4 class ℝ
4		cc 10537	. . . 4 class ℂ
5	3, 4	cpr 4571	. . 3 class {ℝ, ℂ}
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1536	. . . . . 6 class 𝑥
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1536	. . . . . . . . 9 class 𝑓
10		cpnf 10674	. . . . . . . . . 10 class +∞
11	2	cv 1536	. . . . . . . . . . 11 class 𝑠
12		ctayl 24943	. . . . . . . . . . 11 class Tayl
13	11, 9, 12	co 7158	. . . . . . . . . 10 class (𝑠 Tayl 𝑓)
14	10, 7, 13	co 7158	. . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
15	9, 14	cin 3937	. . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
16	15	cdm 5557	. . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17		ccnfld 20547	. . . . . . . . . 10 class ℂfld
18		ctopn 16697	. . . . . . . . . 10 class TopOpen
19	17, 18	cfv 6357	. . . . . . . . 9 class (TopOpen‘ℂfld)
20		crest 16696	. . . . . . . . 9 class ↾t
21	19, 11, 20	co 7158	. . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22		cnt 21627	. . . . . . . 8 class int
23	21, 22	cfv 6357	. . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
24	16, 23	cfv 6357	. . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
25	7, 24	wcel 2114	. . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
26	9	cdm 5557	. . . . 5 class dom 𝑓
27	25, 6, 26	wral 3140	. . . 4 wff ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28		cpm 8409	. . . . 5 class ↑pm
29	4, 11, 28	co 7158	. . . 4 class (ℂ ↑pm 𝑠)
30	27, 8, 29	crab 3144	. . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
31	2, 5, 30	cmpt 5148	. 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)