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 26489
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 26488 . 2  class Σ* k  e.  A B
5 cxrs 14443 . . . . 5  class  RR*s
6 cc0 9287 . . . . . 6  class  0
7 cpnf 9420 . . . . . 6  class +oo
8 cicc 11308 . . . . . 6  class  [,]
96, 7, 8co 6096 . . . . 5  class  ( 0 [,] +oo )
10 cress 14180 . . . . 5  classs
115, 9, 10co 6096 . . . 4  class  ( RR*ss  ( 0 [,] +oo ) )
123, 1, 2cmpt 4355 . . . 4  class  ( k  e.  A  |->  B )
13 ctsu 19701 . . . 4  class tsums
1411, 12, 13co 6096 . . 3  class  ( (
RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
1514cuni 4096 . 2  class  U. (
( RR*ss  ( 0 [,] +oo ) ) tsums  ( k  e.  A  |->  B ) )
164, 15wceq 1369 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  26490  esumcl  26491  esumeq12dvaf  26492  esumeq2  26497  nfesum1  26501  cbvesum  26502  esumid  26504  esumval  26505  esumf1o  26509  esumsn  26520  esumss  26526  esumpfinval  26529  esumpfinvalf  26530
  Copyright terms: Public domain W3C validator