Metamath Proof Explorer


Syntax definition cvol

Description: Extend class notation with the Lebesgue measure.

Ref Expression
Assertion cvol class vol