Set.Accumulate

Stream: mathlib4

[Yury G. Kudryashov]

I have 2 questions about docs#Set.Accumulate:

• should it be called Set.accumulate?
• should we use docs#partialSups instead?

[Jireh Loreaux]

For the latter that changes TC assumptions significantly. So I would think not.

[Yury G. Kudryashov]

Why? Set _ satisfies all required TC assumptions.

[Yury G. Kudryashov]

UPD: I missed the point that Set.Accumulate doesn't assume the domain to be Nat.

[Yury G. Kudryashov]

Do we ever use it for other types?

[Yaël Dillies]

We use it for docs#compactCovering and docs#MeasureTheory.spanningSets, so the answer is "No, at least within mathlib".

[Yury G. Kudryashov]

Then Q2 stands.

[Yaël Dillies]

Yes, I agree with you. We should use partialSups.

[Pedro Sánchez Terraf]

Yury G. Kudryashov said:

Then Q2 stands.

Does the proposal involve deleting Accumulate? It might be still useful for unions over a well-ordered index set.

[Yaël Dillies]

What about we reintroduce it when needed? I find it a bit bloat right now and I suspect there are some places where it could have been used but wasn't because the API wasn't helpful.

[Anatole Dedecker]

I've seen multiple occasions in which I would have liked a version od docs#partialSups indexed by any ordered set (with stronger typeclass assumptions of course), so I think the right answer is to introduce this and then use it instead of docs#Set.Accumulate

[Yury G. Kudryashov]

I think that we can already migrate existing uses of Set.Accumulate to partialSups and deprecate the former.

[Yury G. Kudryashov]

OTOH, partialSups should be redefined as (Finset.Iic a).sup' _ f