partialSups and Accumulate

Stream: mathlib4

[Sébastien Gouëzel]

It looks like the same notion exists twice in Mathlib, as docs#partialSups and docs#Accumulate (weird capitalization for the latter, by the way):

import Mathlib

lemma foo (f : ℕ → Set α) (n : ℕ) : partialSups f n = Accumulate f n := by
  simp [partialSups_eq_sup_range, Accumulate, Nat.lt_succ_iff]

Is it worth cleaning?

[Andrew Yang]

The difference is that partialSups requires locally finiteness on the index and only asks for existence of finite unions. Set.Accumulate only requires an arbitrary LE on the index but (should) only work for lattices with infinite unions (it actually only works for Set _ which is weird).

But I don't know if we want both.

[Floris van Doorn]

Given their different type-class assumptions, I think it makes sense to have both, but maybe with more similar names (and the generalization Andrew mentions)

[Floris van Doorn]

(The capitalization might be a Mathport quirk: didn't it capitalize names of sets, since those are "really Props"? This might show how little Accumulate is used.)

[Sébastien Gouëzel]

I'm just writing a proof where I would need Accumulate and disjointed. They would naturally go together, but there is no API linking the two because all the API for disjointed is in terms of partialSups. So it's not very convenient...

[Etienne Marion]

This came up a while ago for the same reason, but in the end I found another way so didn't go with it. #mathlib4 > Set.Accumulate vs partialSups

[Yaël Dillies]

IMO both definitions could reasonably be dropped? They provide easy to derive API for easy to write functions

[Yaël Dillies]

I myself am guilty of having added more API to partialSups in my mindless youth