Database
BASIC CATEGORY THEORY
Categories
Subcategories
csubc
Next ⟩
df-ssc
Metamath Proof Explorer
Ascii
Structured
Syntax definition
csubc
Description:
Extend class notation to include the collection of subcategories of a category.
Ref
Expression
Assertion
csubc
class
Subcat