Definition df-ana 23914

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 23912	. 2 class Ana
2		vs	. . 3 setvar 𝑠
3		cr 9814	. . . 4 class ℝ
4		cc 9813	. . . 4 class ℂ
5	3, 4	cpr 4127	. . 3 class {ℝ, ℂ}
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1474	. . . . . 6 class 𝑥
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1474	. . . . . . . . 9 class 𝑓
10		cpnf 9950	. . . . . . . . . 10 class +∞
11	2	cv 1474	. . . . . . . . . . 11 class 𝑠
12		ctayl 23911	. . . . . . . . . . 11 class Tayl
13	11, 9, 12	co 6549	. . . . . . . . . 10 class (𝑠 Tayl 𝑓)
14	10, 7, 13	co 6549	. . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
15	9, 14	cin 3539	. . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
16	15	cdm 5038	. . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17		ccnfld 19567	. . . . . . . . . 10 class ℂfld
18		ctopn 15905	. . . . . . . . . 10 class TopOpen
19	17, 18	cfv 5804	. . . . . . . . 9 class (TopOpen‘ℂfld)
20		crest 15904	. . . . . . . . 9 class ↾t
21	19, 11, 20	co 6549	. . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22		cnt 20631	. . . . . . . 8 class int
23	21, 22	cfv 5804	. . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
24	16, 23	cfv 5804	. . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
25	7, 24	wcel 1977	. . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
26	9	cdm 5038	. . . . 5 class dom 𝑓
27	25, 6, 26	wral 2896	. . . 4 wff ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28		cpm 7745	. . . . 5 class ↑pm
29	4, 11, 28	co 6549	. . . 4 class (ℂ ↑pm 𝑠)
30	27, 8, 29	crab 2900	. . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
31	2, 5, 30	cmpt 4643	. 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
32	1, 31	wceq 1475	1 wff Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})

This definition is referenced by: (None)