Metamath Proof Explorer


Syntax definition cbl

Description: Extend class notation with the metric space ball function.

Ref Expression
Assertion cbl class ball