Commit 2022-01-28 15:19 0b6330de
View on Github →feat(data/finsupp/interval): Finitely supported functions to a locally finite order are locally finite (#10930)
... when the codomain itself is locally finite.
This allows getting rid of finsupp.Iic_finset.