Metamath Proof Explorer


Syntax definition cutop

Description: Extend class notation with the function inducing a topology from a uniform structure.

Ref Expression
Assertion cutop class unifTop