Metamath Proof Explorer


Syntax definition cppi

Description: Extend class notation with the prime-counting function pi.

Ref Expression
Assertion cppi class π _