Database
BASIC TOPOLOGY
Metric subcomplex vector spaces
Convergence and completeness
ccmet
Next ⟩
df-cfil
Metamath Proof Explorer
Unicode
Structured
Syntax definition
ccmet
Description:
Extend class notation with the class of complete metrics.
Ref
Expression
Assertion
ccmet
class CMet