HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition cioc 6358
Description: Extend class notation with the set of open-below, closed-above intervals of extended reals.
Assertion
Ref Expression
cioc class (,]
See definition df-ioc 6362 for more information.
Colors of variables: wff set class
Copyright terms: Public domain