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

Definition df-esum 30860
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 Σ*𝑘𝐴𝐵 = ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))

Detailed syntax breakdown of Definition df-esum
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3cesum 30859 . 2 class Σ*𝑘𝐴𝐵
5 cxrs 16590 . . . . 5 class *𝑠
6 cc0 10372 . . . . . 6 class 0
7 cpnf 10507 . . . . . 6 class +∞
8 cicc 12580 . . . . . 6 class [,]
96, 7, 8co 7007 . . . . 5 class (0[,]+∞)
10 cress 16301 . . . . 5 class s
115, 9, 10co 7007 . . . 4 class (ℝ*𝑠s (0[,]+∞))
123, 1, 2cmpt 5035 . . . 4 class (𝑘𝐴𝐵)
13 ctsu 22405 . . . 4 class tsums
1411, 12, 13co 7007 . . 3 class ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
1514cuni 4739 . 2 class ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
164, 15wceq 1520 1 wff Σ*𝑘𝐴𝐵 = ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  esumex  30861  esumcl  30862  esumeq12dvaf  30863  esumeq2  30868  nfesum1  30872  nfesum2  30873  cbvesum  30874  esumid  30876  esumval  30878  esumf1o  30882  esumsnf  30896  esumss  30904  esumpfinval  30907  esumpfinvalf  30908
  Copyright terms: Public domain W3C validator