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 24954
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 24952 . 2 class Ana
2 vs . . 3 setvar 𝑠
3 cr 10534 . . . 4 class
4 cc 10533 . . . 4 class
53, 4cpr 4552 . . 3 class {ℝ, ℂ}
6 vx . . . . . . 7 setvar 𝑥
76cv 1537 . . . . . 6 class 𝑥
8 vf . . . . . . . . . 10 setvar 𝑓
98cv 1537 . . . . . . . . 9 class 𝑓
10 cpnf 10670 . . . . . . . . . 10 class +∞
112cv 1537 . . . . . . . . . . 11 class 𝑠
12 ctayl 24951 . . . . . . . . . . 11 class Tayl
1311, 9, 12co 7149 . . . . . . . . . 10 class (𝑠 Tayl 𝑓)
1410, 7, 13co 7149 . . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)𝑥)
159, 14cin 3918 . . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
1615cdm 5542 . . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥))
17 ccnfld 20545 . . . . . . . . . 10 class fld
18 ctopn 16695 . . . . . . . . . 10 class TopOpen
1917, 18cfv 6343 . . . . . . . . 9 class (TopOpen‘ℂfld)
20 crest 16694 . . . . . . . . 9 class t
2119, 11, 20co 7149 . . . . . . . 8 class ((TopOpen‘ℂfld) ↾t 𝑠)
22 cnt 21625 . . . . . . . 8 class int
2321, 22cfv 6343 . . . . . . 7 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
2416, 23cfv 6343 . . . . . 6 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
257, 24wcel 2115 . . . . 5 wff 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
269cdm 5542 . . . . 5 class dom 𝑓
2725, 6, 26wral 3133 . . . 4 wff 𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))
28 cpm 8403 . . . . 5 class pm
294, 11, 28co 7149 . . . 4 class (ℂ ↑pm 𝑠)
3027, 8, 29crab 3137 . . 3 class {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))}
312, 5, 30cmpt 5132 . 2 class (𝑠 ∈ {ℝ, ℂ} ↦ {𝑓 ∈ (ℂ ↑pm 𝑠) ∣ ∀𝑥 ∈ dom 𝑓 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)𝑥)))})
321, 31wceq 1538 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