interval): Finitely supported functions to a locally finite order are locally finite (#10930)

Commit

4 years ago

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`.

Author

YaelDillies

Parents

445be96e

mathlib 0b6330de - feat(data/finsupp/interval): Finitely supported functions to a locally finite order are locally finite (#10930)

mathlib
0b6330de - feat(data/finsupp/interval): Finitely supported functions to a locally finite order are locally finite (#10930)