Metamath Proof Explorer


Syntax definition cdit

Description: Extend class notation with the directed integral.

Ref Expression
Assertion cdit class ∫ A B C dx