[Merged by Bors] - refactor(data/*/interval): generalize finset.Ico to locally finite orders

[YaelDillies]

finset.Ico currently goes ℕ → ℕ → finset ℕ. This generalizes it to α → α → finset α where locally_finite_order α.
This also ports all the existing finset.Ico lemmas to the new API, which involves renaming and moving them to data.finset.interval or data.nat.interval depending on whether I could generalize them away from ℕ or not.

---

• depends on: [Merged by Bors] - feat(order/locally_finite): introduce locally finite orders #9464
• depends on: [Merged by Bors] - feat(data/nat/interval): finite intervals of naturals #9507
• depends on: [Merged by Bors] - feat(data/fin/interval): Finite intervals in fin n #9523
• depends on: [Merged by Bors] - feat(data/int/interval): Finite intervals in ℤ #9526
• depends on: [Merged by Bors] - feat(data/pnat/interval): Finite intervals in ℕ+ #9534

[pechersky]

I don't think you need multiset.Ixx because that's provided by finset.Ixx.val.

I don't understand why we would want to get rid of list.range', list.iota, and definitely not list.range and list.range_core. They're basic primitives for computation, used in tactics and testing. Would you propose that those files have to import this file just to be able to build a sequential list of nat?

The Ico function you have built is good for proving things about the properties of the function, but it is not good for performance. I think we should retain the list.range' functions as they are, and utilize them to provide the locally_finite_order instances for nat. Possibly also int with int.range. I just don't understand what the benefit is of getting rid of the list.range-like functions, so would be happy to hear your stance on it.

It might make sense to rename the class to just locally_finite since you're not providing anything about the order in this class, the order comes solely from the preorder or order_top.

[YaelDillies]

Noted for multiset.Ixx

My reasoning was that if we could achieve what those do (including in terms of performance), then we might as well use them. But I see we are nowhere near that. So, yeah, probably not worth doing.

There are many many things which could be qualified of locally_finite. I'm pretty sure we can allow a little more verbosity to disambiguate.

What's your opinion about whether the function field should be finset-valued or list-valued? We can always get the list from the finset using finset.sort, but that may not be the most efficient way to do it given that the way we prove the instances (at least for ℕ and ℤ) is actually to first find an enumerating list.

[b-mehta]

There are many many things which could be qualified of locally_finite. I'm pretty sure we can allow a little more verbosity to disambiguate.

(for instance, mathlib already has locally finite topological spaces)

[YaelDillies]

Okay so I think this is ready for a PR. I'm offering not to touch any other file yet, because there's already a good deal of material to be reviewed. If all goes well, I will move all the finset stuff in data.finset.intervals (unless you want me to do it now?).

[pechersky]

You're going to have to at least remove the definition of finset.Ico in data.finset.intervals, otherwise they collide (the reason the tests fail atm).

I don't think the API for set.intervals needs to be copied, because of the coe and mem lemmas, the inter-op shouldn't be too bad. If you're talking about unions, differences, intersections, then the results are reachable via the set API.

In subtype.locally_finite_order, I would make (p : Prop) explicit.

[YaelDillies]

Okay well then I have to also adapt the existing API in data.finset.intervals, so it's gonna take a while.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(order/locally_finite): introduce locally finite orders #9464
• [Merged by Bors] - feat(data/nat/interval): finite intervals of naturals #9507
• [Merged by Bors] - feat(data/fin/interval): Finite intervals in fin n #9523
• [Merged by Bors] - feat(data/int/interval): Finite intervals in ℤ #9526
• [Merged by Bors] - feat(data/pnat/interval): Finite intervals in ℕ+ #9534

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[jcommelin]

@YaelDillies This PR is touch 34 files. It is not exactly clear to me what it is doing. Could you please write a bit more extensive PR description?

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests