Database
BASIC CATEGORY THEORY
Categories
Functors
cresf
Next ⟩
df-func
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cresf
Description:
Extend class notation to include restriction of a functor to a subcategory.
Ref
Expression
Assertion
cresf
class |`f