Metamath Proof Explorer


Syntax definition cfl

Description: Extend class notation with floor (greatest integer) function.

Ref Expression
Assertion cfl class .