set.Ioo

Left-open right-open interval

set.Ico

Left-closed right-open interval

set.Iio

Left-infinite right-open interval

set.Icc

Left-closed right-closed interval

set.Iic

Left-infinite right-closed interval

set.Ioc

Left-open right-closed interval

set.Ici

Left-closed right-infinite interval

set.Ioi

Left-open right-infinite interval

set.eq_of_Ico_disjoint

If two half-open intervals are disjoint and the endpoint of one lies in the other, then it must be equal to the endpoint of the other.

set.nonempty_Ico_sdiff

If we remove a smaller interval from a larger, the result is nonempty