Metamath Proof Explorer


Syntax definition cdit

Description: Extend class notation with the directed integral.

Ref Expression
Assertion cdit class ⨜ [ 𝐴𝐵 ] 𝐶 d 𝑥