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 25731
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 25729 . 2 class Ana
2 vs . . 3 setvar 𝑠
3 cr 11057 . . . 4 class ℝ
4 cc 11056 . . . 4 class β„‚
53, 4cpr 4593 . . 3 class {ℝ, β„‚}
6 vx . . . . . . 7 setvar π‘₯
76cv 1541 . . . . . 6 class π‘₯
8 vf . . . . . . . . . 10 setvar 𝑓
98cv 1541 . . . . . . . . 9 class 𝑓
10 cpnf 11193 . . . . . . . . . 10 class +∞
112cv 1541 . . . . . . . . . . 11 class 𝑠
12 ctayl 25728 . . . . . . . . . . 11 class Tayl
1311, 9, 12co 7362 . . . . . . . . . 10 class (𝑠 Tayl 𝑓)
1410, 7, 13co 7362 . . . . . . . . 9 class (+∞(𝑠 Tayl 𝑓)π‘₯)
159, 14cin 3914 . . . . . . . 8 class (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯))
1615cdm 5638 . . . . . . 7 class dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯))
17 ccnfld 20812 . . . . . . . . . 10 class β„‚fld
18 ctopn 17310 . . . . . . . . . 10 class TopOpen
1917, 18cfv 6501 . . . . . . . . 9 class (TopOpenβ€˜β„‚fld)
20 crest 17309 . . . . . . . . 9 class β†Ύt
2119, 11, 20co 7362 . . . . . . . 8 class ((TopOpenβ€˜β„‚fld) β†Ύt 𝑠)
22 cnt 22384 . . . . . . . 8 class int
2321, 22cfv 6501 . . . . . . 7 class (intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt 𝑠))
2416, 23cfv 6501 . . . . . 6 class ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt 𝑠))β€˜dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯)))
257, 24wcel 2107 . . . . 5 wff π‘₯ ∈ ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt 𝑠))β€˜dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯)))
269cdm 5638 . . . . 5 class dom 𝑓
2725, 6, 26wral 3065 . . . 4 wff βˆ€π‘₯ ∈ dom 𝑓 π‘₯ ∈ ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt 𝑠))β€˜dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯)))
28 cpm 8773 . . . . 5 class ↑pm
294, 11, 28co 7362 . . . 4 class (β„‚ ↑pm 𝑠)
3027, 8, 29crab 3410 . . 3 class {𝑓 ∈ (β„‚ ↑pm 𝑠) ∣ βˆ€π‘₯ ∈ dom 𝑓 π‘₯ ∈ ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt 𝑠))β€˜dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯)))}
312, 5, 30cmpt 5193 . 2 class (𝑠 ∈ {ℝ, β„‚} ↦ {𝑓 ∈ (β„‚ ↑pm 𝑠) ∣ βˆ€π‘₯ ∈ dom 𝑓 π‘₯ ∈ ((intβ€˜((TopOpenβ€˜β„‚fld) β†Ύt 𝑠))β€˜dom (𝑓 ∩ (+∞(𝑠 Tayl 𝑓)π‘₯)))})
321, 31wceq 1542 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