Database
BASIC TOPOLOGY
Uniform Structures and Spaces
Uniform Spaces
ctus
Next ⟩
df-uss
Metamath Proof Explorer
Ascii
Structured
Syntax definition
ctus
Description:
Extend class notation with the function mapping a uniform structure to a uniform space.
Ref
Expression
Assertion
ctus
class
toUnifSp