Syntax Definition csu 15397

Description: Extend class notation to include finite and infinite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)

Hypotheses

Ref	Expression
cA	class 𝐴
cB	class 𝐵
vk	setvar 𝑘

Assertion

Ref	Expression
csu	class Σ𝑘 ∈ 𝐴 𝐵

See definition df-sum 15398 for more information.