Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Partitions of real intervals
ciccp
Next ⟩
df-iccp
Metamath Proof Explorer
Ascii
Structured
Syntax definition
ciccp
Description:
Extend class notation with the partitions of a closed interval of extended reals.
Ref
Expression
Assertion
ciccp
class
RePart