Database
BASIC CATEGORY THEORY
Categorical constructions
Product of categories
c1stf
Next ⟩
c2ndf
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
c1stf
Description:
Extend class notation with the first projection functor.
Ref
Expression
Assertion
c1stf
class
1
st
F