Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Binary length
cblen
Next ⟩
df-blen
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cblen
Description:
Extend class notation with the class of the binary length function.
Ref
Expression
Assertion
cblen
class
#
b