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 26397
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 26395 . 2 class Ana
2 vs . . 3 setvar 𝑠
3 cr 11154 . . . 4 class
4 cc 11153 . . . 4 class
53, 4cpr 4628 . . 3 class {ℝ, ℂ}
6 vx . . . . . . 7 setvar 𝑥
76cv 1539 . . . . . 6 class 𝑥
8 vf . . . . . . . . . 10 setvar 𝑓
98cv 1539 . . . . . . . . 9 class 𝑓
10 cpnf 11292 . . . . . . . . . 10 class +∞
112cv 1539 . . . . . . . . . . 11 class 𝑠
12 ctayl 26394 . . . . . . . . . . 11 class Tayl
1311, 9, 12co 7431 . . . . . . . . . 10 class (𝑠 Tayl 𝑓)
1410, 7, 13co 7431 . . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
159, 14cin 3950 . . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
1615cdm 5685 . . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17 ccnfld 21364 . . . . . . . . . 10 class fld
18 ctopn 17466 . . . . . . . . . 10 class TopOpen
1917, 18cfv 6561 . . . . . . . . 9 class (TopOpen‘ℂfld)
20 crest 17465 . . . . . . . . 9 class t
2119, 11, 20co 7431 . . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22 cnt 23025 . . . . . . . 8 class int
2321, 22cfv 6561 . . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
2416, 23cfv 6561 . . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
257, 24wcel 2108 . . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
269cdm 5685 . . . . 5 class dom 𝑓
2725, 6, 26wral 3061 . . . 4 wff 𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28 cpm 8867 . . . . 5 class pm
294, 11, 28co 7431 . . . 4 class (ℂ ↑pm 𝑠)
3027, 8, 29crab 3436 . . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
312, 5, 30cmpt 5225 . 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
321, 31wceq 1540 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