Database
BASIC STRUCTURES
Extensible structures
Definition of the structure product
ctopn
Next ⟩
df-rest
Metamath Proof Explorer
Ascii
Structured
Syntax definition
ctopn
Description:
Extend class notation with the topology extractor function.
Ref
Expression
Assertion
ctopn
class
TopOpen