Database
BASIC ORDER THEORY
Posets, directed sets, and lattices as relations
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
𝐴
)