MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ana Structured version   Visualization version   GIF version

Definition df-ana 25713
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
StepHypRef Expression
1 cana 25711 . 2 class Ana
2 vs . . 3 setvar 𝑠
3 cr 11049 . . . 4 class
4 cc 11048 . . . 4 class
53, 4cpr 4588 . . 3 class {ℝ, ℂ}
6 vx . . . . . . 7 setvar 𝑥
76cv 1540 . . . . . 6 class 𝑥
8 vf . . . . . . . . . 10 setvar 𝑓
98cv 1540 . . . . . . . . 9 class 𝑓
10 cpnf 11185 . . . . . . . . . 10 class +∞
112cv 1540 . . . . . . . . . . 11 class 𝑠
12 ctayl 25710 . . . . . . . . . . 11 class Tayl
1311, 9, 12co 7356 . . . . . . . . . 10 class (𝑠 Tayl 𝑓)
1410, 7, 13co 7356 . . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
159, 14cin 3909 . . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
1615cdm 5633 . . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17 ccnfld 20794 . . . . . . . . . 10 class fld
18 ctopn 17302 . . . . . . . . . 10 class TopOpen
1917, 18cfv 6496 . . . . . . . . 9 class (TopOpen‘ℂfld)
20 crest 17301 . . . . . . . . 9 class t
2119, 11, 20co 7356 . . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22 cnt 22366 . . . . . . . 8 class int
2321, 22cfv 6496 . . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
2416, 23cfv 6496 . . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
257, 24wcel 2106 . . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
269cdm 5633 . . . . 5 class dom 𝑓
2725, 6, 26wral 3064 . . . 4 wff 𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28 cpm 8765 . . . . 5 class pm
294, 11, 28co 7356 . . . 4 class (ℂ ↑pm 𝑠)
3027, 8, 29crab 3407 . . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
312, 5, 30cmpt 5188 . 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
321, 31wceq 1541 1 wff Ana = (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator