Database
BASIC TOPOLOGY
Topology
Compactness
ccmp
Next ⟩
df-cmp
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
ccmp
Description:
Extend class notation with the class of all compact spaces.
Ref
Expression
Assertion
ccmp
$${class}\mathrm{Comp}$$