Metamath Proof Explorer


Syntax definition covol

Description: Extend class notation with the outer Lebesgue measure.

Ref Expression
Assertion covol class vol *