Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-esum Structured version   Unicode version

Definition df-esum 28202
Description: Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.)
Assertion
Ref Expression
df-esum  |- Σ* k  e.  A B  =  U. (
( RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )

Detailed syntax breakdown of Definition df-esum
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 vk . . 3  setvar  k
41, 2, 3cesum 28201 . 2  class Σ* k  e.  A B
5 cxrs 14917 . . . . 5  class  RR*s
6 cc0 9509 . . . . . 6  class  0
7 cpnf 9642 . . . . . 6  class +oo
8 cicc 11557 . . . . . 6  class  [,]
96, 7, 8co 6296 . . . . 5  class  ( 0 [,] +oo )
10 cress 14645 . . . . 5  classs
115, 9, 10co 6296 . . . 4  class  ( RR*ss  ( 0 [,] +oo ) )
123, 1, 2cmpt 4515 . . . 4  class  ( k  e.  A  |->  B )
13 ctsu 20750 . . . 4  class tsums
1411, 12, 13co 6296 . . 3  class  ( (
RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
1514cuni 4251 . 2  class  U. (
( RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
164, 15wceq 1395 1  wff Σ* k  e.  A B  =  U. (
( RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
Colors of variables: wff setvar class
This definition is referenced by:  esumex  28203  esumcl  28204  esumeq12dvaf  28205  esumeq2  28210  nfesum1  28214  nfesum2  28215  cbvesum  28216  esumid  28218  esumval  28220  esumf1o  28224  esumsnf  28236  esumss  28244  esumpfinval  28247  esumpfinvalf  28248
  Copyright terms: Public domain W3C validator