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 27834
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 27833 . 2  class Σ* k  e.  A B
5 cxrs 14767 . . . . 5  class  RR*s
6 cc0 9502 . . . . . 6  class  0
7 cpnf 9635 . . . . . 6  class +oo
8 cicc 11542 . . . . . 6  class  [,]
96, 7, 8co 6294 . . . . 5  class  ( 0 [,] +oo )
10 cress 14503 . . . . 5  classs
115, 9, 10co 6294 . . . 4  class  ( RR*ss  ( 0 [,] +oo ) )
123, 1, 2cmpt 4510 . . . 4  class  ( k  e.  A  |->  B )
13 ctsu 20469 . . . 4  class tsums
1411, 12, 13co 6294 . . 3  class  ( (
RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
1514cuni 4250 . 2  class  U. (
( RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
164, 15wceq 1379 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  27835  esumcl  27836  esumeq12dvaf  27837  esumeq2  27842  nfesum1  27846  cbvesum  27847  esumid  27849  esumval  27850  esumf1o  27854  esumsn  27865  esumss  27871  esumpfinval  27874  esumpfinvalf  27875
  Copyright terms: Public domain W3C validator