Database
BASIC STRUCTURES
Extensible structures
Definition of the structure product
crest
Next ⟩
ctopn
Metamath Proof Explorer
Ascii
Structured
Syntax definition
crest
Description:
Extend class notation with the function returning a subspace topology.
Ref
Expression
Assertion
crest
class
↾
t