# Metamath Proof Explorer

## 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(ℂ{↑}_{𝑝𝑚}{s}\right)|\forall {x}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{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 ${setvar}{s}$
2 cr ${class}ℝ$
3 cc ${class}ℂ$
4 2 3 cpr ${class}\left\{ℝ,ℂ\right\}$
5 vf ${setvar}{f}$
6 cpm ${class}{↑}_{𝑝𝑚}$
7 1 cv ${setvar}{s}$
8 3 7 6 co ${class}\left(ℂ{↑}_{𝑝𝑚}{s}\right)$
9 vx ${setvar}{x}$
10 5 cv ${setvar}{f}$
11 10 cdm ${class}\mathrm{dom}{f}$
12 9 cv ${setvar}{x}$
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}{↾}_{𝑡}$
18 16 7 17 co ${class}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{s}\right)$
19 18 13 cfv ${class}\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{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){↾}_{𝑡}{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 ${wff}{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{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}{f}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{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(ℂ{↑}_{𝑝𝑚}{s}\right)|\forall {x}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{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(ℂ{↑}_{𝑝𝑚}{s}\right)|\forall {x}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{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(ℂ{↑}_{𝑝𝑚}{s}\right)|\forall {x}\in \mathrm{dom}{f}\phantom{\rule{.4em}{0ex}}{x}\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{s}\right)\left(\mathrm{dom}\left({f}\cap \left(\mathrm{+\infty }\left({s}\mathrm{Tayl}{f}\right){x}\right)\right)\right)\right\}\right)$