Definition df-ana

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)

	Ref	Expression
Assertion	df-ana	$$⊢\mathrm{Ana}=\left(s\in \left\{ℝ,ℂ\right\}⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\forall x\in \mathrm{dom}fx\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cana	$$class\mathrm{Ana}$$
1		vs	$$setvars$$
2		cr	$$classℝ$$
3		cc	$$classℂ$$
4	2 3	cpr	$$class\left\{ℝ,ℂ\right\}$$
5		vf	$$setvarf$$
6		cpm	$$class{\uparrow }_{𝑝𝑚}$$
7	1	cv	$$setvars$$
8	3 7 6	co	$$class\left(ℂ{\uparrow }_{𝑝𝑚}s\right)$$
9		vx	$$setvarx$$
10	5	cv	$$setvarf$$
11	10	cdm	$$class\mathrm{dom}f$$
12	9	cv	$$setvarx$$
13		cnt	$$class\mathrm{int}$$
14		ctopn	$$class\mathrm{TopOpen}$$
15		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
16	15 14	cfv	$$class\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
17		crest	$$class{\upharpoonright }_{𝑡}$$
18	16 7 17	co	$$class\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)$$
19	18 13	cfv	$$class\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)$$
20		cpnf	$$class\mathrm{+\infty }$$
21		ctayl	$$class\mathrm{Tayl}$$
22	7 10 21	co	$$class\left(s\mathrm{Tayl}f\right)$$
23	20 12 22	co	$$class\left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)$$
24	10 23	cin	$$class\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)$$
25	24	cdm	$$class\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)$$
26	25 19	cfv	$$class\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)$$
27	12 26	wcel	$$wffx\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)$$
28	27 9 11	wral	$$wff\forall x\in \mathrm{dom}fx\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)$$
29	28 5 8	crab	$$class\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\forall x\in \mathrm{dom}fx\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)\right\}$$
30	1 4 29	cmpt	$$class\left(s\in \left\{ℝ,ℂ\right\}⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\forall x\in \mathrm{dom}fx\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)\right\}\right)$$
31	0 30	wceq	$$wff\mathrm{Ana}=\left(s\in \left\{ℝ,ℂ\right\}⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)|\forall x\in \mathrm{dom}fx\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}s\right)\left(\mathrm{dom}\left(f\cap \left(\mathrm{+\infty }\left(s\mathrm{Tayl}f\right)x\right)\right)\right)\right\}\right)$$