Metamath Proof Explorer


Syntax definition csumge0

Description: Extend class notation to include the sum of nonnegative extended reals.

Ref Expression
Assertion csumge0 class Σ^