Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-esum | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-esum | ⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | vk | . . 3 setvar 𝑘 | |
4 | 1, 2, 3 | cesum 29416 | . 2 class Σ*𝑘 ∈ 𝐴𝐵 |
5 | cxrs 15983 | . . . . 5 class ℝ*𝑠 | |
6 | cc0 9815 | . . . . . 6 class 0 | |
7 | cpnf 9950 | . . . . . 6 class +∞ | |
8 | cicc 12049 | . . . . . 6 class [,] | |
9 | 6, 7, 8 | co 6549 | . . . . 5 class (0[,]+∞) |
10 | cress 15696 | . . . . 5 class ↾s | |
11 | 5, 9, 10 | co 6549 | . . . 4 class (ℝ*𝑠 ↾s (0[,]+∞)) |
12 | 3, 1, 2 | cmpt 4643 | . . . 4 class (𝑘 ∈ 𝐴 ↦ 𝐵) |
13 | ctsu 21739 | . . . 4 class tsums | |
14 | 11, 12, 13 | co 6549 | . . 3 class ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
15 | 14 | cuni 4372 | . 2 class ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
16 | 4, 15 | wceq 1475 | 1 wff Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: esumex 29418 esumcl 29419 esumeq12dvaf 29420 esumeq2 29425 nfesum1 29429 nfesum2 29430 cbvesum 29431 esumid 29433 esumval 29435 esumf1o 29439 esumsnf 29453 esumss 29461 esumpfinval 29464 esumpfinvalf 29465 |
Copyright terms: Public domain | W3C validator |