interval): `finset α` is a locally finite order (#9963)

Commit

4 years ago

feat(data/finset/interval): `finset α` is a locally finite order (#9963) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

YaelDillies

Parents