Metamath Proof Explorer


Syntax definition crest

Description: Extend class notation with the function returning a subspace topology.

Ref Expression
Assertion crest class 𝑡