Definition df-esum

Description: Define a short-hand for the possibly infinite sum over the extended nonnegative reals. sum* is relying on the properties of the tsums , developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016)

	Ref	Expression
Assertion	df-esum	$$⊢\underset{k\in A}{{\sum }^{*}}B=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vk	$$setvark$$
1		cA	$$classA$$
2		cB	$$classB$$
3	1 2 0	cesum	$$class\underset{k\in A}{{\sum }^{*}}B$$
4		cxrs	$$class{ℝ}_{𝑠}^{*}$$
5		cress	$$class{\upharpoonright }_{𝑠}$$
6		cc0	$$class0$$
7		cicc	$$class\left[.\right]$$
8		cpnf	$$class\mathrm{+\infty }$$
9	6 8 7	co	$$class\left[0,\mathrm{+\infty }\right]$$
10	4 9 5	co	$$class\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
11		ctsu	$$class\mathrm{tsums}$$
12	0 1 2	cmpt	$$class\left(k\in A⟼B\right)$$
13	10 12 11	co	$$class\left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
14	13	cuni	$$class\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
15	3 14	wceq	$$wff\underset{k\in A}{{\sum }^{*}}B=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$