Big Summation operator

Stream: mathlib4

[Vladimir Gladstein]

Hey! I am building a project with Lean and mathlib and I need big operators for it
In particular, I want to do big summation, big set union and some other custom big operations mainly over intervals with integer values. Could you please recommend me a suitable representation of intervals and big operator for that purpose?

[Daniel Weber]

You can use finsets (docs#Finset). Because the integers are a docs#LocallyFiniteOrder, you can use docs#Finset.Ioo, docs#Finset.Ico, docs#Finset.Ioc, docs#Finset.Icc to get intervals. For summation you can use docs#Finset.sum and for set union you can use docs#Finset.sup

[Vladimir Gladstein]

Awesome, thanks