Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Extensible Structures
Chains
cchn
Next ⟩
df-chn
Metamath Proof Explorer
Ascii
Structured
Syntax definition
cchn
Description:
Extend class notation with the class of (finite) chains.
Ref
Expression
Assertion
cchn
class
(
<
Chain
𝐴
)