Metamath Proof Explorer


Syntax definition citgm

Description: Extend class notation with the (measure) Bochner integral.

Ref Expression
Assertion citgm class itgm