Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Digits
cdig
Next ⟩
df-dig
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cdig
Description:
Extend class notation with the class of the digit extraction operation.
Ref
Expression
Assertion
cdig
class digit