feat(order/locally_finite): finset.interval (#17939) A finset-valued version of set.interval.
finset.interval
finset
set.interval