Database
BASIC ALGEBRAIC STRUCTURES
Groups
Direct products
cpj1
Next ⟩
df-lsm
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cpj1
Description:
Extend class notation with left projection.
Ref
Expression
Assertion
cpj1
class proj1