![]() |
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 33094 | . 2 class Σ*𝑘 ∈ 𝐴𝐵 |
5 | cxrs 17448 | . . . . 5 class ℝ*𝑠 | |
6 | cc0 11112 | . . . . . 6 class 0 | |
7 | cpnf 11247 | . . . . . 6 class +∞ | |
8 | cicc 13329 | . . . . . 6 class [,] | |
9 | 6, 7, 8 | co 7411 | . . . . 5 class (0[,]+∞) |
10 | cress 17175 | . . . . 5 class ↾s | |
11 | 5, 9, 10 | co 7411 | . . . 4 class (ℝ*𝑠 ↾s (0[,]+∞)) |
12 | 3, 1, 2 | cmpt 5231 | . . . 4 class (𝑘 ∈ 𝐴 ↦ 𝐵) |
13 | ctsu 23637 | . . . 4 class tsums | |
14 | 11, 12, 13 | co 7411 | . . 3 class ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
15 | 14 | cuni 4908 | . 2 class ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
16 | 4, 15 | wceq 1541 | 1 wff Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: esumex 33096 esumcl 33097 esumeq12dvaf 33098 esumeq2 33103 nfesum1 33107 nfesum2 33108 cbvesum 33109 esumid 33111 esumval 33113 esumf1o 33117 esumsnf 33131 esumss 33139 esumpfinval 33142 esumpfinvalf 33143 |
Copyright terms: Public domain | W3C validator |