Description: Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0iunmptlemfi.a | |
|
sge0iunmptlemfi.b | |
||
sge0iunmptlemfi.dj | |
||
sge0iunmptlemfi.c | |
||
sge0iunmptlemfi.re | |
||
Assertion | sge0iunmptlemfi | |