Metamath Proof Explorer


Syntax definition cinftm

Description: Class notation for the infinitesimal relation.

Ref Expression
Assertion cinftm
class <<<