mathlib
a7b92725 - feat(order/locally_finite): `finset.interval` (#17939)

Commit

2 years ago

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

Author

YaelDillies

Parents