Metamath Proof Explorer


Syntax definition cioc

Description: Extend class notation with the set of open-below, closed-above intervals of extended reals.

Ref Expression
Assertion cioc class (,]