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