Description: Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015) (Revised by Thierry Arnoux, 30-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xrge0tsmsd.g | |
|
xrge0tsmsd.a | |
||
xrge0tsmsd.f | |
||
xrge0tsmsd.s | |
||
Assertion | xrge0tsmsd | |