Database
BASIC TOPOLOGY
Uniform Structures and Spaces
The topology induced by an uniform structure
cutop
Next ⟩
df-utop
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cutop
Description:
Extend class notation with the function inducing a topology from a uniform structure.
Ref
Expression
Assertion
cutop
class
unifTop