Set.Accumulate vs partialSups

Stream: mathlib4

[Etienne Marion]

Hi! Currently in Mathlib we have docs#partialSups which gives the supremum of s j for j ≤ i and is defined only for types with a sup but not necessarily an iSup and thus requires the index type to be LocallyFiniteOrderBot. On the other end we have docs#Set.Accumulate which does not require any hypothesis on the index type because the sets form a complete lattice. I would like to have an equivalent of docs#disjointed but for sets, but disjointed also requires LocallyFiniteOrderBot because it is defined via partialSups, so I had in mind to define a specific definition for disjointed adapted to sets, like Set.Accumulate is for partialSups. My question is: is it fine if I do this, or should we rather define this for a more general structure (complete lattice etc.)?

[Yaël Dillies]

I think it's fine, so long as we simultaneously switch the names of the three existing definitions + your potential new one so as to make it clear that partialSups is to Set.Accumulate what disjointed is to your new definition

[Yaël Dillies]

ie can we rename partialSups to partialFinSup and Set.Accumulate to partialSup, or something like this?

[Etienne Marion]

If we keep it specialized to sets I would propose to keep partialSups and rename Set.Accumulate to Set.partialUnions, though I'm not sure for disjointed because the wording diff/disjoint is the same in general orders and in sets.

[Eric Wieser]

Accumulate is mis-cased, right?

[David Loeffler]

Rather than special casing Set, I would suggest defining something like partialISup, for maps from an arbitrary order to an arbitrary complete lattice. (Case mavens: partialiSup or partialISup?)

[Etienne Marion]

I think the convention is partialISup

[Yaël Dillies]

I think it would actually be iPartialSup