Description: A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | xrge0gsumle.g | |
|
xrge0gsumle.a | |
||
xrge0gsumle.f | |
||
xrge0gsumle.b | |
||
xrge0gsumle.c | |
||
Assertion | xrge0gsumle | |